module Cat.Displayed.Instances.Chaotic
  {o β„“ o' β„“'} (B : Precategory o β„“) (J : Precategory o' β„“')

  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' =
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

  : βˆ€ {x y x' y'} {f : B.Hom x y} {g : J.Hom x' y'}
  β†’ is-cartesian Chaotic f g β†’ g
chaotic-cartesian→is-iso cart =
    (unique _ (J.cancell (commutes
     βˆ™ sym (unique {m =} (J.idr _)))
  where open is-cartesian cart

  : βˆ€ {x y x' y'} {f : B.Hom x y} {g : J.Hom x' y'}
  β†’ g β†’ is-cartesian Chaotic f g
is-iso→chaotic-cartesian {f = f} {g = g} is-inv = cart
    open 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 =
  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.

  : βˆ€ {x y x' y'} {f : B.Hom x y} {g : J.Hom x' y'}
  β†’ is-cocartesian Chaotic f g β†’ g
chaotic-cocartesian→is-iso cocart =
    (unique _ (J.cancelr (commutes
     βˆ™ sym (unique {m =} (J.idl _)))
  where open is-cocartesian cocart

  : βˆ€ {x y x' y'} {f : B.Hom x y} {g : J.Hom x' y'}
  β†’ g β†’ is-cocartesian Chaotic f g
is-iso→chaotic-cocartesian {f = f} {g = g} is-inv = cocart
    open 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 =
  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 =
    (iso (Ξ» f β†’ f .hom , f .preserves)
    (Ξ» _ β†’ total-hom-path Chaotic refl refl)
    (Ξ» _ β†’ refl))
ChaoticTotal-is-iso .is-precat-iso.has-is-iso = id-equiv