open import Cat.Displayed.Cartesian.Discrete
open import Cat.Instances.Shape.Terminal
open import Cat.Displayed.Bifibration
open import Cat.Displayed.Cocartesian
open import Cat.Displayed.Cartesian
open import Cat.Functor.Equivalence
open import Cat.Displayed.Fibre
open import Cat.Displayed.Total
open import Cat.Displayed.Base
open import Cat.Prelude

module Cat.Displayed.Instances.Identity
  {o ℓ} (B : Precategory o ℓ)
  where

open Precategory B
open Displayed
open Functor
open Total-hom

The identity bifibration🔗

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

IdD-fibration .Cartesian-fibration.has-lift f y' .Cartesian-lift.x' = tt
IdD-fibration .Cartesian-fibration.has-lift f y' .Cartesian-lift.lifting = tt
IdD-fibration .Cartesian-fibration.has-lift f y' .Cartesian-lift.cartesian =
  idd-is-cartesian

IdD-opfibration .Cocartesian-fibration.has-lift f x' .Cocartesian-lift.y' = tt
IdD-opfibration .Cocartesian-fibration.has-lift f x' .Cocartesian-lift.lifting = tt
IdD-opfibration .Cocartesian-fibration.has-lift f x' .Cocartesian-lift.cocartesian =
  idd-is-cocartesian

IdD-bifibration .is-bifibration.fibration = IdD-fibration
IdD-bifibration .is-bifibration.opfibration = IdD-opfibration

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 $\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))