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                     β‘
(inv J.β g) J.β m     β‘
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               β‘
m J.β g J.β inv β‘
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