open import Cat.Functor.Equivalence open import Cat.Instances.Functor open import Cat.Functor.Adjoint open import Cat.Functor.Base open import Cat.Univalent open import Cat.Prelude import Cat.Functor.Reasoning as Fr import Cat.Reasoning as Cr 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 .
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 β
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
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