lude

commit 65434a8b929548b0f5cf317d9cc89ed47efa6e5f
parent 96781a09d74372601ea0deb86ee2977f9d0de1bf
Author: Robert Russell <robert@rr3.xyz>
Date:   Wed,  9 Sep 2026 22:13:32 -0700

Algebra.Category: add semigroupal and monoidal functors, and add cartesian categories

Diffstat:
M
package.yaml
 | 
2
+-
M
src/Lude/Algebra/Category/Bifunctor.hs
 | 
84
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
M
src/Lude/Algebra/Category/Core.hs
 | 
13
++++++++++---

3 files changed, 95 insertions(+), 4 deletions(-)
diff --git a/package.yaml b/package.yaml
@@ -36,7 +36,6 @@ default-extensions:
     - FunctionalDependencies
     - LiberalTypeSynonyms
     - MagicHash
-    - NoImplicitPrelude
     - NoListTuplePuns
     - NoStarIsType
     - OverloadedLists
@@ -44,6 +43,7 @@ default-extensions:
     - PartialTypeSignatures
     - PatternSynonyms
     - QuantifiedConstraints
+    - RebindableSyntax
     - RecursiveDo
     - RequiredTypeArguments
     - TypeAbstractions
diff --git a/src/Lude/Algebra/Category/Bifunctor.hs b/src/Lude/Algebra/Category/Bifunctor.hs
@@ -11,6 +11,8 @@ module Lude.Algebra.Category.Bifunctor (
 ) where
 
 import Lude.Algebra.Category.Core
+import Lude.Algebra.Category.Iso
+import Lude.Algebra.Category.Terminal
 import Lude.Haskell
 
 -- TODO: Read Conor McBride's paper on bifunctors and decide what abstractions
@@ -68,3 +70,85 @@ rmap
     => BidomR f ra rb
     -> Bicod f (f l ra) (f l rb)
 rmap rf = map rf \\ f `preservesObj` l
+
+--------------------------------------------------------------------------------
+
+-- | A semigroup structure on a category, represented as a bifunctor
+--
+-- TODO: Laws
+type SemigroupalFunctorial :: forall {i}. Biendo i -> Constraint
+class (Biendofunctorial f) => SemigroupalFunctorial (f :: Biendo i) where
+    assoc :: forall a b c. (Obj3 (Dom f) a b c) => Iso (Dom f) ((a `f` b) `f` c) (a `f` (b `f` c))
+
+type SemigroupalFunctorialOn :: forall {i}. Cat i -> Biendo i -> Constraint
+class (SemigroupalFunctorial f, Dom f ~ p) => SemigroupalFunctorialOn p f
+instance (SemigroupalFunctorial f, Dom f ~ p) => SemigroupalFunctorialOn p f
+
+--------------------------------------------------------------------------------
+
+-- | A monoid structure on a category, represented as a bifunctor and unit object
+--
+-- TODO: Laws
+type MonoidalFunctorial :: forall {i}. Biendo i -> Constraint
+class (SemigroupalFunctorial f) => MonoidalFunctorial (f :: Biendo i) where
+    type Monid f :: i
+    monidl :: forall a. (Obj (Dom f) a) => Iso (Dom f) (Monid f `f` a) a
+    monidr :: forall a. (Obj (Dom f) a) => Iso (Dom f) (a `f` Monid f) a
+
+type MonoidalFunctorialOn :: forall {i}. Cat i -> Biendo i -> Constraint
+class (MonoidalFunctorial f, Dom f ~ p) => MonoidalFunctorialOn p f
+instance (MonoidalFunctorial f, Dom f ~ p) => MonoidalFunctorialOn p f
+
+--------------------------------------------------------------------------------
+
+-- TODO: Require Diag -| Prod adjunction.
+
+type CartesianCategorial :: forall {i}. Cat i -> Constraint
+class (MonoidalFunctorialOn p (Prod p), HasTerminalObject p, Terminal p ~ Monid (Prod p)) => CartesianCategorial (p :: Cat i) where
+    {-# MINIMAL outl, outr, (diag | pair) #-}
+
+    type Prod p :: i -> i -> i
+
+    outl :: forall a b. (Obj2 p a b) => Prod p a b `p` a
+    outr :: forall a b. (Obj2 p a b) => Prod p a b `p` b
+
+    diag :: forall a. (Obj p a) => a `p` Prod p a a
+    diag = pair identity identity
+
+    -- TODO: Make this an iso? We don't need the Obj constraint, either, but
+    -- I don't like having to pick f or g for the witness.
+    pair :: forall a b c. (Obj p a) => a `p` b -> a `p` c -> a `p` Prod p b c
+    pair f g = bimap f g . diag
+
+--------------------------------------------------------------------------------
+-- TODO: Temp
+
+type Pair :: Type -> Type -> Type
+data Pair a b = MkPair a b
+
+instance Functorial (Pair a) where map f = \(MkPair x y) -> MkPair x (f y)
+instance Functorial Pair where map f = Natural \(MkPair x y) -> MkPair (f x) y
+
+instance SemigroupalFunctorial Pair where
+    assoc = MkIso to fro
+      where
+        to (MkPair (MkPair x y) z) = MkPair x (MkPair y z)
+        fro (MkPair x (MkPair y z)) = MkPair (MkPair x y) z
+
+instance MonoidalFunctorial Pair where
+    type Monid Pair = Terminal Function
+    monidl = MkIso to fro
+      where
+        to (MkPair () x) = x
+        fro x = MkPair () x
+    monidr = MkIso to fro
+      where
+        to (MkPair x ()) = x
+        fro x = MkPair x ()
+
+instance CartesianCategorial Function where
+    type Prod Function = Pair
+    outl (MkPair x _) = x
+    outr (MkPair _ y) = y
+    diag x = MkPair x x
+    pair f g = \x -> MkPair (f x) (g x)
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -7,6 +7,8 @@ module Lude.Algebra.Category.Core (
     --
     Categorical (..),
     Mor,
+    Obj2,
+    Obj3,
     (.),
     --
     Dual (..),
@@ -54,9 +56,14 @@ class Categorical (p :: Cat i) where
     default witnessMor :: forall a b. (Mor p a b) => Witness (a `p` b) (Mor p a b)
     witnessMor = witnessOf tautology
 
-type Mor :: forall {i}. Cat i -> i -> i -> Constraint
-class (Obj p a, Obj p b) => Mor p a b
-instance (Obj p a, Obj p b) => Mor p a b
+type Mor = Obj2
+type Obj2 :: forall {i}. Cat i -> i -> i -> Constraint
+class (Obj p a, Obj p b) => Obj2 p a b
+instance (Obj p a, Obj p b) => Obj2 p a b
+
+type Obj3 :: forall {i}. Cat i -> i -> i -> i -> Constraint
+class (Obj p a, Obj p b, Obj p c) => Obj3 p a b c
+instance (Obj p a, Obj p b, Obj p c) => Obj3 p a b c
 
 (.) :: forall {i} (p :: Cat i) a b c. (Categorical p) => b `p` c -> a `p` b -> a `p` c
 (.) = compose