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 $F : \mathcal{C} \to \mathcal{D}$ be a functor participating in two adjunctions $F \dashv G$ and $F \dashv G'$. Using the data from both adjunctions, we can exhibit a natural isomorphism $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'{\varepsilon}\eta'G$, with inverse $G{\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 \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 $\mathcal{C}$ is furthermore univalent, so that natural isomorphisms are an identity system on the functor category $[D, C]$, we can upgrade the isomorphism $G \cong G'$ to an identity $G \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 : \mathcal{C} \to \mathcal{D}$ from a univalent category $\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