Investigate feature algebra composition order

[ibbem]

I'm not quite sure if LeftAdditive and RightAdditive are particular good names. Do you have any ideas for naming them?

[pmbittner]

Hi @ibbem ,
thanks for this great PR! :) I am about to push my review.

One thing I wonder is, what the following is used for and what it actually does. It seems to do some Agda compiler magic? Why is it necessary?

open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant)

[pmbittner]

See TODO commit

[ibbem]

One thing I wonder is, what the following is used for and what it actually does. It seems to do some Agda compiler magic? Why is it necessary?

open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant)

There is no magic in this module whatsoever. The K axiom (aka. uniqueness of identity proofs, short UIP) is just the following:

≡-irrelevant : ∀ {ℓ} {A : Set ℓ} → {a b : A} → (p q : a ≡ b) → p ≡ q
≡-irrelevant refl refl = refl

Indeed, this is the (simplified) proof implemented in Relation.Binary.PropositionalEquality.WithK.

The point of the separation into WithK modules is that some pattern matching rules imply the K axiom. However, the K axiom is incompatible with Univalence (the point of Homotopy Type Theory and Cubical Agda). Hence, whenever possible, the standard library uses --without-K or --cubical-compatible to ensure that these modules can be used in standard Agda and Cubical Agda without modification. In contrast, Relation.Binary.PropositionalEquality.WithK cannot be used in Cubical Agda.

By importing this module, similar to importing Axioms.Extensionality, I'm just trying to state explicitly that this relies code relies on the K axiom.

See Pattern Matching Without K if you want to learn more about how pattern matching implies the K axiom and how to avoid that.

[pmbittner]

Ah ok, thanks for the explanation! When I looked up the definition ≡-irrelevant I somehow found some function a ≡ b → a ≡ b and was confused about its purpose. Now when I look up that definition, I can find the correct definition and I can follow your explanation. (Maybe i pressed some wrong buttons in emacs or whatever, I cannot reproduce finding that other function anymore ,:D).

Explicitly documenting the dependency on axiom K via this dependency is a good idea. 👍 I would be great if you could document why we need the axiom.

[pmbittner]

Also, I will have a look at that paper. Thanks for the link. :)

[pmbittner]

Ah, I was accidentally looking at

primitive primEraseEquality : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y

and was left confused. So it was a "misclick". 😓

[pmbittner]

I recommend proceeding this line of research in a fork? What do you think? (We should only fork once we settled for a name of this library.)