module
  Cat.Functor.Adjoint.Unique
  {o  o′ ℓ′} {C : Precategory o } {D : Precategory o′ ℓ′}
  where

Uniqueness of adjoints🔗

Let F:CDF : \mathcal{C} \to \mathcal{D} be a functor participating in two adjunctions FGF \dashv G and FGF \dashv G'. Using the data from both adjunctions, we can exhibit a natural isomorphism GGG \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.

The isomorphism is defined (in components) to be GεηGG'\varepsilon\eta'G, with inverse GεηGG\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              

The data above is exactly what we need to define a natural isomorphism GGG \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 C\mathcal{C} is furthermore univalent, so that natural isomorphisms are an identity system on the functor category [D,C][D, C], we can upgrade the isomorphism GGG \cong G' to an identity GGG \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

As a corollary, we conclude that, for a functor F:CDF : \mathcal{C} \to \mathcal{D} from a univalent category C\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