open import Cat.Functor.Naturality
open import Cat.Functor.Univalence
open import Cat.Functor.Kan.Base
open import Cat.Functor.Compose
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

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 $F$ along $p$β also includes the natural transformation. For accuracy, using the setup from the diagram below, we should say β$(G, \eta)$ is the Kan extension of $F$ along $p$β.

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 $(G_1, \eta_1)$ and $(G_2, \eta_2)$ and both left extensions of $F$ along $p$. 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 $\mathcal{C}' \leftarrow \mathcal{C} \to \mathcal{D}$. So, to be clear: The upper triangle and the lower triangle are the same.

Recall that $(G_1, \eta_1)$ being a left extension means we can (uniquely) factor natural transformations $F \to Mp$ through transformations $G_1 \to M$. We want a map $G_1 \to G_2$, for which it will suffice to find a map $F \to G_2p$ β but $\eta_2$ is right there! In the other direction, we can factor $\eta_1$ to get a map $G_2 \to G_1$. Since these factorisations are unique, we have a natural isomorphism.

  Ο-inversesp
: β {Ξ± : Gβ => Gβ} {Ξ² : Gβ => Gβ}
β (Ξ± β p) βnt Ξ·β β‘ Ξ·β
β (Ξ² β p) βnt Ξ·β β‘ Ξ·β
β 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-invertibleβΏ Ξ±
Ο-is-invertiblep {Ξ± = Ξ±} Ξ±-factor =
C'D.inversesβinvertible (Ο-inversesp {Ξ±} Ξ±-factor lβ.Ο-comm)

Ο-inverses : InversesβΏ (lβ.Ο Ξ·β) (lβ.Ο Ξ·β)
Ο-inverses = Ο-inversesp lβ.Ο-comm lβ.Ο-comm

Ο-is-invertible : is-invertibleβΏ (lβ.Ο Ξ·β)
Ο-is-invertible = Ο-is-invertiblep lβ.Ο-comm

unique : Gβ ββΏ Gβ
unique = C'D.invertibleβiso (lβ.Ο Ξ·β) (Ο-is-invertiblep lβ.Ο-comm)


Itβs immediate from the construction that this isomorphism βsends $\eta_1$ to $\eta_2$β.

  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 $G' : \mathcal{C}' \to \mathcal{D}$ and candidate βunitβ transformation $\eta' : F \to G'p$, if a left extension $\operatorname{Lan}_p(F)$ sends $\eta'$ to a natural isomorphism, then $(G', \eta')$ is also a left extension of $F$ along $p$.

  is-invertibleβis-lan
: β {G' : Functor C' D} {eta' : F => G' Fβ p}
β is-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 : F ββΏ F')
β is-lan p F' G (eta βnt IsoβΏ.from isos)
natural-iso-ofβis-lan {F' = F'} isos = lan' where
open is-lan
module isos = 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 : G β βΏ G') β is-lan p F G' ((IsoβΏ.to isos β p) βnt eta) natural-iso-extβis-lan {G' = G'} isos = lan' where open is-lan module isos = 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 : p β βΏ p') β is-lan p' F G ((G βΈ IsoβΏ.to isos) βnt eta) natural-iso-alongβis-lan {p'} isos = lan' where open is-lan module isos = IsoβΏ isos open Cat.Functor.Reasoning lan' : is-lan p' F G ((G βΈ 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 : p β βΏ p') β (F-iso : F β βΏ F') β (G-iso : G β βΏ G') β ((IsoβΏ.to G-iso β IsoβΏ.to p-iso) βnt eps βnt 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 IsoβΏ  ## Into univalent categoriesπ As traditional with universal constructions, if $F : \mathcal{C} \to \mathcal{D}$ takes values in a univalent category, we can sharpen our result: the type of left extensions of $F$ along $p$ 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 $\mathcal{D}$ is univalent, then so is $[\mathcal{C}', \mathcal{D}]$, so our natural isomorphism $i : G_1 \cong G_2$ is equivalent to an identification $i' : G_1 \equiv G_2$. Then, our tiny lemma stating that this isomorphism βsends $\eta_1$ to $\eta_2$β is precisely the data of a dependent identification $\eta_1 \equiv \eta_2$ over $i'$.  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 $(G, \eta)$, 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)) β‘ Ξ΅β β 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-invertibleβΏ Ξ± Ο-is-invertiblep {Ξ±} Ξ±-factor = C'D.inversesβinvertible (Ο-inversesp {Ξ±} Ξ±-factor rβ.Ο-comm) Ο-inverses : InversesβΏ (rβ.Ο Ξ΅β) (rβ.Ο Ξ΅β) Ο-inverses = Ο-inversesp rβ.Ο-comm rβ.Ο-comm Ο-is-invertible : is-invertibleβΏ (rβ.Ο Ξ΅β) Ο-is-invertible = Ο-is-invertiblep rβ.Ο-comm unique : 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-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 : F β βΏ F') β is-ran p F' G (IsoβΏ.to isos βnt eps) natural-iso-ofβis-ran {F'} isos = ran' where open is-ran module isos = 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.deletel (isos.invr Ξ·β _)

natural-iso-extβis-ran
: {G' : Functor C' D}
β (isos : G ββΏ G')
β is-ran p F G' (eps βnt (IsoβΏ.from isos β p))
natural-iso-extβis-ran {G'} isos = ran' where
open is-ran
module isos = 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 : p ββΏ p')
β is-ran p' F G (eps βnt (G βΈ IsoβΏ.from isos))
natural-iso-alongβis-ran {p'} isos = ran' where
open is-ran
module isos = IsoβΏ isos
open Cat.Functor.Reasoning

ran' : is-ran p' F G (eps βnt (G βΈ IsoβΏ.from isos))
ran' .Ο {M} Ξ² = ran.Ο (Ξ² βnt (M βΈ 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 : p ββΏ p')
β (F-iso : F ββΏ F')
β (G-iso : G ββΏ G')
β (IsoβΏ.to F-iso βnt eps βnt (IsoβΏ.from G-iso β 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