module Cat.Displayed.Cartesian.Street where

# Street fibrationsπ

In classical category theory, a fibration is defined to be a certain functor $P:EβB,$ the idea being that $E$ is really the total category of a certain displayed category, and $P$ is really the first projection functor $Ο_{f},$ which sends each displayed object to the object it is displayed over. But can we go the other way? If we have a functor $P:EβB,$ can we create a category displayed $E_{β²}$ over $B,$ such that $β«E_{β²}βE?$

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 = Functor P

functorβdisplayed : Displayed B (o β β') (β β β') functorβdisplayed .Ob[_] x = Ξ£[ u β E ] (P.β u B.β x)

Following (Sterling and Angiuli 2022), we define such a category by defining the space of objects over $x$ to be βleft cornersβ. Strictly speaking, a left corner is given by an object $u$ together with an isomorphism $Ο:P(u)βx.$ But visually, we depict them as

whence the name βleft cornerβ. The maps lying over $f$ consist of those maps $uβ_{f}v$ 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 $E,$ 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' = Ξ£-prop-pathp! (E.idr _) functorβdisplayed .idl' f' = Ξ£-prop-pathp! (E.idl _) functorβdisplayed .assoc' f' g' h' = Ξ£-prop-pathp! (E.assoc _ _ _)

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/frct-003I.xml.