open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

module Cat.Displayed.Cartesian.Street where

open Displayed


# 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

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 , 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' = Ξ£-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.