module Cat.Displayed.Cartesian.Street where
Street fibrationsπ
In classical category theory, a fibration is defined to be a certain functor , the idea being that is really the total space of a certain displayed category, and is really the first projection functor , which sends each displayed object to the object it is displayed over. But can we go the other way? If we have a functor , can we create a category displayed over , such that ?
module _ {o β oβ² ββ²} {E : Precategory o β} {B : Precategory oβ² ββ²} (P : Functor E B) where private module E = Cat.Reasoning E module B = Cat.Reasoning B module P = Cat.Functor.Reasoning P open B.HLevel-instance open E.HLevel-instance
functorβdisplayed : Displayed B (o β ββ²) (β β ββ²) functorβdisplayed .Ob[_] x = Ξ£[ u β E.Ob ] (P.β u B.β x)
Following (Sterling and Angiuli 2022), we define such a category by defining the space of objects over to be βleft cornersβ. Strictly speaking, a left corner is given by an object together with an isomorphism . But visually, we depict them as
whence the name βleft cornerβ. The maps lying over consist of those maps which commute with the mediating isomorphisms:
functorβdisplayed .Hom[_] f (u , Ο) (v , Ο) = Ξ£[ h β E.Hom u v ] (B.to Ο B.β P.β h β‘ f B.β B.to Ο)
This fits in a diagram like the one below. Note that the commutativity condition is for the lower shape, which is a distorted square.
The axioms for a displayed category are evident: all that matters are the maps in the total category , since the rest of the data is property (rather than data).
functorβdisplayed .Hom[_]-set f a b = hlevel 2 functorβdisplayed .idβ² = E.id , B.elimr P.F-id β B.introl refl functorβdisplayed ._ββ²_ (f , Ο) (g , Ο) = f E.β g , apβ B._β_ refl (P.F-β f g) β B.pulll Ο β B.pullr Ο β B.assoc _ _ _ functorβdisplayed .idrβ² fβ² = Ξ£-pathp-dep (E.idr _) $ is-setβsquarep (Ξ» _ _ β hlevel 2) _ _ _ _ functorβdisplayed .idlβ² fβ² = Ξ£-pathp-dep (E.idl _) $ is-setβsquarep (Ξ» _ _ β hlevel 2) _ _ _ _ functorβdisplayed .assocβ² fβ² gβ² hβ² = Ξ£-pathp-dep (E.assoc _ _ _) $ is-setβsquarep (Ξ» _ _ β hlevel 2) _ _ _ _
We call a functor that gives rise to a Cartesian fibration through this process a Street fibration. It is routine to verify that our notion of Street fibration corresponds to.. well, Streetβs.
References
- Sterling, Jonathan, and Carlo Angiuli. 2022. βFoundations of Relative Category Theory.β https://www.jonmsterling.com/math/lectures/categorical-foundations.html.