module Cat.Displayed.Instances.Externalisation
  {o β„“} (B : Precategory o β„“) (β„‚ : Internal-cat B)
  where

Externalisation of internal categoriesπŸ”—

Every internal category in gives rise to a fibration over known as the externalisation of The core idea is almost the same as that of the family fibration, but with playing the role of The space of objects over will be the generalised objects

Externalise : Displayed B β„“ β„“
Externalise = disp module Externalisation where
  disp : Displayed B β„“ β„“
  disp .Ob[_] Ξ“ = Hom Ξ“ Cβ‚€

Morphisms over are given by commuting diagrams of the following form:

The intuition here is that a generalized object can be seen as a family of morphisms in the internal category. To display one of these families over a map we simply precompose with the domain of the internal morphism; this yields something that mirrors the morphisms in the family fibration.

The identity morphism of families can almost be given by the identity morphism, though we run into definitional equality issues. A similar situation occurs for composition, though luckily these issues aren’t too hard to work around.

  disp .Hom[_] u x y = Homi x (y ∘ u)
  disp .Hom[_]-set _ _ _ = Internal-hom-set
  disp .id' = adjusti refl (sym (idr _)) (idi _)
  disp ._∘'_ {f = u} {g = v} f g = adjusti refl (sym (assoc _ _ _)) (f [ v ] ∘i g)
