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 category 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

  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 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.∘ 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 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' = Σ-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.