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 = _β£_.Ξ· (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 = _β£_.Ξ΅ (adjs i) a}) (x .counit-iso a) (y .counit-iso a) i