module Cat.Displayed.Cartesian.Street where

Street fibrationsπŸ”—

In classical category theory, a fibration is defined to be a certain functor P:Eβ†’BP : \mathcal{E} \to \mathcal{B}, the idea being that E\mathcal{E} is really the total category of a certain displayed category, and PP is really the first projection functor Ο€f\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:Eβ†’BP : \mathcal{E} \to \mathcal{B}, can we create a category displayed Eβ€²\mathcal{E}' over B\mathcal{B}, such that ∫Eβ€²β‰…E\int \mathcal{E}' \cong \mathcal{E}?

  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 xx to be β€œleft corners”. Strictly speaking, a left corner is given by an object uu together with an isomorphism Ο•:P(u)β‰…x\phi : P(u) \cong x. But visually, we depict them as

whence the name β€œleft corner”. The maps lying over ff consist of those maps uβ†’fvu \to_f v which commute with the mediating isomorphisms:

  functorβ†’displayed .Hom[_] f (u , Ο†) (v , ψ) =
    Ξ£[ h ∈ E.Hom u v ] ( ψ B.∘ P.₁ h ≑ f B.∘ Ο†)

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\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' = , 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 (E.idr _) $
    is-set→squarep (λ _ _ → hlevel 2) _ _ _ _
  functor→displayed .idl' f' = Σ-pathp (E.idl _) $
    is-set→squarep (λ _ _ → hlevel 2) _ _ _ _
  functor→displayed .assoc' f' g' h' = Σ-pathp (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.