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: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

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