Closed TashiWalde closed 1 year ago
Thanks @TashiWalde! Cf. also [BW23, Subsection 3.1.2].
- For every map
f : B -> A
right orthogonal toϕ ⊂ ψ
, the fibersfib B A f a
have unique extensions with respect toϕ ⊂ ψ
.- As a corollary we get that for any map between types with unique extensions, the fibers have again unique extensions.
- In particular, this answers a question I was discussing with @emilyriehl : every map between Segal types has Segal fibers. I haven't yet formalized that specific instance, since I wasn't sure if this was something someone else (@nimarasekh ?) already did/wanted to do.
- I have also reorganized and expanded the material about functoriality of extension types in 03-extension-types.
Just to make sure, I don't think I had any particular plans to formalize this statement, as I was working on other stuff in Section 8 (whereas to me this seems like it would fit into Section 5)? So @TashiWalde you should feel free to go for it if you want.
f : B -> A
right orthogonal toϕ ⊂ ψ
, the fibersfib B A f a
have unique extensions with respect toϕ ⊂ ψ
.