module
  Cat.Instances.Comma.Univalent
  {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)
  where

Comma categories preserve univalenceπŸ”—

Theorem. Let be a cospan of functors between three univalent categories. Then the comma category is also univalent.

It suffices to establish that, given an isomorphism in one gets an identification over which is the identity map. Since and are both univalent categories, we get (from the components of identifications and

Comma-is-category : is-category (F ↓ G)
Comma-is-category = record { to-path = objs ; to-path-over = maps } where
  module _ {ob ob'} (isom : F↓G.Isomorphism ob ob') 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.to .Ξ±) (isom.from .Ξ±) (ap Ξ± isom.invl) (ap Ξ± isom.invr)
    y-is-y = Z.make-iso (isom.to .Ξ²) (isom.from .Ξ²) (ap Ξ² isom.invl) (ap Ξ² isom.invr)

Observe that, over and the map components and 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 and object-part action on paths to statements about their morphism parts on the components of the isomorphisms and But then we have

so over these isomorphisms the map parts become equal, thus establishing an identification

    objs : ob ≑ ob'
    objs i .x = yuniv .to-path x-is-x i
    objs i .y = zuniv .to-path 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 yuniv xuniv F x-is-x (~ i) j)
                                  (F-map-path zuniv xuniv G y-is-y (~ i) j))
                    (ob .map) (ob' .map)) $
        Univalent.Hom-pathp-iso xuniv $
          X.pulll   (sym (isom.to .sq)) βˆ™
          X.cancelr (F.annihilate (ap Ξ± isom.invl))

It still remains to show that, over this identification, the isomorphism 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 _ _ (Univalent.Hom-pathp-reflr-iso yuniv (Y.idr _))
                      (Univalent.Hom-pathp-reflr-iso zuniv (Z.idr _)))