search

rzk-lang / sHoTT

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

Formalization of Prop 10.3 of [RS17] #66

Closed dvmcarpena closed 1 year ago

dvmcarpena commented 1 year ago

Closes #22 . Depends on some helper definitions in #55 , so it should not be merged before that one.

The PR also contains some basic results about propositions that I couldn't find in the library. Proof of 10.3 is split into three definitions: the map from natural isos to pointwise natural isos, the inverse map, and the proof of the equivalence. I am not sure of the names, please feel free to suggest better ones!

emilyriehl commented 1 year ago

@dvmcarpena thanks for all this work. I'm going to hold off reviewing until I can get someone to look at the open adjunctions PR.

emilyriehl commented 1 year ago

@dvmcarpena I did some renaming and changed the inputs to your function twice. Throught the library we often prove a logical equivalence iff so I took that data as an input.

I'm going to merge this now to free up space for something else.