search

rzk-lang / sHoTT

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

Towards Theorem 8.8 #58

Closed cesarbm03 closed 1 year ago

cesarbm03 commented 1 year ago

Preliminary definitions

emilyriehl commented 1 year ago

@cesarbm03 I'm going to merge this now but as a warning I renamed some of your terms. Since all terms are globally defined we have to be careful to only use generic names like map-to-fiber for very general concepts.