module Cat.Displayed.Cartesian.Street where

# Street fibrationsπ

In classical category theory, a fibration is defined to be a certain functor $P : \mathcal{E} \to \mathcal{B}$, the idea being that $\mathcal{E}$ is really the total space of a certain displayed category, and $P$ is really the first projection functor $\pi^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 : \mathcal{E} \to \mathcal{B}$, can we create a category displayed $\mathcal{E}'$ over $\mathcal{B}$, such that $\int \mathcal{E}' \cong \mathcal{E}$?

functorβdisplayed : Displayed B (o β ββ²) (β β ββ²)
functorβdisplayed .Ob[_] x = Ξ£[ u β E.Ob ] (P.β u B.β x)

Following , 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 $\phi : P(u) \cong x$. But visually, we depict them as

whence the name βleft cornerβ. The maps lying over $f$ consist of those maps $u \to_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 $\mathcal{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β² = Ξ£-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.