open import Cat.Functor.Adjoint
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning as Cat

{o ℓ o′ ℓ′} {C : Precategory o ℓ} {D : Precategory o′ ℓ′}
{L : Functor D C} {R : Functor C D}
where


Recall from the page on adjoint functors that an adjoint pair $L \dashv R$ induces an isomorphism

${\mathbf{Hom}}_\mathcal{C}(L(x), y) \cong {\mathbf{Hom}}_\mathcal{D}(x, R(y))$

of ${\mathbf{Hom}}$-sets, sending each morphism to its left and right adjuncts, respectively. What that page does not mention is that any functors $L, R$ with such a correspondence — as long as the isomorphism is natural — actually generates an adjunction $L \dashv R$, with the unit and counit given by the adjuncts of each identity morphism.

More precisely, the data we require is an equivalence (of sets) $f : {\mathbf{Hom}}_\mathcal{C}(Lx,y) \to {\mathbf{Hom}}_\mathcal{D}(x,Ry)$ such that the equation

$f(g \circ x \circ Lh) = Rg \circ fx \circ h$

holds. While this may seem un-motivated, it’s really a naturality square for a transformation between the functors ${\mathbf{Hom}}_\mathcal{C}(L-,-)$ and ${\mathbf{Hom}}_\mathcal{D}(-,R-)$ whose data has been “unfolded” into elementary terms.

hom-iso-natural
: (∀ {x y} → C.Hom (L.₀ x) y → D.Hom x (R.₀ y))
→ Type _
hom-iso-natural f =
∀ {a b c d} (g : C.Hom a b) (h : D.Hom c d) x
→ f (g C.∘ x C.∘ L.₁ h) ≡ R.₁ g D.∘ f x D.∘ h

: (f : ∀ {x y} → C.Hom (L.₀ x) y → D.Hom x (R.₀ y))
→ (eqv : ∀ {x y} → is-equiv (f {x} {y}))
→ hom-iso-natural f
→ L ⊣ R
f⁻¹ : ∀ {x y} → D.Hom x (R.₀ y) → C.Hom (L.₀ x) y
f⁻¹ = equiv→inverse f-equiv

inv-natural : ∀ {a b c d} (g : C.Hom a b) (h : D.Hom c d) x
→ f⁻¹ (R.₁ g D.∘ x D.∘ h) ≡ g C.∘ f⁻¹ x C.∘ L.₁ h
inv-natural g h x = ap fst \$ is-contr→is-prop (f-equiv .is-eqv _)
(f⁻¹ (R.₁ g D.∘ x D.∘ h) , refl)
( g C.∘ f⁻¹ x C.∘ L.₁ h
, natural _ _ _
∙ sym (equiv→counit f-equiv _)
∙ ap (f ⊙ f⁻¹)
(D.extendl (ap (R.₁ g D.∘_) (equiv→counit f-equiv _))))


We do not require an explicit naturality witness for the inverse of $f$, since if a natural transformation is componentwise invertible, then its inverse is natural as well. It remains to use our “binaturality” to compute that $f({{\mathrm{id}}_{}})$ and $f^{-1}({{\mathrm{id}}_{}})$ do indeed give a system of adjunction units and co-units.

  adj′ : L ⊣ R
adj′ .unit .η x = f C.id
adj′ .unit .is-natural x y h =
f C.id D.∘ h                    ≡⟨ D.introl R.F-id ⟩≡
R.₁ C.id D.∘ f C.id D.∘ h       ≡˘⟨ natural _ _ _ ⟩≡˘
f (C.id C.∘ C.id C.∘ L.₁ h)     ≡⟨ ap f (C.cancell (C.idl _) ∙ C.intror (C.idl _ ∙ L.F-id)) ⟩≡
f (L.₁ h C.∘ C.id C.∘ L.₁ D.id) ≡⟨ natural _ _ C.id ⟩≡
R.₁ (L.₁ h) D.∘ f C.id D.∘ D.id ≡⟨ D.refl⟩∘⟨ D.idr _ ⟩≡
R.₁ (L.₁ h) D.∘ f C.id          ∎
adj′ .counit .η x = f⁻¹ D.id
adj′ .counit .is-natural x y f =
f⁻¹ D.id C.∘ L.₁ (R.₁ f) ≡⟨ C.introl refl ⟩≡
C.id C.∘ f⁻¹ D.id C.∘ L.₁ (R.₁ f) ≡˘⟨ inv-natural _ _ _ ⟩≡˘
f⁻¹ (R.₁ C.id D.∘ D.id D.∘ R.₁ f) ≡⟨ ap f⁻¹ (D.cancell (D.idr _ ∙ R.F-id) ∙ D.intror (D.idl _)) ⟩≡
f⁻¹ (R.₁ f D.∘ D.id D.∘ D.id)     ≡⟨ inv-natural _ _ _ ⟩≡
f C.∘ f⁻¹ D.id C.∘ L.₁ D.id       ≡⟨ C.refl⟩∘⟨ C.elimr L.F-id ⟩≡
f C.∘ f⁻¹ D.id                    ∎