search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
46 stars 12 forks source link

Isomorphism extensionality #85

Closed dvmcarpena closed 1 year ago

dvmcarpena commented 1 year ago

Closes #23. In addition to iso extensionality, I have proven some HoTT results needed for the proof.

List of things proven:

  1. Substitution law for transport.
  2. Type theoretic principle of choice.
  3. Iso extensionality.

Main concerns:

  1. I think names in general can be improved, please suggest any idea.
  2. I tried to put the substitution law for transport inside the section of transport, but failed. Adding the type "A'" was conflicting in some way with the variable "A", and I was not able to solve. That's why now it is just outside the section. Maybe someone can help me with that, or we leave it like that.
  3. My first proof of the type theoretic principle of choice followed the book of Rijke and needed function extensionality (see the commit for more details). For some reason, I tried to replace the non-trivial part of the proof by refl, and it just worked. I don't understand what's rzk doing there.
TashiWalde commented 1 year ago

It seems like some of these things might already exist in the library. For example sigma-preserves-second is In 08 under the name total-equiv-family-equiv. And sigma-preserves-first seems to basically be the same as total-equiv-pullback-is-equiv.

dvmcarpena commented 1 year ago

You're totally right, thank you! I have removed the redundant definitions and changed the proof to use the already existing ones.