Generalized proofs of [RS17, Cor. 5.6]

[thchatzidiamantis]

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]

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]

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]

@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