Computational identity types

[fredrik-bakke]

Summary

Adds

• the strictly right unital concatenation operation on identity types.
• the strictly involutive identity types. They satisfy the judgmental laws
  1. inv (inv p) ≐ p
  2. inv refl ≐ refl
  3. refl ∙ p ≐ p or p ∙ refl ≐ p
  4. ind-Id B f refl ≐ f refl
• the Yoneda identity types. They satisfy the judgmental laws
  1. (p ∙ q) ∙ r ≐ p ∙ (q ∙ r)
  2. refl ∙ p ≐ p
  3. p ∙ refl ≐ p
  4. inv refl ≐ refl
  5. rec-Id f refl ≐ f refl
• the computational identity types. They satisfy the judgmental laws
  1. inv (inv p) ≐ p
  2. inv refl ≐ refl
  3. refl ∙ p ≐ p or p ∙ refl ≐ p
  4. (p ∙ q) ∙ r ≐ p ∙ (q ∙ r)
  5. rec-Id f refl ≐ f refl

References

• https://groups.google.com/g/homotopytypetheory/c/FfiZj1vrkmQ/m/GJETdy0AAgAJ

[fredrik-bakke]

Turns out I could also make the concatenation operation on the judgmentally involutive identity types judgmentally left unital by being a little meticulous with definitions. 😄

[EgbertRijke]

Note that we are both editing foundation-core.identity-types right now

[fredrik-bakke]

Oh, apologies. Thanks for reminding me!

[EgbertRijke]

It's ok. I can work your changes into mine if you finish before me. If I finish before you then you'll have to do it :)

[EgbertRijke]

This pull request is going to be an amazing addition to the library, and you should also think about writing up a preprint with this stuff. This is real progress.

[EgbertRijke]

This is an impressive pull request. It is very well written and well-documented. I went into more detail than usual with my feedback, because you specifically mentioned that you were shooting for perfection. Otherwise I would not have gone into such annoying detail.

My biggest complaint is that you use the words "definitional", "judgmental", and "strict" interchangeably. Note that the words "definitional" and "judgmental" are not considered synonymous. "Definitional equality" is equality that holds by definition, and judgmental equality is a notion of equality that encompasses judgmental equality, but also includes other strict equalities such as rewrite rules.

I would drop your extensive use of "definitionally unital" and or "judgmentally unital", which is used inconsistently, in favor of "strictly unital", which is also in line with your use of "strictly associative". You had some concerns about the word strict, but it is widely understood what is meant by "strict" in this setting, while your use of "definitional" in some places is widely understood to be inaccurate.

Other than that, I applaud you for finding these excellent definitions, and I am very grateful that you are adding them to the library. This is very awesome work!

[EgbertRijke]

Note that if my feedback is "too much" then I'm happy to be more lenient, because I am actually very happy with this pull request. It's just that you asked for the text to be "perfect" so I gave it a thorough read-through.

[fredrik-bakke]

I don't find your review too meticulous at all! Thanks for the added attention. It's much appreciated :)

[fredrik-bakke]

I've addressed all of your comments to the best of my ability now.