module
  Cat.Functor.Adjoint.Unique
  {o β„“ oβ€² β„“β€²} {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²}
  where

Uniqueness of adjointsπŸ”—

Let F:Cβ†’DF : \mathcal{C} \to \mathcal{D} be a functor participating in two adjunctions F⊣GF \dashv G and F⊣Gβ€²F \dashv G'. Using the data from both adjunctions, we can exhibit a natural isomorphism Gβ‰…Gβ€²G \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 G≅G′G \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 Gβ‰…Gβ€²G \cong G' to an identity G≑GG \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
  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 F:Cβ†’DF : \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