lude

commit 1526357302ee8f276421363b7d7387de52c71041
parent 8888a4c875636eb311f7f8693f41814e206a978c
Author: Robert Russell <robert@rr3.xyz>
Date:   Sun,  6 Sep 2026 17:46:13 -0700

Algebra.Category: add Discrete

Diffstat:
M
src/Lude/Algebra/Category.hs
 | 
1
+
A
src/Lude/Algebra/Category/Discrete.hs
 | 
17
+++++++++++++++++

2 files changed, 18 insertions(+), 0 deletions(-)
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -3,6 +3,7 @@ module Lude.Algebra.Category (
 ) where
 
 import Lude.Algebra.Category.Core as X
+import Lude.Algebra.Category.Discrete as X
 import Lude.Algebra.Category.Dual as X
 import Lude.Algebra.Category.Object as X
 
diff --git a/src/Lude/Algebra/Category/Discrete.hs b/src/Lude/Algebra/Category/Discrete.hs
@@ -0,0 +1,17 @@
+module Lude.Algebra.Category.Discrete (
+    Discrete (..),
+) where
+
+import Lude.Algebra.Category.Core
+
+-- TODO: Discrete is a groupoid.
+
+--------------------------------------------------------------------------------
+
+type Discrete :: forall k. Cat k
+data Discrete _ _ where
+    Refl :: forall a. Discrete a a
+
+instance Categorical Discrete where
+    identity = Refl
+    compose Refl Refl = Refl