adjunct : (L a → b) → (a → R b)
coadjunct : (a → R b) → (L a → b)
unit : a → RL a
counit : LR b → b
Lmap : (a → b) → (L a → L b)
Rmap : (a → b) → (R a → R b)
adjunct f = unit ; Rmap f
coadjunct f = Lmap f ; counit
unit = adjunct id
counit = coadjunct id
Lmap f = coadjunct (f ; unit)
Rmap f = adjunct (counit ; f)
Last active
June 14, 2024 13:42
-
-
Save ncfavier/f9199fe5fb2aab356aafccedf2808d0a to your computer and use it in GitHub Desktop.
adjunction yoga 🧘
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment