open import Cat.Displayed.Bifibration
open import Cat.Displayed.Cocartesian
open import Cat.Displayed.Cartesian
open import Cat.Functor.Equivalence
open import Cat.Instances.Product
open import Cat.Displayed.Fibre
open import Cat.Displayed.Total
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Reasoning

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 $\mathcal{B}$ and $\mathcal{J}$ be precategories. We define the chaotic bifibration of $\mathcal{J}$ over $\mathcal{B}$ to be the displayed category where we trivially fibre $\mathcal{J}$ over $\mathcal{B}$, disregarding the structure of $\mathcal{B}$ 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 $\mathcal{J}$:

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 =
(inv J.β g) J.β m     β‘β¨ J.pullr p β©β‘
inv J.β h             β


This implies that the chaotic fibration is a fibration, as $id$ is invertible, and also lies above every morphism in $\mathcal{B}$. 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.β 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 $\mathcal{J}$.

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 $\mathcal{B}$ and $\mathcal{J}$.

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