Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
(*
Lemma homset_adjunction `(C:ECategory(V:=V))`(D:ECategory(V:=V))(L:Func C D)(R:Func D C)
: (L -| R)
- -> RepresentableFunctorºᑭ _ _ >>>> YonedaBiFunctor D ≃
- RepresentableFunctorºᑭ _ _ >>>> YonedaBiFunctor C.
+ -> HomFunctorºᑭ _ _ >>>> YonedaBiFunctor D ≃
+ HomFunctorºᑭ _ _ >>>> YonedaBiFunctor C.
*)
(* adjuncts are unique up to natural iso *)
(* adjuncts compose *)