open import Cat.Functor.Equivalence
open import Cat.Functor.Naturality
open import Cat.Functor.Univalence
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning as Fr
import Cat.Reasoning as Cr

module
{o β oβ² ββ²} {C : Precategory o β} {D : Precategory oβ² ββ²}
where

private
module C = Cr C
module D = Cr D


# Uniqueness of adjointsπ

Let $F : \mathcal{C} \to \mathcal{D}$ be a functor participating in two adjunctions $F \dashv G$ and $F \dashv G'$. Using the data from both adjunctions, we can exhibit a natural isomorphism $G \cong G'$, which additionally preserves the unit and counit: Letting $\gamma$, $\delta$ be the components of the natural isomorphism, we have $\gamma\eta = \eta'$, idem for $\varepsilon$.

module _ {F : Functor C D} {G Gβ² : Functor D C} (a : F β£ G) (aβ² : F β£ Gβ²) where
private
module F = Fr F
module G = Fr G
module Gβ² = Fr Gβ²
module a = _β£_ a
module aβ² = _β£_ aβ²
open a.unit using (Ξ·)
open a.counit using (Ξ΅)
open aβ².unit hiding (is-natural) renaming (Ξ· to Ξ·β²)
open aβ².counit hiding (is-natural) renaming (Ξ΅ to Ξ΅β²)
open make-natural-iso


The isomorphism is defined (in components) to be $G'\varepsilon\eta'G$, with inverse $G\varepsilon'\eta{}G$. Here, we show the construction of both directions, cancellation in one directly, and naturality (naturality for the inverse is taken care of by make-natural-iso). Cancellation in the other direction is exactly analogous, and so was omitted.

  private
make-GβGβ² : make-natural-iso G Gβ²
make-GβGβ² .eta x = Gβ².β (Ξ΅ x) C.β Ξ·β² _
make-GβGβ² .inv x = G.β (Ξ΅β² x) C.β Ξ· _
make-GβGβ² .invβeta x =
(G.β (Ξ΅β² x) C.β Ξ· _) C.β Gβ².β (Ξ΅ _) C.β Ξ·β² _    β‘β¨ C.extendl (C.pullr (a.unit.is-natural _ _ _) β G.pulll (aβ².counit.is-natural _ _ _)) β©β‘
G.β (Ξ΅ x D.β Ξ΅β² _) C.β Ξ· _ C.β Ξ·β² _             β‘β¨ C.reflβ©ββ¨ a.unit.is-natural _ _ _ β©β‘
G.β (Ξ΅ x D.β Ξ΅β² _) C.β G.β (F.β (Ξ·β² _)) C.β Ξ· _ β‘β¨ G.pulll (D.cancelr aβ².zig) β©β‘
G.β (Ξ΅ x) C.β Ξ· _                               β‘β¨ a.zag β©β‘
C.id                                            β
make-GβGβ² .natural x y f =
Gβ².β f C.β Gβ².β (Ξ΅ x) C.β Ξ·β² _               β‘β¨ C.pulll (Gβ².weave (sym (a.counit.is-natural _ _ _))) β©β‘
(Gβ².β (Ξ΅ y) C.β Gβ².β (F.β (G.β f))) C.β Ξ·β² _ β‘β¨ C.extendr (sym (aβ².unit.is-natural _ _ _)) β©β‘
(Gβ².β (Ξ΅ y) C.β Ξ·β² _) C.β G.β f              β

    make-GβGβ² .etaβinv x =
C.extendl (C.pullr (aβ².unit.is-natural _ _ _))
Β·Β· apβ C._β_ refl (C.pushl (sym (aβ².unit.is-natural _ _ _)))
Β·Β· C.extend-inner (aβ².unit.is-natural _ _ _)
Β·Β· Gβ².extendl (a.counit.is-natural _ _ _)
Β·Β· apβ C._β_ refl ( apβ C._β_ refl (aβ².unit.is-natural _ _ _)
β Gβ².cancell a.zig)
β aβ².zag


The data above is exactly what we need to define a natural isomorphism $G \cong G'$. Showing that this isomorphism commutes with the adjunction natural transformations is a matter of calculating:

  right-adjoint-unique : Cr.Isomorphism Cat[ D , C ] G Gβ²
right-adjoint-unique = to-natural-iso make-GβGβ²

abstract
unique-preserves-unit
: β {x} β make-GβGβ² .eta _ C.β Ξ· x β‘ Ξ·β² x
unique-preserves-unit =
make-GβGβ² .eta _ C.β Ξ· _                 β‘β¨ C.pullr (aβ².unit.is-natural _ _ _) β©β‘
Gβ².β (Ξ΅ _) C.β Gβ².β (F.β (Ξ· _)) C.β Ξ·β² _ β‘β¨ Gβ².cancell a.zig β©β‘
Ξ·β² _                                     β

