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 Yβ†’FX←GZ\ca{Y} \xto{F} \ca{X} \xot{G} \ca{Z} be a cospan of functors between three univalent categories. Then the comma category F↓GF \downarrow G is also univalent.

It suffices to establish that, given an isomorphism f:oβ‰…oβ€²f : o \cong o' in F↓GF \downarrow G, one gets an identification fΛ†:o≑oβ€²\^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Λ†Ξ±:ox≑oxβ€²\^f_\alpha : o_x \equiv o'_x and fΛ†Ξ²:oy≑oyβ€²\^f_\beta : o_y \equiv o'_y.

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.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 omβ€²o'_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)=omβ€²F1(fΞ±)F1(fΞ±βˆ’1)=omβ€²F1(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 o≑oβ€²o \equiv o'.

    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 F x-is-x yuniv xuniv (~ i) j)
                                  (F-map-path G y-is-y zuniv xuniv (~ i) j))
                    (ob .map) (obβ€² .map)) $
        Univalent.Hom-pathp-iso 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 _ _ (Univalent.Hom-pathp-reflr-iso yuniv (Y.idr _))
                      (Univalent.Hom-pathp-reflr-iso zuniv (Z.idr _)))