open import Cat.Instances.Comma
open import Cat.Functor.Base
open import Cat.Univalent
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning

  {xo xℓ yo yℓ zo zℓ}
  {X : Precategory xo xℓ} {Y : Precategory yo yℓ} {Z : Precategory zo zℓ}
  (F : Functor Y X) (G : Functor Z X)
  (xuniv : is-category X)
  (yuniv : is-category Y)
  (zuniv : is-category Z)

Comma categories preserve univalence🔗

Theorem. Let YFXGZ\ca{Y} \xto{F} \ca{X} \xot{G} \ca{Z} be a cospan of functors between three univalent categories. Then the comma category FGF \downarrow G is also univalent.

It suffices to establish that, given an isomorphism f:oof : o \cong o' in FGF \downarrow G, one gets an identification fˆ:oo\^f : o \equiv o', over which ff is the identity map. Since Y\ca{Y} and Z\ca{Z} are both univalent categories, we get (from the components fαf_\alpha, fβf_\beta of ff) identifications fˆα:oxox\^f_\alpha : o_x \equiv o'_x and fˆβ:oyoy\^f_\beta : o_y \equiv o'_y.

Comma-is-category : is-category (F  G)
Comma-is-category ob .centre = ob , F↓
Comma-is-category ob .paths (ob′ , isom) = Σ-pathp objs maps where
  module isom = F↓G._≅_ isom

  x-is-x : ob .x Y.≅ ob′ .x
  y-is-y : ob .y Z.≅ ob′ .y

  x-is-x = Y.make-iso ( .α) (isom.from .α) (ap α isom.invl) (ap α isom.invr)
  y-is-y = Z.make-iso ( .β) (isom.from .β) (ap β isom.invl) (ap β isom.invr)

Observe that, over fˆα\^f_\alpha and fˆβ\^f_\beta, the map components omo_m and omo'_m are equal (we say “equal” rather than “identified” because Hom-sets are sets). This follows by standard abstract nonsense: in particular, functors between univalent categories respect isomorphisms in a strong sense (F-map-path).

This lets us reduce statements about FF and GG’s object-part action on paths to statements about their morphism parts F1F_1, G1G_1 on the components of the isomorphisms fαf_\alpha and fβf_\beta. But then we have

G1(fβ)omF1(fα1)=omF1(fα)F1(fα1)=omF1(fαfα1)=om, \begin{split} G_1(f_\beta) o_m F_1(f_\alpha^{-1}) &= o'_m F_1(f_\alpha) F_1(f_\alpha^{-1}) \\ &= o'_m F_1(f_\alpha f_\alpha^{-1}) \\ &= o'_m\text{,} \end{split}

so over these isomorphisms the map parts become equal, thus establishing an identification ooo \equiv o'.

  objs : ob  ob′
  objs i .x = iso→path Y yuniv x-is-x i
  objs i .y = iso→path Z zuniv y-is-y i
  objs i .map = lemma′ i where
    lemma′ : PathP  i  X.Hom (F.₀ (objs i .x)) (G.₀ (objs i .y)))
              (ob .map) (ob′ .map)
    lemma′ = transport
       i  PathP  j  X.Hom (F-map-path F x-is-x yuniv xuniv (~ i) j)
                                (F-map-path G y-is-y zuniv xuniv (~ i) j))
                   (ob .map) (ob′ .map)) $
      Hom-pathp-iso X xuniv $
        X.pulll   (sym ( .sq)) 
        X.cancelr (F.annihilate (ap α isom.invl))

It still remains to show that, over this identification, the isomorphism ff is equal to the identity function. But this is simply a matter of pushing the identifications down to reach the “leaf” morphisms.

  maps : PathP  i  ob F↓G.≅ objs i) _ isom
  maps = F↓G.≅-pathp _ _
    (↓Hom-pathp _ _ (Hom-pathp-reflr-iso Y yuniv (Y.idr _))
                    (Hom-pathp-reflr-iso Z zuniv (Z.idr _)))