1 Generalizable All Variables.
2 Require Import Preamble.
3 Require Import Categories_ch1_3.
4 Require Import Functors_ch1_4.
5 Require Import Isomorphisms_ch1_5.
6 Require Import NaturalTransformations_ch7_4.
7 Require Import NaturalIsomorphisms_ch7_5.
8 Require Import MonoidalCategories_ch7_8.
10 (*******************************************************************************)
11 (* Chapter 9: Adjoints *)
12 (*******************************************************************************)
14 Class Adjunction `{C:Category}`{D:Category}{Fobj}{Gobj}(L:Functor D C Fobj)(R:Functor C D Gobj) :=
15 { adj_counit : functor_id D ~~~> L >>>> R
16 ; adj_unit : R >>>> L ~~~> functor_id C
17 ; adj_pf1 : forall (X:C)(Y:D), id (L Y) ~~ (L \ (adj_counit Y)) >>> (adj_unit (L Y))
18 ; adj_pf2 : forall (X:C)(Y:D), id (R X) ~~ (adj_counit (R X)) >>> (R \ (adj_unit X))
19 (* FIXME: use the definition based on whiskering *)
21 Notation "L -| R" := (Adjunction L R).
22 Notation "'ε'" := (adj_counit _).
23 Notation "'η'" := (adj_unit _).
25 (* Definition 9.6 "Official" *)
27 Lemma homset_adjunction `(C:ECategory(V:=V))`(D:ECategory(V:=V))(L:Func C D)(R:Func D C)
29 -> HomFunctorºᑭ _ _ >>>> YonedaBiFunctor D ≃
30 HomFunctorºᑭ _ _ >>>> YonedaBiFunctor C.
32 (* adjuncts are unique up to natural iso *)
33 (* adjuncts compose *)
34 (* adjuncts preserve limits *)
35 (* every adjunction determines a monad, vice versa *)
37 (* Kleisli category *)
38 (* if C is enriched, then we get an iso of hom-sets *)
43 (* Example 9.7: exopnentiation is right adjoint to product *)
45 (* Example 9.8: terminal object selection is right adjoint to the terminal-functor in Cat *)
47 (* Proposition 9.9: Adjoints are unique up to iso *)
49 (* Example 9.9: Product is left adjoint to diagonal, and coproduct is right adjoint; generalizes to limits/colimits *)
52 (* Proposition 9.14: RAPL *)