open import Cat.Displayed.Cartesian open import Cat.Displayed.Fibre open import Cat.Displayed.Total open import Cat.Displayed.Base open import Cat.Prelude import Cat.Functor.Reasoning import Cat.Reasoning 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 space 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.Ob ] (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.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′ = Σ-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.
References
- Sterling, Jonathan, and Carlo Angiuli. 2022. “Foundations of Relative Category Theory.” https://www.jonmsterling.com/math/lectures/categorical-foundations.html.