search

rzk-lang / sHoTT

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

Fibers between Segal types are Segal #122

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

Direct corollary of #120.

TashiWalde commented 1 year ago

Hi @TashiWalde. I'm going to approve now for easy merging but out of curiosity what is the point of unpack-is-local-horn-inclusion?

It was mostly a sanity check to myself when I replaced the original definition of is-local-horn-inclusion with the one using the general theory; to make sure it was just the (definitionally) same. I left it in so that the reader can see at a glance what the definition expands to. It has no technical purpose for formalization.