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 $P : \mathcal{E} \to \mathcal{B}$, the idea being that $\mathcal{E}$ is really the total category 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}$?

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
open B.HLevel-instance
open E.HLevel-instance

  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 (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.