{o β„“ o' β„“'} {C : Precategory o β„“} {D : Precategory o' β„“'}

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.

    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 ( _ _ _) βˆ™ G.pulll (a' _ _ _)) βŸ©β‰‘
      G.₁ (Ξ΅ x D.∘ Ξ΅' _) C.∘ Ξ· _ C.∘ Ξ·' _             β‰‘βŸ¨ C.refl⟩∘⟨ _ _ _ βŸ©β‰‘
      G.₁ (Ξ΅ x D.∘ Ξ΅' _) C.∘ G.₁ (F.₁ (Ξ·' _)) C.∘ Ξ· _ β‰‘βŸ¨ G.pulll (D.cancelr a'.zig) βŸ©β‰‘
      G.₁ (Ξ΅ x) C.∘ Ξ· _                               β‰‘βŸ¨ a.zag βŸ©β‰‘                                            ∎
    make-G≅G' .natural x y f =
      G'.₁ f C.∘ G'.₁ (Ξ΅ x) C.∘ Ξ·' _               β‰‘βŸ¨ C.pulll (G'.weave (sym ( _ _ _))) βŸ©β‰‘
      (G'.₁ (Ξ΅ y) C.∘ G'.₁ (F.₁ (G.₁ f))) C.∘ Ξ·' _ β‰‘βŸ¨ C.extendr (sym (a' _ _ _)) βŸ©β‰‘
      (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'

      : βˆ€ {x} β†’ make-Gβ‰…G' .eta _ C.∘ Ξ· x ≑ Ξ·' x
    unique-preserves-unit =
      make-Gβ‰…G' .eta _ C.∘ Ξ· _                 β‰‘βŸ¨ C.pullr (a' _ _ _) βŸ©β‰‘
      G'.₁ (Ξ΅ _) C.∘ G'.₁ (F.₁ (Ξ· _)) C.∘ Ξ·' _ β‰‘βŸ¨ G'.cancell a.zig βŸ©β‰‘
      η' _                                     ∎

      : βˆ€ {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 ( _ _ _) βŸ©β‰‘
      Ξ΅' _ 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-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-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 β†’ {f = _⊣_.Ξ· (adjs i) a})
      (x .unit-iso a)
      (y .unit-iso a) i
  go i .counit-iso a =
    is-propβ†’pathp (Ξ» i β†’ {f = _⊣_.Ξ΅ (adjs i) a})
      (x .counit-iso a)
      (y .counit-iso a) i