open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Functor.Adjoint
open import Cat.Instances.Sets
open import Cat.Functor.Hom
open import Cat.Prelude

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

module Cat.Functor.Adjoint.Hom where

module _ {o β o' β'} {C : Precategory o β} {D : Precategory o' β'}
{L : Functor D C} {R : Functor C D}
where

  private
module C = Cat C
module D = Cat D
module L = Func L
module R = Func R
open _β£_
open _=>_


# Adjoints as hom-isomorphismsπ

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 bifunctors $\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

hom-isoβadjoints
: (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
hom-isoβadjoints f f-equiv natural = adj' where
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(\operatorname{id}_{})$ and $f^{-1}(\operatorname{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                    β
adj' .zig =
fβ»ΒΉ D.id C.β L.β (f C.id)          β‘β¨ C.introl refl β©β‘
C.id C.β fβ»ΒΉ D.id C.β L.β (f C.id) β‘Λβ¨ inv-natural _ _ _ β©β‘Λ
fβ»ΒΉ (R.β C.id D.β D.id D.β f C.id) β‘β¨ ap fβ»ΒΉ (D.cancell (D.idr _ β R.F-id)) β©β‘
fβ»ΒΉ (f C.id)                       β‘β¨ equivβunit f-equiv _ β©β‘
C.id                               β
adj' .zag =
R.β (fβ»ΒΉ D.id) D.β f C.id          β‘β¨ D.reflβ©ββ¨ D.intror refl β©β‘
R.β (fβ»ΒΉ D.id) D.β f C.id D.β D.id β‘Λβ¨ natural _ _ _ β©β‘Λ
f (fβ»ΒΉ D.id C.β C.id C.β L.β D.id) β‘β¨ ap f (C.elimr (C.idl _ β L.F-id)) β©β‘
f (fβ»ΒΉ D.id)                       β‘β¨ equivβcounit f-equiv _ β©β‘
D.id                               β

  hom-iso-inv-natural
: (f : β {x y} β D.Hom x (R.β y) β C.Hom (L.β x) y)
β Type _
hom-iso-inv-natural f =
β {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

hom-iso-invβadjoints
: (f : β {x y} β D.Hom x (R.β y) β C.Hom (L.β x) y)
β (eqv : β {x y} β is-equiv (f {x} {y}))
β hom-iso-inv-natural f
β L β£ R
hom-iso-invβadjoints f f-equiv natural = hom-isoβadjoints f.from (f.inverse .snd) nat where
module f {x} {y} = Equiv (_ , f-equiv {x} {y})
abstract
nat : hom-iso-natural f.from
nat g h x = f.injective (f.Ξ΅ _ β sym (natural _ _ _ β ap (g C.β_) (ap (C._β L.β h) (f.Ξ΅ _))))

module _ {o β o'} {C : Precategory o β} {D : Precategory o' β}
{L : Functor D C} {R : Functor C D}
where
private
module C = Cat C
module D = Cat D
module L = Func L
module R = Func R

hom-natural-isoβadjoints
: (Hom[-,-] C Fβ (Functor.op L FΓ Id)) ββΏ (Hom[-,-] D Fβ (Id FΓ R))
β L β£ R
hom-natural-isoβadjoints eta =
hom-isoβadjoints (to .Ξ· _) (natural-iso-to-is-equiv eta (_ , _)) Ξ» g h x β
happly (to .is-natural _ _ (h , g)) x
where
open IsoβΏ eta
open _=>_

module _ {o β o'} {C : Precategory o β} {D : Precategory o' β}
{L : Functor D C} {R : Functor C D}
(adj : L β£ R)
where
private
module C = Cat C
module D = Cat D
module L = Func L
module R = Func R

hom-equiv : β {a b} β C.Hom (L.β a) b β D.Hom a (R.β b)
hom-equiv = _ , L-adjunct-is-equiv adj

adjunct-hom-iso-from
: β a β Hom-from C (L.β a) ββΏ Hom-from D a Fβ R
adjunct-hom-iso-from a = isoβisoβΏ (Ξ» _ β equivβiso hom-equiv)
Ξ» f β funext Ξ» g β sym (L-adjunct-naturalr adj _ _)

adjunct-hom-iso-into
: β b β Hom-into C b Fβ Functor.op L ββΏ Hom-into D (R.β b)
adjunct-hom-iso-into b = isoβisoβΏ (Ξ» _ β equivβiso hom-equiv)
Ξ» f β funext Ξ» g β sym (L-adjunct-naturall adj _ _)

adjunct-hom-iso
: Hom[-,-] C Fβ (Functor.op L FΓ Id) ββΏ Hom[-,-] D Fβ (Id FΓ R)
adjunct-hom-iso = isoβisoβΏ (Ξ» _ β equivβiso hom-equiv)
Ξ» (f , h) β funext Ξ» g β sym (L-adjunct-naturalβ adj _ _ _)