unique-preserves-counit
: β {x} β Ξ΅ _ D.β F.β (make-GβGβ² .inv _) β‘ Ξ΅β² x
unique-preserves-counit =
Ξ΅ _ D.β F.β (make-GβGβ² .inv _)         β‘β¨ D.reflβ©ββ¨ F.F-β _ _ β©β‘
Ξ΅ _ D.β F.β (G.β (Ξ΅β² _)) D.β F.β (Ξ· _) β‘β¨ D.extendl (a.counit.is-natural _ _ _) β©β‘
Ξ΅β² _ D.β Ξ΅ _ D.β F.β (Ξ· _)             β‘β¨ D.elimr a.zig β©β‘
Ξ΅β² _                                   β


If the codomain category $\mathcal{C}$ is furthermore univalent, so that natural isomorphisms are an identity system on the functor category $[D, C]$, we can upgrade the isomorphism $G \cong G'$ to an identity $G \equiv G$, and preservation of the adjunction data means this identity can be improved to an identification between pairs of the functors and their respective adjunctions.

is-left-adjoint-is-prop
: is-category C
β (F : Functor C D)
β is-prop $Ξ£[ G β Functor D C ] (F β£ G) is-left-adjoint-is-prop cc F (G , a) (Gβ² , aβ²) i = Gβ‘Gβ² cd i , aβ‘aβ² cd i   where Gβ Gβ² = right-adjoint-unique a aβ² cd = Functor-is-category cc open _β£_ open _=>_ open Functor module F = Fr F module _ (d : is-category Cat[ D , C ]) where Gβ‘Gβ² = d .to-path Gβ Gβ² abstract same-eta : PathP (Ξ» i β Id => Gβ‘Gβ² i Fβ F) (a .unit) (aβ² .unit) same-eta = Nat-pathp refl (Ξ» i β Gβ‘Gβ² i Fβ F) Ξ» x β Hom-pathp-reflr C$
apβ C._β_ (whisker-path-left {G = G} {Gβ²} {F = F} d GβGβ²) refl
β unique-preserves-unit a aβ²

same-eps : PathP (Ξ» i β F Fβ Gβ‘Gβ² i => Id) (a .counit) (aβ² .counit)
same-eps = Nat-pathp (Ξ» i β F Fβ Gβ‘Gβ² i) refl
Ξ» x β Hom-pathp-refll D $apβ D._β_ refl (whisker-path-right {G = F} {F = G} {Gβ²} d Gβ Gβ²) β unique-preserves-counit a aβ² aβ‘aβ² : PathP (Ξ» i β F β£ Gβ‘Gβ² i) a aβ² aβ‘aβ² i .unit = same-eta i aβ‘aβ² i .counit = same-eps i aβ‘aβ² i .zig {A} = is-setβsquarep (Ξ» i j β D.Hom-set (F.β A) (F.β A)) (Ξ» i β same-eps i .Ξ· (F.β A) D.β F.β (same-eta i .Ξ· A)) (a .zig) (aβ² .zig) refl i aβ‘aβ² i .zag {A} = is-setβsquarep (Ξ» i j β C.Hom-set (Gβ‘Gβ² i .Fβ A) (Gβ‘Gβ² i .Fβ A)) (Ξ» i β Gβ‘Gβ² i .Fβ (same-eps i .Ξ· A) C.β same-eta i .Ξ· (Gβ‘Gβ² i .Fβ A)) (a .zag) (aβ² .zag) (Ξ» _ β C.id) i  As a corollary, we conclude that, for a functor $F : \mathcal{C} \to \mathcal{D}$ from a univalent category $\mathcal{C}$, βbeing an equivalence of categoriesβ is a proposition. open is-equivalence is-equivalence-is-prop : is-category C β (F : Functor C D) β is-prop (is-equivalence F) is-equivalence-is-prop ccat F x y = go where invs = ap fst$
is-left-adjoint-is-prop ccat F (x .Fβ»ΒΉ , x .Fβ£Fβ»ΒΉ) (y .Fβ»ΒΉ , y .Fβ£Fβ»ΒΉ)

adjs = ap snd \$
is-left-adjoint-is-prop ccat F (x .Fβ»ΒΉ , x .Fβ£Fβ»ΒΉ) (y .Fβ»ΒΉ , y .Fβ£Fβ»ΒΉ)

go : x β‘ y
go i .Fβ»ΒΉ = invs i
go i .Fβ£Fβ»ΒΉ = adjs i
go i .unit-iso a =
is-propβpathp (Ξ» i β C.is-invertible-is-prop {f = _β£_.unit.Ξ· (adjs i) a})
(x .unit-iso a)
(y .unit-iso a) i
go i .counit-iso a =
is-propβpathp (Ξ» i β D.is-invertible-is-prop {f = _β£_.counit.Ξ΅ (adjs i) a})
(x .counit-iso a)
(y .counit-iso a) i