search

rzk-lang / sHoTT

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

Generalized proofs of [RS17, Cor. 5.6] #147

Open thchatzidiamantis opened 2 months ago

thchatzidiamantis commented 2 months ago

The proof that function types into a fiberwise Segal family are Segal can me made to say that dependent function types where the family is local with respect to a shape inclusion are themselves local with respect to the same shape inclusion.

nimarasekh commented 2 months ago

It might be worth pointing out, that if this is implemented then beyond just for Segal spaces, this can also directly be applied to 2-Segal spaces, rather than having to crudely copy paste code.

TashiWalde commented 2 months ago

Also note that a relative version of this statement already exists in is-right-orthogonal-Π-to-shape. It says that if you have a family of right orthogonal maps, then the induces map of pi-types is also right orthogonal.

emilyriehl commented 3 weeks ago

@thchatzidiamantis I'm sorry this has languished for so long. It's been a busy teaching semester.

I started to look at this today and couldn't find the term is-right-orthogonal-Pi-to-shape that @TashiWalde refers to. Is that also in this file? I wonder if it makes sense to deduce the special case from the relative one using the connection between is-right-orthogonal and is-local