Skip to content

Instantly share code, notes, and snippets.

@ncfavier

ncfavier/adjunction.txt

Last active February 4, 2024 11:46
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save ncfavier/f9199fe5fb2aab356aafccedf2808d0a to your computer and use it in GitHub Desktop.
Save ncfavier/f9199fe5fb2aab356aafccedf2808d0a to your computer and use it in GitHub Desktop.
Download ZIP
adjunction yoga cheatsheet
Raw
adjunction.txt
L ⊣ R
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment