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 B\mathcal{B} and J\mathcal{J} be precategories. We define the chaotic bifibration of J\mathcal{J} over B\mathcal{B} to be the displayed category where trivially fibre J\mathcal{J} over B\mathcal{B}, disregarding the structure of B\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 J\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 =
      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 idid is invertible, and also lies above every morphism in B\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.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 J\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 B\mathcal{B} and J\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