module Cat.Functor.Kan.Unique where
Uniqueness of Kan extensionsπ
Kan extensions (both left and right) are universal constructions, so they are unique when they exist. To get a theorem out of this intuition, we must be careful about how the structure and the properties are separated: Informally, we refer to the functor as βthe Kan extensionβ, but in reality, the data associated with βthe Kan extension of along β also includes the natural transformation. For accuracy, using the setup from the diagram below, we should say β is the Kan extension of along β.
private variable o β : Level C Cβ² D : Precategory o β module Lan-unique {p : Functor C Cβ²} {F : Functor C D} {Gβ Gβ : Functor Cβ² D} {Ξ·β Ξ·β} (lβ : is-lan p F Gβ Ξ·β) (lβ : is-lan p F Gβ Ξ·β) where private module lβ = is-lan lβ module lβ = is-lan lβ module D = Cat.Reasoning D module Cβ²D = Cat.Reasoning Cat[ Cβ² , D ] open Cβ²D._β _ open Cβ²D.Inverses
To show uniqueness, suppose that and and both left extensions of along . Diagramming this with both natural transformations shown is a bit of a nightmare: the option which doesnβt result in awful crossed arrows is to duplicate the span . So, to be clear: The upper triangle and the lower triangle are the same.
Recall that being a left extension means we can (uniquely) factor natural transformations through transformations . We want a map , for which it will suffice to find a map β but is right there! In the other direction, we can factor to get a map . Since these factorisations are unique, we have a natural isomorphism.
Ο-inversesp : β {Ξ± : Gβ => Gβ} {Ξ² : Gβ => Gβ} β (Ξ± β p) βnt Ξ·β β‘ Ξ·β β (Ξ² β p) βnt Ξ·β β‘ Ξ·β β natural-inverses Ξ± Ξ² Ο-inversesp Ξ±-factor Ξ²-factor = Cβ²D.make-inverses (lβ.Ο-uniqβ Ξ·β (Nat-path Ξ» j β sym (D.pullr (Ξ²-factor Ξ·β j) β Ξ±-factor Ξ·β j)) (Nat-path Ξ» j β sym (D.idl _))) (lβ.Ο-uniqβ Ξ·β (Nat-path Ξ» j β sym (D.pullr (Ξ±-factor Ξ·β j) β Ξ²-factor Ξ·β j)) (Nat-path Ξ» j β sym (D.idl _)))
Ο-is-invertiblep : β {Ξ± : Gβ => Gβ} β (Ξ± β p) βnt Ξ·β β‘ Ξ·β β is-natural-invertible Ξ± Ο-is-invertiblep {Ξ± = Ξ±} Ξ±-factor = Cβ²D.inversesβinvertible (Ο-inversesp {Ξ±} Ξ±-factor lβ.Ο-comm) Ο-inverses : natural-inverses (lβ.Ο Ξ·β) (lβ.Ο Ξ·β) Ο-inverses = Ο-inversesp lβ.Ο-comm lβ.Ο-comm Ο-is-invertible : is-natural-invertible (lβ.Ο Ξ·β) Ο-is-invertible = Ο-is-invertiblep lβ.Ο-comm unique : natural-iso Gβ Gβ unique = Cβ²D.invertibleβiso (lβ.Ο Ξ·β) (Ο-is-invertiblep lβ.Ο-comm)
Itβs immediate from the construction that this isomorphism βsends to β.
unit : (lβ.Ο Ξ·β β p) βnt Ξ·β β‘ Ξ·β unit = lβ.Ο-comm
module _ {p : Functor C Cβ²} {F : Functor C D} {G : Functor Cβ² D} {eta} (lan : is-lan p F G eta) where private module lan = is-lan lan module D = Cat.Reasoning D module Cβ²D = Cat.Reasoning Cat[ Cβ² , D ] open _=>_
Another uniqueness-like result we can state for left extensions is the following: Given any functor and candidate βunitβ transformation , if a left extension sends to a natural isomorphism, then is also a left extension of along .
is-invertibleβis-lan : β {G' : Functor Cβ² D} {eta' : F => G' Fβ p} β is-natural-invertible (lan.Ο eta') β is-lan p F G' eta' is-invertibleβis-lan {G' = G'} {eta'} invert = lan' where open is-lan open Cβ²D.is-invertible invert lan' : is-lan p F G' eta' lan' .Ο Ξ± = lan.Ο Ξ± βnt inv lan' .Ο-comm {M} {Ξ±} = Nat-path Ξ» j β (lan.Ο Ξ± .Ξ· _ D.β inv .Ξ· _) D.β eta' .Ξ· j β‘Λβ¨ D.reflβ©ββ¨ (lan.Ο-comm Ξ·β _) β©β‘Λ (lan.Ο Ξ± .Ξ· _ D.β inv .Ξ· _) D.β (lan.Ο eta' .Ξ· _ D.β eta .Ξ· j) β‘β¨ D.cancel-inner (invr Ξ·β _) β©β‘ lan.Ο Ξ± .Ξ· _ D.β eta .Ξ· j β‘β¨ lan.Ο-comm Ξ·β _ β©β‘ Ξ± .Ξ· j β lan' .Ο-uniq {M} {Ξ±} {Οβ²} p = Nat-path Ξ» j β lan.Ο Ξ± .Ξ· j D.β inv .Ξ· j β‘β¨ (lan.Ο-uniq {Οβ² = Οβ² βnt lan.Ο eta'} (Nat-path Ξ» j β p Ξ·β j β D.pushr (sym (lan.Ο-comm Ξ·β j))) Ξ·β j) D.β©ββ¨refl β©β‘ (Οβ² .Ξ· j D.β lan.Ο eta' .Ξ· j) D.β inv .Ξ· _ β‘β¨ D.cancelr (invl Ξ·β _) β©β‘ Οβ² .Ξ· j β
natural-iso-ofβis-lan : {F' : Functor C D} β (isos : natural-iso F F') β is-lan p F' G (eta βnt natural-iso.from isos) natural-iso-ofβis-lan {F' = F'} isos = lan' where open is-lan module isos = natural-iso isos lan' : is-lan p F' G (eta βnt isos.from) lan' .Ο Ξ± = lan.Ο (Ξ± βnt isos.to) lan' .Ο-comm {M} {Ξ±} = Nat-path Ξ» j β lan.Ο (Ξ± βnt isos.to) .Ξ· _ D.β eta .Ξ· j D.β isos.from .Ξ· j β‘β¨ D.pulll (lan.Ο-comm Ξ·β j) β©β‘ (Ξ± .Ξ· j D.β isos.to .Ξ· j) D.β isos.from .Ξ· j β‘β¨ D.cancelr (isos.invl Ξ·β _) β©β‘ Ξ± .Ξ· j β lan' .Ο-uniq {M} {Ξ±} {Οβ²} p = lan.Ο-uniq $ Nat-path Ξ» j β Ξ± .Ξ· j D.β isos.to .Ξ· j β‘β¨ (p Ξ·β j) D.β©ββ¨refl β©β‘ (Οβ² .Ξ· _ D.β eta .Ξ· j D.β isos.from .Ξ· j) D.β isos.to .Ξ· j β‘β¨ D.deleter (isos.invr Ξ·β _) β©β‘ Οβ² .Ξ· _ D.β eta .Ξ· j β natural-iso-extβis-lan : {G' : Functor Cβ² D} β (isos : natural-iso G G') β is-lan p F G' ((natural-iso.to isos β p) βnt eta) natural-iso-extβis-lan {G' = G'} isos = lan' where open is-lan module isos = natural-iso isos lan' : is-lan p F G' ((isos.to β p) βnt eta) lan' .Ο Ξ± = lan.Ο Ξ± βnt isos.from lan' .Ο-comm {M} {Ξ±} = Nat-path Ξ» j β (lan.Ο Ξ± .Ξ· _ D.β isos.from .Ξ· _) D.β isos.to .Ξ· _ D.β eta .Ξ· j β‘β¨ D.cancel-inner (isos.invr Ξ·β _) β©β‘ lan.Ο Ξ± .Ξ· _ D.β eta .Ξ· j β‘β¨ lan.Ο-comm Ξ·β _ β©β‘ Ξ± .Ξ· j β lan' .Ο-uniq {M} {Ξ±} {Οβ²} p = Nat-path Ξ» j β lan.Ο Ξ± .Ξ· j D.β isos.from .Ξ· j β‘β¨ D.pushl (lan.Ο-uniq {Οβ² = Οβ² βnt isos.to} (Nat-path Ξ» j β p Ξ·β j β D.assoc _ _ _) Ξ·β j) β©β‘ Οβ² .Ξ· j D.β isos.to .Ξ· j D.β isos.from .Ξ· j β‘β¨ D.elimr (isos.invl Ξ·β _) β©β‘ Οβ² .Ξ· j β natural-iso-alongβis-lan : {p' : Functor C Cβ²} β (isos : natural-iso p p') β is-lan p' F G ((G βΈ natural-iso.to isos) βnt eta) natural-iso-alongβis-lan {p'} isos = lan' where open is-lan module isos = natural-iso isos open Cat.Functor.Reasoning lan' : is-lan p' F G ((G βΈ natural-iso.to isos) βnt eta) lan' .Ο {M} Ξ± = lan.Ο ((M βΈ isos.from) βnt Ξ±) lan' .Ο-comm {M = M} = Nat-path Ξ» j β D.pulll ((lan.Ο _ .is-natural _ _ _)) β D.pullr (lan.Ο-comm Ξ·β _) β cancell M (isos.invl Ξ·β _) lan' .Ο-uniq {M = M} {Ξ± = Ξ±} {Οβ² = Οβ²} q = Nat-path Ξ» c' β lan.Ο-uniq {Ξ± = (M βΈ isos.from) βnt Ξ±} {Οβ² = Οβ²} (Nat-path Ξ» j β D.pushr (q Ξ·β _) β D.pulll (D.pullr (Οβ² .is-natural _ _ _) β cancell M (isos.invr Ξ·β _))) Ξ·β c' universal-pathβis-lan : β {eta'} β eta β‘ eta' β is-lan p F G eta' universal-pathβis-lan {eta'} q = lan' where open is-lan lan' : is-lan p F G eta' lan' .Ο = lan.Ο lan' .Ο-comm = ap (_ βnt_) (sym q) β lan.Ο-comm lan' .Ο-uniq r = lan.Ο-uniq (r β ap (_ βnt_) (sym q)) module _ {p p' : Functor C Cβ²} {F F' : Functor C D} {G G' : Functor Cβ² D} {eps eps'} where private module D = Cat.Reasoning D open Cat.Functor.Reasoning open _=>_
Left Kan extensions are also invariant under arbitrary natural isomorphisms. To get better definitional control, we allow βadjustingβ the resulting construction to talk about any natural transformation which is propositionally equal to the whiskering:
natural-isosβis-lan : (p-iso : natural-iso p p') β (F-iso : natural-iso F F') β (G-iso : natural-iso G G') β (natural-iso.to G-iso β natural-iso.to p-iso) βnt eps βnt natural-iso.from F-iso β‘ eps' β is-lan p F G eps β is-lan p' F' G' eps'
natural-isosβis-lan p-iso F-iso G-iso q lan = universal-pathβis-lan (natural-iso-extβis-lan (natural-iso-ofβis-lan (natural-iso-alongβis-lan lan p-iso) F-iso) G-iso) (Nat-path Ξ» x β D.extendl (D.pulll (G-iso .to .is-natural _ _ _)) β q Ξ·β _) where open natural-iso
Into univalent categoriesπ
As traditional with universal constructions, if takes values in a univalent category, we can sharpen our result: the type of left extensions of along is a proposition.
Lan-is-prop : β {p : Functor C Cβ²} {F : Functor C D} β is-category D β is-prop (Lan p F) Lan-is-prop {C = C} {Cβ² = Cβ²} {D = D} {p = p} {F = F} d-cat Lβ Lβ = path where
module Lβ = Lan Lβ module Lβ = Lan Lβ module Lu = Lan-unique Lβ.has-lan Lβ.has-lan open Lan cβ²d-cat : is-category Cat[ Cβ² , D ] cβ²d-cat = Functor-is-category d-cat
Thatβs because if is univalent, then so is , so our natural isomorphism is equivalent to an identification . Then, our tiny lemma stating that this isomorphism βsends to β is precisely the data of a dependent identification over .
functor-path : Lβ.Ext β‘ Lβ.Ext functor-path = cβ²d-cat .to-path Lu.unique eta-path : PathP (Ξ» i β F => functor-path i Fβ p) Lβ.eta Lβ.eta eta-path = Nat-pathp _ _ Ξ» x β Univalent.Hom-pathp-reflr-iso d-cat (Lu.unit Ξ·β _)
Since being a left extension is always a proposition when applied to , even when the categories are not univalent, we can finish our proof.
path : Lβ β‘ Lβ path i .Ext = functor-path i path i .eta = eta-path i path i .has-lan = is-propβpathp (Ξ» i β is-lan-is-prop {p = p} {F} {functor-path i} {eta-path i}) Lβ.has-lan Lβ.has-lan i
module Ran-unique {p : Functor C Cβ²} {F : Functor C D} {Gβ Gβ : Functor Cβ² D} {Ξ΅β Ξ΅β} (rβ : is-ran p F Gβ Ξ΅β) (rβ : is-ran p F Gβ Ξ΅β) where private module rβ = is-ran rβ module rβ = is-ran rβ module D = Cat.Reasoning D module Cβ²D = Cat.Reasoning Cat[ Cβ² , D ] open Cβ²D._β _ open Cβ²D.Inverses Ο-inversesp : β {Ξ± : Gβ => Gβ} {Ξ² : Gβ => Gβ} β (Ξ΅β βnt (Ξ± β p)) β‘ Ξ΅β β (Ξ΅β βnt (Ξ² β p)) β‘ Ξ΅β β natural-inverses Ξ± Ξ² Ο-inversesp Ξ±-factor Ξ²-factor = Cβ²D.make-inverses (rβ.Ο-uniqβ Ξ΅β (Nat-path Ξ» j β sym (D.pulll (Ξ±-factor Ξ·β j) β Ξ²-factor Ξ·β j)) (Nat-path Ξ» j β sym (D.idr _))) (rβ.Ο-uniqβ Ξ΅β (Nat-path Ξ» j β sym (D.pulll (Ξ²-factor Ξ·β j) β Ξ±-factor Ξ·β j)) (Nat-path Ξ» j β sym (D.idr _))) Ο-is-invertiblep : β {Ξ± : Gβ => Gβ} β (Ξ΅β βnt (Ξ± β p)) β‘ Ξ΅β β is-natural-invertible Ξ± Ο-is-invertiblep {Ξ±} Ξ±-factor = Cβ²D.inversesβinvertible (Ο-inversesp {Ξ±} Ξ±-factor rβ.Ο-comm) Ο-inverses : natural-inverses (rβ.Ο Ξ΅β) (rβ.Ο Ξ΅β) Ο-inverses = Ο-inversesp rβ.Ο-comm rβ.Ο-comm Ο-is-invertible : is-natural-invertible (rβ.Ο Ξ΅β) Ο-is-invertible = Ο-is-invertiblep rβ.Ο-comm unique : natural-iso Gβ Gβ unique = Cβ²D.invertibleβiso (rβ.Ο Ξ΅β) (Ο-is-invertiblep rβ.Ο-comm) niβ»ΒΉ counit : Ξ΅β βnt (rβ.Ο Ξ΅β β p) β‘ Ξ΅β counit = rβ.Ο-comm module _ {p : Functor C Cβ²} {F : Functor C D} {G : Functor Cβ² D} {eps} (ran : is-ran p F G eps) where private module ran = is-ran ran module D = Cat.Reasoning D module Cβ²D = Cat.Reasoning Cat[ Cβ² , D ] open _=>_ -- These are more annoying to do via duality then it is to do by hand, -- due to the natural isos. is-invertibleβis-ran : β {G' : Functor Cβ² D} {eps'} β is-natural-invertible (ran.Ο eps') β is-ran p F G' eps' is-invertibleβis-ran {G' = G'} {eps'} invert = ran' where open is-ran open Cβ²D.is-invertible invert ran' : is-ran p F G' eps' ran' .Ο Ξ² = inv βnt ran.Ο Ξ² ran' .Ο-comm {M} {Ξ²} = Nat-path Ξ» j β sym ((ran.Ο-comm Ξ·β _) D.β©ββ¨refl) Β·Β· D.cancel-inner (invl Ξ·β _) Β·Β· (ran.Ο-comm Ξ·β _) ran' .Ο-uniq {M} {Ξ²} {Οβ²} p = Nat-path Ξ» j β (D.reflβ©ββ¨ ran.Ο-uniq {Οβ² = ran.Ο eps' βnt Οβ²} (Nat-path Ξ» j β p Ξ·β j β D.pushl (sym (ran.Ο-comm Ξ·β j))) Ξ·β _) β D.cancell (invr Ξ·β _) natural-iso-ofβis-ran : {F' : Functor C D} β (isos : natural-iso F F') β is-ran p F' G (natural-iso.to isos βnt eps) natural-iso-ofβis-ran {F'} isos = ran' where open is-ran module isos = natural-iso isos ran' : is-ran p F' G (isos.to βnt eps) ran' .Ο Ξ² = ran.Ο (isos.from βnt Ξ²) ran' .Ο-comm {M} {Ξ²} = Nat-path Ξ» j β D.pullr (ran.Ο-comm Ξ·β j) β D.cancell (isos.invl Ξ·β _) ran' .Ο-uniq {M} {Ξ²} {Οβ²} p = ran.Ο-uniq $ Nat-path Ξ» j β (D.reflβ©ββ¨ p Ξ·β j) β D.deletel (isos.invr Ξ·β _) natural-iso-extβis-ran : {G' : Functor Cβ² D} β (isos : natural-iso G G') β is-ran p F G' (eps βnt (natural-iso.from isos β p)) natural-iso-extβis-ran {G'} isos = ran' where open is-ran module isos = natural-iso isos ran' : is-ran p F G' (eps βnt (isos.from β p)) ran' .Ο Ξ² = isos.to βnt ran.Ο Ξ² ran' .Ο-comm {M} {Ξ²} = Nat-path Ξ» j β D.cancel-inner (isos.invr Ξ·β _) β ran.Ο-comm Ξ·β _ ran' .Ο-uniq {M} {Ξ²} {Οβ²} p = Nat-path Ξ» j β D.pushr (ran.Ο-uniq {Οβ² = isos.from βnt Οβ²} (Nat-path Ξ» j β p Ξ·β j β sym (D.assoc _ _ _)) Ξ·β j) β D.eliml (isos.invl Ξ·β _) natural-iso-alongβis-ran : {p' : Functor C Cβ²} β (isos : natural-iso p p') β is-ran p' F G (eps βnt (G βΈ natural-iso.from isos)) natural-iso-alongβis-ran {p'} isos = ran' where open is-ran module isos = natural-iso isos open Cat.Functor.Reasoning ran' : is-ran p' F G (eps βnt (G βΈ natural-iso.from isos)) ran' .Ο {M} Ξ² = ran.Ο (Ξ² βnt (M βΈ natural-iso.to isos)) ran' .Ο-comm {M = M} = Nat-path Ξ» j β D.pullr (sym (ran.Ο _ .is-natural _ _ _)) β D.pulll (ran.Ο-comm Ξ·β _) β cancelr M (isos.invl Ξ·β _) ran' .Ο-uniq {M = M} {Ξ² = Ξ²} {Οβ² = Οβ²} q = Nat-path Ξ» c' β ran.Ο-uniq {Ξ² = Ξ² βnt (M βΈ isos.to)} {Οβ² = Οβ²} (Nat-path Ξ» j β D.pushl (q Ξ·β _) β D.pullr (D.pulll (sym (Οβ² .is-natural _ _ _)) β cancelr M (isos.invr Ξ·β _))) Ξ·β c' universal-pathβis-ran : β {eps'} β eps β‘ eps' β is-ran p F G eps' universal-pathβis-ran {eps'} q = ran' where open is-ran ran' : is-ran p F G eps' ran' .Ο = ran.Ο ran' .Ο-comm = ap (_βnt _) (sym q) β ran.Ο-comm ran' .Ο-uniq r = ran.Ο-uniq (r β ap (_βnt _) (sym q)) module _ {p p' : Functor C Cβ²} {F F' : Functor C D} {G G' : Functor Cβ² D} {eps eps'} where private module D = Cat.Reasoning D open _=>_ natural-isosβis-ran : (p-iso : natural-iso p p') β (F-iso : natural-iso F F') β (G-iso : natural-iso G G') β (natural-iso.to F-iso βnt eps βnt (natural-iso.from G-iso β natural-iso.from p-iso)) β‘ eps' β is-ran p F G eps β is-ran p' F' G' eps' natural-isosβis-ran p-iso F-iso G-iso p ran = universal-pathβis-ran (natural-iso-extβis-ran (natural-iso-ofβis-ran (natural-iso-alongβis-ran ran p-iso) F-iso) G-iso) (Nat-path Ξ» c β sym (D.assoc _ _ _) Β·Β· apβ D._β_ refl (sym $ D.assoc _ _ _) Β·Β· p Ξ·β _) Ran-is-prop : β {p : Functor C Cβ²} {F : Functor C D} β is-category D β is-prop (Ran p F) Ran-is-prop {C = C} {Cβ² = Cβ²} {D = D} {p = p} {F = F} d-cat Rβ Rβ = path where module Rβ = Ran Rβ module Rβ = Ran Rβ module Ru = Ran-unique Rβ.has-ran Rβ.has-ran open Ran cβ²d-cat : is-category Cat[ Cβ² , D ] cβ²d-cat = Functor-is-category d-cat fp : Rβ.Ext β‘ Rβ.Ext fp = cβ²d-cat .to-path Ru.unique Ξ΅p : PathP (Ξ» i β fp i Fβ p => F) Rβ.eps Rβ.eps Ξ΅p = Nat-pathp _ _ Ξ» x β Univalent.Hom-pathp-refll-iso d-cat (Ru.counit Ξ·β _) path : Rβ β‘ Rβ path i .Ext = fp i path i .eps = Ξ΅p i path i .has-ran = is-propβpathp (Ξ» i β is-ran-is-prop {p = p} {F} {fp i} {Ξ΅p i}) Rβ.has-ran Rβ.has-ran i