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

open Precategory B
open Displayed
open Functor
open Total-hom

The Identity BifibrationπŸ”—

Let B\mathcal{B} be a precategory. We can define a displayed category Id(B)\mathrm{Id}(\mathcal{B}) over BB whose total category is isomorphic to BB, 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 B\mathcal{B} 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))