open import Cat.Instances.Functor.Compose open import Cat.Instances.Functor open import Cat.Functor.Base open import Cat.Functor.Kan open import Cat.Prelude import Cat.Reasoning module Cat.Functor.Kan.Unique
Uniqueness of Kan extensionsπ
Since (left) Kan extensions are defined by a universal property (they are partial values of a specific adjunction), they are unique: When is a category, then the type of left Kan extensions of along is a proposition.
Lan-is-prop : is-prop (Lan p F) Lan-is-prop Lβ Lβ = Lan-unique module Lan-unique where
We diagram the situation generically as follows: and are fixed, with and being both left extensions of along . The functor (resp. ) is equipped with a natural transformation (resp. ), and if is equipped with , then can cough up a unique natural transformation (resp. ) making everything in sight commute.
The isomorphism is constructed as follows: Since is equipped with , can produce ; Since is equipped with , can produce . To show is the identity, note that both make βeverything in sight commuteβ, so they inhabit a contractible space since is an extension. The argument for is analogous.
Ext-unique : [Cβ²,D].Isomorphism Lβ.Ext Lβ.Ext Ext-unique = [Cβ²,D].make-iso (Lβ.Ο Lβ.eta) (Lβ.Ο Lβ.eta) ( sym (Lβ.Ο-uniq {Ξ± = Lβ.eta} (Nat-path Ξ» _ β sym ( D.pullr (Lβ.Ο-comm Ξ·β _) β Lβ.Ο-comm Ξ·β _))) β Lβ.Ο-uniq (Nat-path Ξ» _ β D.introl refl)) ( sym (Lβ.Ο-uniq {Ξ± = Lβ.eta} (Nat-path Ξ» _ β sym ( D.pullr (Lβ.Ο-comm Ξ·β _) β Lβ.Ο-comm Ξ·β _))) β Lβ.Ο-uniq (Nat-path Ξ» _ β D.introl refl)) Ext-uniqueβ : Lβ.Ext β‘ Lβ.Ext Ext-uniqueβ = cd-cat .to-path Ext-unique
The functor is not the only data associated with a left extension, though: we must also verify that, under the identification we just produced, the natural transformations and are also identified. This boils down to verifying, in components, that , but that is immediate by the specification for .
eta-uniqueβ : PathP (Ξ» i β F => Ext-uniqueβ i Fβ p) Lβ.eta Lβ.eta eta-uniqueβ = Nat-pathp refl _ Ξ» _ β Univalent.Hom-pathp-reflr-iso dcat (Lβ.Ο-comm Ξ·β _)
A similar argument shows that and are also identified.
Ο-uniqueβ : β {M} (f : F => M Fβ p) β PathP (Ξ» i β Ext-uniqueβ i => M) (Lβ.Ο f) (Lβ.Ο f) Ο-uniqueβ {M = M} f = Nat-pathp _ _ Ξ» _ β Univalent.Hom-pathp-refll-iso dcat lemma where Οβ² : Lβ.Ext => M Οβ² .Ξ· x = Lβ.Ο f .Ξ· x D.β Lβ.Ο Lβ.eta .Ξ· x Οβ² .is-natural x y f = D.pullr (Lβ.Ο _ .is-natural _ _ _) β D.extendl (Lβ.Ο _ .is-natural _ _ _) lemma : β {x} β Lβ.Ο f .Ξ· x D.β Lβ.Ο (Lβ.eta) .Ξ· x β‘ Lβ.Ο f .Ξ· x lemma {x = x} = sym $ ap (Ξ» e β e .Ξ· x) {y = Οβ²} $ Lβ.Ο-uniq $ Nat-path Ξ» _ β sym ( D.pullr (Lβ.Ο-comm Ξ·β _) β Lβ.Ο-comm Ξ·β _)
Now is all the data of a left extension: The other two fields are propositions, and so they are automatically identified β regardless of the specific isomorphism we would have exhibited.
open Lan Lan-unique : Lβ β‘ Lβ Lan-unique i .Ext = cd-cat .to-path Ext-unique i Lan-unique i .eta = eta-uniqueβ i Lan-unique i .Ο f = Ο-uniqueβ f i Lan-unique i .Ο-comm {Ξ± = Ξ±} = is-propβpathp (Ξ» i β [C,D].Hom-set _ _ ((Ο-uniqueβ Ξ± i β p) βnt eta-uniqueβ i) Ξ±) Lβ.Ο-comm Lβ.Ο-comm i Lan-unique i .Ο-uniq {M = M} {Ξ± = Ξ±} {Οβ² = Οβ²} = is-propβpathp (Ξ» i β Ξ -is-hlevelΒ² {A = cd-cat .to-path Ext-unique i => M} {B = Ξ» Οβ² β Ξ± β‘ (Οβ² β p) βnt eta-uniqueβ i} 1 Ξ» Οβ² x β [Cβ²,D].Hom-set _ _ (Ο-uniqueβ Ξ± i) Οβ²) (Ξ» Οβ² β Lβ.Ο-uniq {Οβ² = Οβ²}) (Ξ» Οβ² β Lβ.Ο-uniq {Οβ² = Οβ²}) i Οβ²