module Cat.Displayed.Instances.Chaotic {o β o' β'} (B : Precategory o β) (J : Precategory o' β') where private module B = Cat.Reasoning B module J = Cat.Reasoning J open Functor open Displayed open Total-hom
The Chaotic Bifibrationπ
Let and be precategories. We define the chaotic bifibration of over to be the displayed category where we trivially fibre over , disregarding the structure of entirely.
Chaotic : Displayed B o' β' Chaotic. Ob[_] _ = J.Ob Chaotic .Hom[_] _ = J.Hom Chaotic .Hom[_]-set _ = J.Hom-set Chaotic .idβ² = J.id Chaotic ._ββ²_ = J._β_ Chaotic .idrβ² = J.idr Chaotic .idlβ² = J.idl Chaotic .assocβ² = J.assoc
Note that the only cartesian morphisms in the chaotic bifibration are the isomorphisms in :
chaotic-cartesianβis-iso : β {x y x' y'} {f : B.Hom x y} {g : J.Hom x' y'} β is-cartesian Chaotic f g β J.is-invertible g chaotic-cartesianβis-iso cart = J.make-invertible (universal B.id J.id) (commutes B.id J.id) (unique _ (J.cancell (commutes B.id J.id)) β sym (unique {m = B.id} J.id (J.idr _))) where open is-cartesian cart is-isoβchaotic-cartesian : β {x y x' y'} {f : B.Hom x y} {g : J.Hom x' y'} β J.is-invertible g β is-cartesian Chaotic f g is-isoβchaotic-cartesian {f = f} {g = g} is-inv = cart where open J.is-invertible is-inv open is-cartesian cart : is-cartesian Chaotic f g cart .universal _ h = inv J.β h cart .commutes _ h = J.cancell invl cart .unique {hβ² = h} m p = m β‘β¨ J.introl invr β©β‘ (inv J.β g) J.β m β‘β¨ J.pullr p β©β‘ inv J.β h β
This implies that the chaotic fibration is a fibration, as
is invertible, and also lies above every morphism in
.
We could use our lemmas from before to show this, but doing it by hand
lets us avoid an extra id
composite when constructing the
universal map.
Chaotic-fibration : Cartesian-fibration Chaotic Chaotic-fibration .Cartesian-fibration.has-lift f y = cart-lift where open Cartesian-lift open is-cartesian cart-lift : Cartesian-lift Chaotic f y cart-lift .xβ² = y cart-lift .lifting = J.id cart-lift .cartesian .universal _ g = g cart-lift .cartesian .commutes _ g = J.idl g cart-lift .cartesian .unique m p = sym (J.idl m) β p
We observe a similar situation for cocartesian morphisms.
chaotic-cocartesianβis-iso : β {x y x' y'} {f : B.Hom x y} {g : J.Hom x' y'} β is-cocartesian Chaotic f g β J.is-invertible g chaotic-cocartesianβis-iso cocart = J.make-invertible (universal B.id J.id) (unique _ (J.cancelr (commutes B.id J.id)) β sym (unique {m = B.id} J.id (J.idl _))) (commutes B.id J.id) where open is-cocartesian cocart is-isoβchaotic-cocartesian : β {x y x' y'} {f : B.Hom x y} {g : J.Hom x' y'} β J.is-invertible g β is-cocartesian Chaotic f g is-isoβchaotic-cocartesian {f = f} {g = g} is-inv = cocart where open J.is-invertible is-inv open is-cocartesian cocart : is-cocartesian Chaotic f g cocart .universal _ h = h J.β inv cocart .commutes _ h = J.cancelr invr cocart .unique {hβ² = h} m p = m β‘β¨ J.intror invl β©β‘ m J.β g J.β inv β‘β¨ J.pulll p β©β‘ h J.β inv β Chaotic-opfibration : Cocartesian-fibration Chaotic Chaotic-opfibration .Cocartesian-fibration.has-lift f x' = cocart-lift where open Cocartesian-lift open is-cocartesian cocart-lift : Cocartesian-lift Chaotic f x' cocart-lift .yβ² = x' cocart-lift .lifting = J.id cocart-lift .cocartesian .universal _ g = g cocart-lift .cocartesian .commutes _ g = J.idr g cocart-lift .cocartesian .unique m p = sym (J.idr m) β p
This implies that the chaotic bifibration actually lives up to its name.
Chaotic-bifibration : is-bifibration Chaotic Chaotic-bifibration .is-bifibration.fibration = Chaotic-fibration Chaotic-bifibration .is-bifibration.opfibration = Chaotic-opfibration
Fibre Categoriesπ
Unsurprisingly, the fibre categories of the chaotic bifibration are isomorphic to .
ChaoticFib : β x β Functor J (Fibre Chaotic x) ChaoticFib x .Fβ j = j ChaoticFib x .Fβ f = f ChaoticFib x .F-id = refl ChaoticFib x .F-β _ _ = sym (transport-refl _) ChaoticFib-is-iso : β x β is-precat-iso (ChaoticFib x) ChaoticFib-is-iso x .is-precat-iso.has-is-ff = id-equiv ChaoticFib-is-iso x .is-precat-iso.has-is-iso = id-equiv
Total Categoryπ
The total category of the chaotic bifibration is isomorphic to the product of and .
ChaoticTotal : Functor (B ΓαΆ J) (β« Chaotic) ChaoticTotal .Fβ bj = bj ChaoticTotal .Fβ (f , g) = total-hom f g ChaoticTotal .F-id = total-hom-path Chaotic refl refl ChaoticTotal .F-β f g = total-hom-path Chaotic refl refl ChaoticTotal-is-iso : is-precat-iso ChaoticTotal ChaoticTotal-is-iso .is-precat-iso.has-is-ff = is-isoβis-equiv (iso (Ξ» f β f .hom , f .preserves) (Ξ» _ β total-hom-path Chaotic refl refl) (Ξ» _ β refl)) ChaoticTotal-is-iso .is-precat-iso.has-is-iso = id-equiv