search

rzk-lang / sHoTT

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

Fiber facts #93

Closed emilyriehl closed 1 year ago

emilyriehl commented 1 year ago

This proves some lemmas about fibers that I noticed were missing from the HoTT directory while working on something similar to PR #88. In particular, I don't believe we'd calculated that the homotopy fiber of the projection from a total type is equivalent to the strict fiber (in the type family).

I'd be grateful for suggestions about the namings of terms and other ideas for streamlining the code.

emilyriehl commented 1 year ago

Thanks @fredrik-bakke. I've implemented all the suggested name changes now.

fredrik-bakke commented 1 year ago

Great! I'll merge this PR now so I can merge the other one as well :)