lude

commit 49af51c87b8fd1dde1b2ac6f08b04248b9c7b4db
parent 2f411f6a6242544a7795051312651328b8c37932
Author: Robert Russell <robert@rr3.xyz>
Date:   Fri,  4 Sep 2026 20:34:33 -0700

Add initial and terminal objects for Function and Entailment

Diffstat:
M
src/Lude/Algebra/Category/Core.hs
 | 
2
+-
M
src/Lude/Algebra/Category/Object.hs
 | 
31
+++++++++++++++++++++++++++++++
M
src/Lude/Constraint/Falsum.hs
 | 
6
------
M
src/Lude/Constraint/Verum.hs
 | 
5
-----
M
src/Lude/Unit.hs
 | 
5
-----
M
src/Lude/Void.hs
 | 
5
-----

6 files changed, 32 insertions(+), 22 deletions(-)
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -20,7 +20,7 @@ module Lude.Algebra.Category.Core (
     --
     Function,
     type (~>),
-    Entailment,
+    Entailment (..),
     (:-),
     (:~),
 ) where
diff --git a/src/Lude/Algebra/Category/Object.hs b/src/Lude/Algebra/Category/Object.hs
@@ -1,10 +1,17 @@
 module Lude.Algebra.Category.Object (
     HasTerminalObject (..),
+    trivial,
     HasInitialObject (..),
+    absurd,
 ) where
 
 import Lude.Algebra.Category.Core
+import Lude.Constraint.Core
+import Lude.Constraint.Falsum
+import Lude.Constraint.Verum
 import Lude.Kind
+import Lude.Unit
+import Lude.Void
 
 --------------------------------------------------------------------------------
 
@@ -13,9 +20,33 @@ class (Categorical p) => HasTerminalObject (p :: Cat k) where
     type Terminal p :: k
     terminate :: forall a. a `p` Terminal p
 
+-- | Alias for `terminate`
+trivial :: (HasTerminalObject p) => forall a. a `p` Terminal p
+trivial = terminate
+
+instance HasTerminalObject Function where
+    type Terminal Function = Unit
+    terminate = \_ -> ()
+
+instance HasTerminalObject Entailment where
+    type Terminal Entailment = Verum
+    terminate = Entailment Evidence
+
 --------------------------------------------------------------------------------
 
 type HasInitialObject :: forall {k}. Cat k -> Constraint
 class (Categorical p) => HasInitialObject (p :: Cat k) where
     type Initial p :: k
     initiate :: forall a. Initial p `p` a
+
+-- | Alias for `initiate`
+absurd :: (HasInitialObject p) => forall a. Initial p `p` a
+absurd = initiate
+
+instance HasInitialObject Function where
+    type Initial Function = Void
+    initiate = \case {}
+
+instance HasInitialObject Entailment where
+    type Initial Entailment = Falsum
+    initiate = Entailment contradiction
diff --git a/src/Lude/Constraint/Falsum.hs b/src/Lude/Constraint/Falsum.hs
@@ -1,16 +1,10 @@
 module Lude.Constraint.Falsum (
     Falsum (..),
-    absurd,
 ) where
 
-import Lude.Constraint.Core
 import Lude.Kind
 
 --------------------------------------------------------------------------------
 
 type Falsum :: Constraint
 class Falsum where contradiction :: a
-
--- TODO: Generalize to initial objects for any category (also `never`?)
-absurd :: forall a. Falsum :- a
-absurd = Entailment contradiction
diff --git a/src/Lude/Constraint/Verum.hs b/src/Lude/Constraint/Verum.hs
@@ -1,6 +1,5 @@
 module Lude.Constraint.Verum (
     Verum,
-    trivial,
 ) where
 
 import Lude.Constraint.Core
@@ -15,7 +14,3 @@ instance Verum
 
 instance forall a. Witnesses a Verum where
     witness _ _ = Evidence
-
--- TODO: Generalize to terminal objects for any category (also `always`?)
-trivial :: forall a. a :- Verum
-trivial = Entailment Evidence
diff --git a/src/Lude/Unit.hs b/src/Lude/Unit.hs
@@ -1,6 +1,5 @@
 module Lude.Unit (
     Unit,
-    trivial,
 ) where
 
 import Prelude.Experimental (Unit)
@@ -8,7 +7,3 @@ import Prelude.Experimental (Unit)
 -- TODO: Instances
 
 --------------------------------------------------------------------------------
-
--- TODO: Generalize to terminal objects for any category
-trivial :: forall a. a -> Unit
-trivial _ = ()
diff --git a/src/Lude/Void.hs b/src/Lude/Void.hs
@@ -1,6 +1,5 @@
 module Lude.Void (
     Void,
-    absurd,
 ) where
 
 import Data.Void (Void)
@@ -8,7 +7,3 @@ import Data.Void (Void)
 -- TODO: Instances
 
 --------------------------------------------------------------------------------
-
--- TODO: Generalize to initial objects for any category
-absurd :: forall a. Void -> a
-absurd = \case {}