open import Cat.Instances.Functor
open import Cat.Instances.Product
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 _=>_


Recall from the page on adjoint functors that an adjoint pair induces an isomorphism

of sending each morphism to its left and right adjuncts, respectively. What that page does not mention is that any functors with such a correspondence β as long as the isomorphism is natural β actually generates an adjunction with the unit and counit given by the adjuncts of each identity morphism.

More precisely, the data we require is an equivalence (of sets) such that the equation

holds. While this may seem un-motivated, itβs really a naturality square for a transformation between the bifunctors and 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 since if a natural transformation is componentwise invertible, then its inverse is natural as well. It remains to use our βbinaturalityβ to compute that and 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                    β
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                               β
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

: (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
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[-,-] C Fβ (Functor.op L FΓ Id)) ββΏ (Hom[-,-] D Fβ (Id FΓ R))
β L β£ R
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}
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)

: β 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 _ _)