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 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 Î·â â¡ Î·â
â Inversesâ¿ Î± Î²
Ï-inversesp Î±-factor Î²-factor = C'D.make-inverses
(lâ.Ï-uniqâ Î·â
(ext Î» j â sym (D.pullr (Î²-factor Î·â j) â Î±-factor Î·â j))
(ext Î» j â sym (D.idl _)))
(lâ.Ï-uniqâ Î·â
(ext Î» j â sym (D.pullr (Î±-factor Î·â j) â Î²-factor Î·â j))
(ext Î» 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 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-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} {Î±} = ext Î» 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 = ext Î» j â
lan.Ï Î± .Î· j D.â inv .Î· j                  â¡âš (lan.Ï-uniq {Ï' = Ï' ânt lan.Ï eta'} (ext Î» 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} {Î±} = ext Î» 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 $ext Î» 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} {Î±} = ext Î» 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 = ext Î» j â lan.Ï Î± .Î· j D.â isos.from .Î· j â¡âš D.pushl (lan.Ï-uniq {Ï' = Ï' ânt isos.to} (ext Î» 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} = ext Î» j â D.pulll ((lan.Ï _ .is-natural _ _ _)) â D.pullr (lan.Ï-comm Î·â _) â cancell M (isos.invl Î·â _) lan' .Ï-uniq {M = M} {Î± = Î±} {Ï' = Ï'} q = ext Î» c' â lan.Ï-uniq {Î± = (M âž isos.from) ânt Î±} {Ï' = Ï'} (ext Î» 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) (ext Î» x â D.extendl (D.pulll (G-iso .to .is-natural _ _ _)) â q Î·â _) where open 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)) â¡ Îµâ â Inversesâ¿ Î± Î² Ï-inversesp Î±-factor Î²-factor = C'D.make-inverses (râ.Ï-uniqâ Îµâ (ext Î» j â sym (D.pulll (Î±-factor Î·â j) â Î²-factor Î·â j)) (ext Î» j â sym (D.idr _))) (râ.Ï-uniqâ Îµâ (ext Î» j â sym (D.pulll (Î²-factor Î·â j) â Î±-factor Î·â j)) (ext Î» 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} {Î²} = ext Î» j â sym ((ran.Ï-comm Î·â _) D.â©ââšrefl) Â·Â· D.cancel-inner (invl Î·â _) Â·Â· (ran.Ï-comm Î·â _) ran' .Ï-uniq {M} {Î²} {Ï'} p = ext Î» j â (D.reflâ©ââš ran.Ï-uniq {Ï' = ran.Ï eps' ânt Ï'} (ext Î» 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} {Î²} = ext Î» j â D.pullr (ran.Ï-comm Î·â j) â D.cancell (isos.invl Î·â _) ran' .Ï-uniq {M} {Î²} {Ï'} p = ran.Ï-uniq$ ext Î» j â
(D.reflâ©ââš p Î·â 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} {Î²} = ext Î» j â
D.cancel-inner (isos.invr Î·â _)
â ran.Ï-comm Î·â _
ran' .Ï-uniq {M} {Î²} {Ï'} p = ext Î» j â
D.pushr (ran.Ï-uniq {Ï' = isos.from ânt Ï'} (ext Î» 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} = ext Î» j â
D.pullr (sym (ran.Ï _ .is-natural _ _ _))
â D.pulll (ran.Ï-comm Î·â _)
â cancelr M (isos.invl Î·â _)
ran' .Ï-uniq {M = M} {Î² = Î²} {Ï' = Ï'} q = ext Î» c' â
ran.Ï-uniq {Î² = Î² ânt (M âž isos.to)} {Ï' = Ï'}
(ext Î» 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)
(ext Î» 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