module Cat.Displayed.Instances.Identity
  {o β„“} (B : Precategory o β„“)
  where

open Precategory B
open Displayed
open Functor
open Total-hom

The identity bifibrationπŸ”—

Let be a precategory. We can define a displayed category over whose total category is isomorphic to called the identity bifibration.

IdD : Displayed B lzero lzero
IdD .Ob[_] _ = ⊀
IdD .Hom[_] _ _ _ = ⊀
IdD .Hom[_]-set _ _ _ = hlevel!
IdD .id' = tt
IdD ._∘'_ _ _ = tt
IdD .idr' _ = refl
IdD .idl' _ = refl
IdD .assoc' _ _ _ = refl

This fibration is obviously a discrete fibration; in fact, it’s about as discrete as you can get!

IdD-discrete-fibration : Discrete-fibration IdD
IdD-discrete-fibration .Discrete-fibration.fibre-set = hlevel!
IdD-discrete-fibration .Discrete-fibration.lifts _ _ = hlevel!

Every morphism in the identity fibration is trivially cartesian and cocartesian.

idd-is-cartesian
  : βˆ€ {x y} {f : Hom x y}
  β†’ is-cartesian IdD f tt
idd-is-cartesian .is-cartesian.universal _ _ = tt
idd-is-cartesian .is-cartesian.commutes _ _ = refl
idd-is-cartesian .is-cartesian.unique _ _ = refl

idd-is-cocartesian
  : βˆ€ {x y} {f : Hom x y}
  β†’ is-cocartesian IdD f (tt)
idd-is-cocartesian .is-cocartesian.universal _ _ = tt
idd-is-cocartesian .is-cocartesian.commutes _ _ = refl
idd-is-cocartesian .is-cocartesian.unique _ _ = refl

This implies that it’s trivially a bifibration. We omit the proofs, because they are totally uninteresting.

IdD-fibration : Cartesian-fibration IdD
IdD-opfibration : Cocartesian-fibration IdD
IdD-bifibration : is-bifibration IdD

Fibre categoriesπŸ”—

The fibre categories of the identity bifibration are isomorphic to the terminal category.

IdDFib : βˆ€ x β†’ Functor ⊀Cat (Fibre IdD x)
IdDFib x .Fβ‚€ _ = tt
IdDFib x .F₁ _ = tt
IdDFib x .F-id = refl
IdDFib x .F-∘ _ _ = refl

IdD-is-iso : βˆ€ x β†’ is-precat-iso (IdDFib x)
IdD-is-iso x .is-precat-iso.has-is-ff = id-equiv
IdD-is-iso x .is-precat-iso.has-is-iso = id-equiv

Total categoryπŸ”—

The total category of the identity bifibration is isomorphic to itself.

IdDTotal : Functor B (∫ IdD)
IdDTotal .Fβ‚€ x = x , tt
IdDTotal .F₁ f = total-hom f (tt)
IdDTotal .F-id = total-hom-path _ refl refl
IdDTotal .F-∘ _ _ = total-hom-path _ refl refl

IdDTotal-is-iso : is-precat-iso IdDTotal
IdDTotal-is-iso .is-precat-iso.has-is-ff =
  is-iso→is-equiv (iso hom (λ _ → total-hom-path _ refl refl) (λ _ → refl))
IdDTotal-is-iso .is-precat-iso.has-is-iso =
  is-iso→is-equiv (iso fst (λ _ → refl) (λ _ → refl))