module Cat.Functor.Adjoint.Unique {o β oβ² ββ²} {C : Precategory o β} {D : Precategory oβ² ββ²} where
Uniqueness of adjointsπ
Let be a functor participating in two adjunctions and . Using the data from both adjunctions, we can exhibit a natural isomorphism , which additionally preserves the unit and counit: Letting , be the components of the natural isomorphism, we have , idem for .
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
,
with inverse
.
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 . 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 is furthermore univalent, so that natural isomorphisms are an identity system on the functor category , we can upgrade the isomorphism to an identity , 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 from a univalent category , β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