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

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

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

private
module X = Cat.Reasoning X
module Y = Cat.Reasoning Y
module Z = Cat.Reasoning Z
module F = Func F
module G = Func G
module FβG = Cat.Reasoning (F β G)

open βObj
open βHom


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 F yuniv xuniv x-is-x (~ i) j)
(F-map-path G zuniv xuniv 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 _)))