search

rzk-lang / sHoTT

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

Triangle identities #55

Closed emilyriehl closed 1 year ago

emilyriehl commented 1 year ago

This pull request contains 700 lines of code to prove the two claimed equivalences on the final two lines of page 171 (and the dual statements). The first equivalence is an immediate application of equiv-hom2-eq-comp-is-segal. The second one, relating a composition equation between natural transformations to a composition equation between their components, was surprisingly delicate because one has to relate composition in a Segal function type with componentwise composition of natural transformations.

It's possible this isn't optimal but I have tested that various proofs are not provable by refl.

This is part of the way towards the proof of Theorem 11.8 but I'm not there yet!

emilyriehl commented 1 year ago

@fizruk @jonweinb could you review this when you get the chance?

fizruk commented 1 year ago

@emilyriehl feel free to resolve the conversations above and merge.

emilyriehl commented 1 year ago

Good suggestion @fizruk. I implemented that name change for the case of function types and also for the case of extension types. I just need approval again ;)