lude

commit 96781a09d74372601ea0deb86ee2977f9d0de1bf
parent 727fa06d23cee17763553e8c703bbfcd06a6a6ce
Author: Robert Russell <robert@rr3.xyz>
Date:   Wed,  9 Sep 2026 21:46:35 -0700

Algebra.Category: add Adjunction

Diffstat:
A
src/Lude/Algebra/Category/Adjunction.hs
 | 
35
+++++++++++++++++++++++++++++++++++

1 file changed, 35 insertions(+), 0 deletions(-)
diff --git a/src/Lude/Algebra/Category/Adjunction.hs b/src/Lude/Algebra/Category/Adjunction.hs
@@ -0,0 +1,35 @@
+module Lude.Algebra.Category.Adjunction (
+    Adjoint (..),
+) where
+
+import Lude.Algebra.Category.Core
+import Lude.Algebra.Category.Iso
+import Lude.Haskell
+
+--------------------------------------------------------------------------------
+
+type Adjoint :: forall {i} {j}. (i -> j) -> (j -> i) -> Constraint
+class (Functorial f, Functorial g, Dom f ~ Cod g, Cod f ~ Dom g) => Adjoint (f :: i -> j) (g :: j -> i) | f -> g, g -> f where
+    {-# MINIMAL unit, counit | adj #-}
+
+    unit :: forall (a :: i). (Obj (Dom f) a) => Dom f a (g (f a))
+    unit = to adj identity \\ f `preservesObj` a
+
+    counit :: forall (b :: j). (Obj (Cod f) b) => Cod f (f (g b)) b
+    counit = fro adj identity \\ g `preservesObj` b
+
+    adj :: forall (a :: i) (b :: j). (Obj (Dom f) a, Obj (Cod f) b) => Iso Function (Cod f (f a) b) (Dom f a (g b))
+    adj = MkIso (\h -> map h . unit) (\h -> counit . map h)
+
+--------------------------------------------------------------------------------
+-- Haskell
+
+instance Adjoint Given Evidence where
+    unit = witnessSelf
+    counit = coprovisionSelf
+    adj = MkIso witnessOf coprovisionOf
+
+instance Adjoint Evidence Given where
+    unit = provisionSelf
+    counit = cowitnessSelf
+    adj = MkIso provisionOf cowitnessOf