module Cat.Displayed.Instances.Trivial
  {o } (𝒞 : Precategory o )
  where

The trivial bifibration🔗

Any category can be regarded as being displayed over the terminal category

Trivial : Displayed ⊤Cat o 
Trivial .Displayed.Ob[_] _ = Ob
Trivial .Displayed.Hom[_] _ = Hom
Trivial .Displayed.Hom[_]-set _ _ _ = Hom-set _ _
Trivial .Displayed.id' = id
Trivial .Displayed._∘'_ = _∘_
Trivial .Displayed.idr' = idr
Trivial .Displayed.idl' = idl
Trivial .Displayed.assoc' = assoc

All morphisms in the trivial displayed category are vertical over the same object, so producing cartesian lifts is extremely easy: just use the identity morphism!

open Cocartesian-lift
open Cartesian-lift

Trivial-fibration : Cartesian-fibration Trivial
Trivial-fibration f y' .x' = y'
Trivial-fibration f y' .lifting = id
Trivial-fibration f y' .cartesian = cartesian-id Trivial

We can use a similar line of argument to deduce that it is also an opfibration.

Trivial-opfibration : Cocartesian-fibration Trivial
Trivial-opfibration f x' .y' =
  x'
Trivial-opfibration f x' .lifting = id
Trivial-opfibration f x' .cocartesian = cocartesian-id Trivial

Therefore, it is also a bifibration.

Trivial-bifibration : is-bifibration Trivial
Trivial-bifibration .is-bifibration.fibration = Trivial-fibration
Trivial-bifibration .is-bifibration.opfibration = Trivial-opfibration

The joint cartesian morphisms in the trivial displayed category are precisely the projections out of indexed products.

trivial-joint-cartesian→product
  :  {κ} {Ix : Type κ}
   {∏xᵢ : Ob} {xᵢ : Ix  Ob} {π : (i : Ix)  Hom ∏xᵢ (xᵢ i)}
   is-jointly-cartesian Trivial  _  tt) π
   is-indexed-product 𝒞 xᵢ π

product→trivial-joint-cartesian
  :  {κ} {Ix : Type κ}
   {∏xᵢ : Ob} {xᵢ : Ix  Ob} {π : (i : Ix)  Hom ∏xᵢ (xᵢ i)}
   is-indexed-product 𝒞 xᵢ π
   is-jointly-cartesian Trivial  _  tt) π
The proofs are basically just shuffling data around, so we will not describe the details.
trivial-joint-cartesian→product {xᵢ = xᵢ} {π = π} π-cart =
  π-product
  where
    module π = is-jointly-cartesian π-cart
    open is-indexed-product

    π-product : is-indexed-product 𝒞 xᵢ π
    π-product .tuple fᵢ = π.universal tt fᵢ
    π-product .commute = π.commutes tt _ _
    π-product .unique fᵢ p = π.unique _ p

product→trivial-joint-cartesian {xᵢ = xᵢ} {π = π} π-product =
  π-cart
  where
    module π = is-indexed-product π-product
    open is-jointly-cartesian

    π-cart : is-jointly-cartesian Trivial  _  tt) π
    π-cart .universal tt fᵢ = π.tuple fᵢ
    π-cart .commutes tt fᵢ ix = π.commute
    π-cart .unique other p = π.unique _ p

In contrast, the cartesian morphisms in the trivial displayed category are the invertible morphisms.

invertible→trivial-cartesian
  :  {a b} {f : Hom a b}
   is-invertible f
   is-cartesian Trivial tt f

trivial-cartesian→invertible
  :  {a b} {f : Hom a b}
   is-cartesian Trivial tt f
   is-invertible f

The forward direction is easy: every invertible morphism is cartesian, and the invertible morphisms in the trivial displayed category on are the invertible maps in

invertible→trivial-cartesian f-inv =
  invertible→cartesian Trivial
    (⊤Cat-is-pregroupoid tt)
    (invertible→trivial-invertible f-inv)

For the reverse direction, recall that all vertical cartesian morphisms are invertible. Every morphism in the trivial displayed category is vertical, so cartesianness implies invertibility.

trivial-cartesian→invertible f-cart =
  trivial-invertible→invertible $
  vertical+cartesian→invertible Trivial f-cart

Furthermore, the total category of the trivial bifibration is isomorphic to the category we started with.

trivial-total : Functor ( Trivial) 𝒞
trivial-total .F₀ = snd
trivial-total .F₁ = preserves
trivial-total .F-id = refl
trivial-total .F-∘ _ _ = refl

trivial-total-iso : is-precat-iso trivial-total
trivial-total-iso .is-precat-iso.has-is-ff =
  is-iso→is-equiv $
    iso (total-hom tt)
         _  refl)
         _  total-hom-pathp Trivial refl refl refl refl)
trivial-total-iso .is-precat-iso.has-is-iso =
  is-iso→is-equiv $
    iso (tt ,_)
         _  refl)
         _  refl ,ₚ refl)

As the trivial bifibration only has one fibre, this fibre is also isomorphic to

trivial-fibre : Functor (Fibre Trivial tt) 𝒞
trivial-fibre .F₀ x = x
trivial-fibre .F₁ f = f
trivial-fibre .F-id = refl
trivial-fibre .F-∘ _ _ = transport-refl _

trivial→fibre-iso : is-precat-iso trivial-fibre
trivial→fibre-iso .is-precat-iso.has-is-ff = id-equiv
trivial→fibre-iso .is-precat-iso.has-is-iso = id-equiv