Unfortunately, proof assistants make establishing the axioms fairly nasty. Associativity is especially bad.
  disp .idr' f =
    Internal-hom-pathp refl (ap (_ ∘_) (idr _)) $
      (f [ id ] ∘i adjusti _ _ (idi _)) .ihom β‰‘βŸ¨ ∘i-ihom refl (idr _) (idr _) (idr _) refl βŸ©β‰‘
      (f ∘i idi _) .ihom                      β‰‘βŸ¨ ap ihom (idri _) βŸ©β‰‘
      f .ihom ∎
  disp .idl' {f = u} f =
    Internal-hom-pathp refl (ap (_ ∘_) (idl _)) $
      (adjusti _ _ (idi _) [ u ] ∘i f) .ihom β‰‘βŸ¨ ∘i-ihom refl refl (ap (_∘ _) (idr _)) (ap ihom (idi-nat u)) refl βŸ©β‰‘
      (idi _ ∘i f) .ihom                     β‰‘βŸ¨ ap ihom (idli _) βŸ©β‰‘
      f .ihom                                ∎
  disp .assoc' {w = a} {b} {c} {d} {f = u} {g = v} {h = w} f g h =
    Internal-hom-pathp refl (ap (_ ∘_) (assoc _ _ _)) $
    (f [ v ∘ w ] ∘i adjusti _ _ (g [ w ] ∘i h)) .ihom β‰‘βŸ¨ ∘i-ihom refl refl refl refl (∘i-ihom refl refl (sym (assoc _ _ _)) g-path refl) βŸ©β‰‘
    (f [ v ∘ w ] ∘i g' ∘i h) .ihom                    β‰‘βŸ¨ ap ihom (associ _ _ _) βŸ©β‰‘
    ((f [ v ∘ w ] ∘i g') ∘i h) .ihom                  β‰‘βŸ¨ ∘i-ihom refl refl reassoc inner refl βŸ©β‰‘
    (adjusti _ _ (f [ v ] ∘i g) [ w ] ∘i h) .ihom     ∎
    where
      g' : Homi (b ∘ w) (c ∘ v ∘ w)
      g' = coe1β†’0 (Ξ» i β†’ Homi (b ∘ w) (assoc c v w i)) (g [ w ])

      g-path : g .ihom ∘ w ≑ g' .ihom
      g-path = sym (transport-refl _)

      reassoc : (d ∘ u) ∘ (v ∘ w) ≑ (d ∘ u ∘ v) ∘ w
      reassoc = pulll (sym (assoc _ _ _))

      inner : (f [ v ∘ w ] ∘i g') .ihom ≑ (f [ v ] ∘i g) .ihom ∘ w
      inner =
        (f [ v ∘ w ] ∘i g') .ihom          β‰‘βŸ¨ ∘i-ihom refl (assoc _ _ _) (assoc _ _ _) (assoc _ _ _) (transport-refl _) βŸ©β‰‘
        ((f [ v ]) [ w ] ∘i g [ w ]) .ihom β‰‘Λ˜βŸ¨ ap ihom (∘i-nat (f [ v ]) g w) βŸ©β‰‘Λ˜
        (f [ v ] ∘i g) .ihom ∘ w           ∎

Cartesian mapsπŸ”—

To really hammer home that point that the externalisation of an internal category is the internal version of the family fibration, we show that the cartesian morphisms are precisely the internal isomorphisms.

The forward direction looks almost identical to the proof that pointwise isomorphisms are cartesian morphisms in the family fibration.

internal-iso→cartesian
  : βˆ€ {Ξ“ Ξ” : Ob} {u : Hom Ξ“ Ξ”} {x : Hom Ξ“ Cβ‚€} {y : Hom Ξ” Cβ‚€}
  β†’ (f : Homi x (y ∘ u))
  β†’ is-invertiblei f
  β†’ is-cartesian Externalise u f
internal-iso→cartesian {Γ} {Δ} {u} {x} {y} f f-inv = cart where
  open is-cartesian
  module f-inv = is-invertiblei f-inv
  open f-inv using (invi)

  cart : is-cartesian _ _ _
  cart .universal {u' = u'} m h' =
    invi [ m ] ∘i adjusti refl (assoc y u m) h'
  cart .commutes {u' = u'} m h' =
    Internal-hom-path $
    (f [ m ] ∘i invi [ m ] ∘i _) .ihom      β‰‘βŸ¨ ap ihom (pullli (sym (∘i-nat f invi m))) βŸ©β‰‘
    (⌜ f ∘i invi ⌝ [ m ] ∘i _) .ihom        β‰‘βŸ¨ ap! f-inv.invli βŸ©β‰‘
    (⌜ idi _ [ m ] ⌝ ∘i _) .ihom            β‰‘βŸ¨ ap! (idi-nat m) βŸ©β‰‘
    (idi _ ∘i _) .ihom                      β‰‘βŸ¨ ap ihom (idli _) βŸ©β‰‘
    h' .ihom                                ∎
  cart .unique {u' = u'} {m = m} {h' = h'} m' p =
    Internal-hom-path $
    m' .ihom                                β‰‘βŸ¨ ap ihom (introli (Internal-hom-path (ap ihom (idi-nat m)))) βŸ©β‰‘
    (⌜ idi _ [ m ] ⌝ ∘i m') .ihom           β‰‘βŸ¨ ap! (ap (Ξ» e β†’ e [ m ]) (sym (f-inv.invri)) βˆ™ ∘i-nat _ _ _) βŸ©β‰‘
    ((invi [ m ] ∘i f [ m ]) ∘i m') .ihom   β‰‘βŸ¨ ap ihom (pullri (Internal-hom-path (ap ihom p))) βŸ©β‰‘
    (invi [ m ] ∘i adjusti _ _ h') .ihom    ∎

The reverse direction also mirrors the corresponding construction for the family fibration: we use the same trick of factoring the identity morphism.

cartesian→internal-iso
  : βˆ€ {Ξ“ Ξ” : Ob} {u : Hom Ξ“ Ξ”} {x : Hom Ξ“ Cβ‚€} {y : Hom Ξ” Cβ‚€}
  β†’ (f : Homi x (y ∘ u))
  β†’ is-cartesian Externalise u f
  β†’ is-invertiblei f
cartesian→internal-iso {Γ} {Δ} {u} {x} {y} f f-cart = f-inv where
  open is-cartesian f-cart
  open is-invertiblei
  open Inversesi
  open Externalisation

  f-inv : is-invertiblei f
  f-inv .invi =
    adjusti (ap (y ∘_) (idr u)) (idr x) (universal id (idi _))
  f-inv .inversesi .invli =
    Internal-hom-path $
      (f ∘i f-inv .invi) .ihom                 β‰‘βŸ¨ ∘i-ihom (ap (_ ∘_) (sym (idr _))) (sym (idr _)) (sym (idr _)) (sym (idr _)) refl βŸ©β‰‘
      (f [ id ] ∘i universal id (idi _)) .ihom β‰‘βŸ¨ ap ihom (commutes id (idi _)) βŸ©β‰‘
      idi (y ∘ ⌜ u ∘ id ⌝) .ihom               β‰‘βŸ¨ ap! (idr _) βŸ©β‰‘
      idi (y ∘ u) .ihom ∎
  f-inv .inversesi .invri =
    Internal-hom-path $
      (f-inv .invi ∘i f) .ihom               β‰‘βŸ¨ ∘i-ihom refl refl (sym (idr _)) refl refl βŸ©β‰‘
      (adjusti _ _ (f-inv .invi) ∘i f) .ihom β‰‘βŸ¨ ap ihom (unique (adjusti refl (sym (idr _)) (f-inv .invi) ∘i f) f∘f⁻¹∘f≑f*) βŸ©β‰‘
      universal id (adjusti _ _ f) .ihom     β‰‘Λ˜βŸ¨ ap ihom (unique (adjusti refl (sym (idr _)) (idi _)) f∘id≑f*) βŸ©β‰‘Λ˜
      idi x .ihom ∎
The right inverse case needs some nightmare re-adjustments. Unfold this at your own risk!
    where
      f∘f⁻¹∘f≑f*
        : adjusti _ _ (f [ id ] ∘i adjusti _ _ (f-inv .invi) ∘i f)
        ≑ adjusti refl (ap (_ ∘_) (sym (idr _))) f
      f∘f⁻¹∘f≑f* = Internal-hom-path $
        (f [ id ] ∘i adjusti _ _ (f-inv .invi) ∘i f) .ihom
          β‰‘βŸ¨ ap ihom (associ _ _ _) βŸ©β‰‘
        ((f [ id ] ∘i adjusti _ _ (f-inv .invi)) ∘i f) .ihom
          β‰‘βŸ¨ ∘i-ihom refl (ap (y ∘_) (sym (idr _))) (sym (assoc _ _ _)) (∘i-ihom (ap (y ∘_) (sym (idr _))) refl refl refl refl) refl βŸ©β‰‘
        (adjusti refl (sym (assoc _ _ _)) (f [ id ] ∘i universal id (idi _)) ∘i adjusti refl (ap (y ∘_) (sym (idr _))) f) .ihom
          β‰‘βŸ¨ ∘i-ihom refl refl refl (ap ihom (commutes id (idi _))) refl βŸ©β‰‘
        (idi _ ∘i adjusti refl (ap (y ∘_) (sym (idr _))) f) .ihom β‰‘βŸ¨ ap ihom (idli _) βŸ©β‰‘
        f .ihom                                                                       ∎
      f∘id≑f* : adjusti _ _ (f [ id ] ∘i adjusti _ _ (idi x)) ≑ adjusti _ _ f
      f∘id≑f* = Internal-hom-path $
        (f [ id ] ∘i adjusti _ _ (idi x)) .ihom β‰‘βŸ¨ ∘i-ihom refl (idr _) (idr _) (idr _) refl βŸ©β‰‘
        (f ∘i idi _) .ihom                      β‰‘βŸ¨ ap ihom (idri _) βŸ©β‰‘
        f .ihom ∎

Finally, we show that the externalisation is a fibration. As per usual, the argument proceeds in the same manner as for the family fibration. Given a generalized object and a morphism we can take the pullback of to be the lift of is then simply the (internal) identity morphism.

Externalisation-fibration : Cartesian-fibration Externalise
Externalisation-fibration .Cartesian-fibration.has-lift u y = cart-lift where
  open Cartesian-lift

  cart-lift : Cartesian-lift Externalise u y
  cart-lift .x' = y ∘ u
  cart-lift .lifting = idi _
  cart-lift .cartesian .is-cartesian.universal m h' =
    adjusti refl (assoc _ _ _) h'
  cart-lift .cartesian .is-cartesian.commutes m h' =
    Internal-hom-path $
      (⌜ idi _ [ m ] ⌝ ∘i _) .ihom β‰‘βŸ¨ ap! (idi-nat m) βŸ©β‰‘
      (idi _ ∘i _) .ihom           β‰‘βŸ¨ ap ihom (idli _) βŸ©β‰‘
      h' .ihom ∎
  cart-lift .cartesian .is-cartesian.unique {m = m} {h' = h'} m' p =
    Internal-hom-path $
      m' .ihom                  β‰‘Λ˜βŸ¨ ap ihom (idli _) βŸ©β‰‘Λ˜
      (⌜ idi _ ⌝ ∘i m') .ihom   β‰‘βŸ¨ ap! (sym (idi-nat m)) βŸ©β‰‘
      (idi _ [ m ] ∘i m') .ihom β‰‘βŸ¨ ap ihom p βŸ©β‰‘
      h' .ihom                  ∎

Generic objectsπŸ”—

The externalisation is always globally small. We shall use the object of objects as the base for our generic object, and the identity morphism as the upstairs portion. Classifying maps in the base are given by interpreting using a object in the externalisation as a morphism in the base, and the displayed classifying map is the internal identity morphism, which is always cartesian.

Externalisation-globally-small : Globally-small Externalise
Externalisation-globally-small = small where
  open Globally-small
  open Generic-object
  open is-cartesian

  small : Globally-small Externalise
  small .U = Cβ‚€
  small .Gen = id
  small .has-generic-ob .classify x = x
  small .has-generic-ob .classify' x =
    adjusti refl (sym (idl _)) (idi _)
However, showing the internal identity morphism needs to be transported around a bit, so showing that it is cartesian requires some tedious calculations.
  small .has-generic-ob .classify-cartesian x' .universal m h' =
    adjusti refl (idl _) h'
  small .has-generic-ob .classify-cartesian x' .commutes m h' =
    Internal-hom-path $
      ∘i-ihom refl
        (sym (idl _))
        (sym (assoc _ _ _))
        (ap ihom (idi-nat _) βˆ™ ap (Ξ» Ο• β†’ idi Ο• .ihom) (sym (idl _)))
        refl
      βˆ™ ap ihom (idli h')
  small .has-generic-ob .classify-cartesian x' .unique {m = m} m' p =
    Internal-hom-path $
      sym (ap ihom (idli m'))
      ·· ∘i-ihom refl refl (ap (_∘ m) (sym (idl _))) (sym (ap ihom (idi-nat m))) refl
      Β·Β· ap ihom p