open import Cat.Functor.Equivalence.Path 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.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 Cartesian-fibration open Cocartesian-fibration open Cartesian-lift open Cocartesian-lift Trivial-fibration : Cartesian-fibration Trivial Trivial-fibration .has-lift f yβ² .xβ² = yβ² Trivial-fibration .has-lift f yβ² .lifting = id Trivial-fibration .has-lift 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 .has-lift f xβ² .yβ² = xβ² Trivial-opfibration .has-lift f xβ² .lifting = id Trivial-opfibration .has-lift 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
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