search

rzk-lang / sHoTT

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

Unit and counit and transposition #37

Closed emilyriehl closed 1 year ago

emilyriehl commented 1 year ago

This proves equivalences between units and counits and the transposition maps of an adjunction.

The proof used a dual version of the Yoneda lemma, which was added, involving the equivalence in the other direction.