search

rzk-lang / sHoTT

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

moved homotopy pullbacks into new file #72

Closed emilyriehl closed 1 year ago

emilyriehl commented 1 year ago

Mostly this takes the material on homotopy pullbacks and creates a new file at the end of the hott directory.

I also renamed the "codomain-based-path-space" which had been bothering me to "endpoint-based-paths".

I also shortened the "Covariantly functorial type familes" to "Covariant families" which is what we actually call them everywhere.

emilyriehl commented 1 year ago

@fizruk if you have a moment this PR involved some reorganization so it would be good to merge.