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 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 ob .centre = ob , FβG.id-iso 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.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 βs 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 = 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 (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 _ _ (Hom-pathp-reflr-iso Y yuniv (Y.idr _)) (Hom-pathp-reflr-iso Z zuniv (Z.idr _)))