lude

commit 875475640b6b2c214134966ad4c95f7065d9de81
parent 02d083d8977a8522a1d5909dcacefd027f831af5
Author: Robert Russell <robert@rr3.xyz>
Date:   Sun, 22 Mar 2026 00:44:42 -0700

Rename Ob to Obj

Diffstat:
M
src/Lude/Algebra/Category.hs
 | 
58
+++++++++++++++++++++++++++++-----------------------------
A
src/Lude/These.hs
 | 
7
+++++++

2 files changed, 36 insertions(+), 29 deletions(-)
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -22,9 +22,9 @@ type Cat i = i -> i -> Type
 
 type Category :: forall i. Cat i -> Constraint
 class Category (p :: Cat i) where
-    type Ob p :: Constraint1 i
-    type Ob p = Always1
-    identity :: (Ob p a) => p a a
+    type Obj p :: Constraint1 i
+    type Obj p = Always1
+    identity :: (Obj p a) => p a a
     compose :: p b c -> p a b -> p a c
 
 --------------------------------------------------------------------------------
@@ -42,16 +42,16 @@ type Prod :: forall i j. Cat i -> Cat j -> Cat (i × j)
 data Prod p q a b where
     Prod :: p a0 b0 -> q a1 b1 -> Prod p q '(a0, a1) '(b0, b1)
 
--- We could simplify this, but this way it's consistent with SumOb.
-type ProdOb :: forall i j. Cat i -> Cat j -> Constraint1 (i × j)
-class ProdOb p q a where
-    prodOb :: Pair1 (Evidence1 (Ob p)) (Evidence1 (Ob q)) a
-instance (Ob p i, Ob q j) => ProdOb p q '(i, j) where
-    prodOb = Pair1 Evidence1 Evidence1
+-- We could simplify this, but this way it's consistent with SumObj.
+type ProdObj :: forall i j. Cat i -> Cat j -> Constraint1 (i × j)
+class ProdObj p q a where
+    prodObj :: Pair1 (Evidence1 (Obj p)) (Evidence1 (Obj q)) a
+instance (Obj p i, Obj q j) => ProdObj p q '(i, j) where
+    prodObj = Pair1 Evidence1 Evidence1
 
 instance (Category p, Category q) => Category (Prod p q) where
-    type Ob (Prod p q) = ProdOb p q
-    identity @a = case prodOb @_ @_ @p @q @a of
+    type Obj (Prod p q) = ProdObj p q
+    identity @a = case prodObj @_ @_ @p @q @a of
         Pair1 Evidence1 Evidence1 -> Prod identity identity
     compose (Prod f0 f1) (Prod g0 g1) = Prod (compose f0 g0) (compose f1 g1)
 
@@ -62,17 +62,17 @@ data Sum p q a b where
     SumL :: p a b -> Sum p q (L a) (L b)
     SumR :: q a b -> Sum p q (R a) (R b)
 
-type SumOb :: forall i j. Cat i -> Cat j -> Constraint1 (i + j)
-class SumOb p q a where
-    sumOb :: Either1 (Evidence1 (Ob p)) (Evidence1 (Ob q)) a
-instance (Ob p a) => SumOb p q (L a) where
-    sumOb = L1 Evidence1
-instance (Ob q a) => SumOb p q (R a) where
-    sumOb = R1 Evidence1
+type SumObj :: forall i j. Cat i -> Cat j -> Constraint1 (i + j)
+class SumObj p q a where
+    sumObj :: Either1 (Evidence1 (Obj p)) (Evidence1 (Obj q)) a
+instance (Obj p a) => SumObj p q (L a) where
+    sumObj = L1 Evidence1
+instance (Obj q a) => SumObj p q (R a) where
+    sumObj = R1 Evidence1
 
 instance (Category p, Category q) => Category (Sum p q) where
-    type Ob (Sum p q) = SumOb p q
-    identity @a = case sumOb @_ @_ @p @q @a of
+    type Obj (Sum p q) = SumObj p q
+    identity @a = case sumObj @_ @_ @p @q @a of
         L1 Evidence1 -> SumL identity
         R1 Evidence1 -> SumR identity
     compose (SumL f) (SumL g) = SumL (compose f g)
@@ -82,15 +82,15 @@ instance (Category p, Category q) => Category (Sum p q) where
 
 type Nt :: forall i j. Cat i -> Cat j -> Cat (i -> j)
 newtype Nt p q f g where
-    Nt :: (forall a. (Ob p a) => q (f a) (g a)) -> Nt p q f g
+    Nt :: (forall a. (Obj p a) => q (f a) (g a)) -> Nt p q f g
 
-type NtOb :: Cat i -> Cat j -> (i -> j) -> Constraint
-class (Functor f, Dom f ~ p, Cod f ~ q) => NtOb p q f
-instance (Functor f, Dom f ~ p, Cod f ~ q) => NtOb p q f
+type NtObj :: Cat i -> Cat j -> (i -> j) -> Constraint
+class (Functor f, Dom f ~ p, Cod f ~ q) => NtObj p q f
+instance (Functor f, Dom f ~ p, Cod f ~ q) => NtObj p q f
 
 instance (Category p, Category q) => Category (Nt p q) where
-    type Ob (Nt p q) = NtOb p q
-    identity @f = Nt \ @a -> identity `because` (preserveOb :: Ob p a :- Ob q (f a))
+    type Obj (Nt p q) = NtObj p q
+    identity @f = Nt \ @a -> identity `because` (preserveObj :: Obj p a :- Obj q (f a))
     compose (Nt a) (Nt b) = Nt (compose a b)
 
 --------------------------------------------------------------------------------
@@ -106,9 +106,9 @@ class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
     type Cod f :: Cat j
     type Cod f = DefaultCat
 
-    preserveOb :: Ob (Dom f) a :- Ob (Cod f) (f a)
-    default preserveOb :: (Ob (Cod f) ~ Always1) => Ob (Dom f) a :- Ob (Cod f) (f a)
-    preserveOb = always1
+    preserveObj :: Obj (Dom f) a :- Obj (Cod f) (f a)
+    default preserveObj :: (Obj (Cod f) ~ Always1) => Obj (Dom f) a :- Obj (Cod f) (f a)
+    preserveObj = always1
 
     map :: Dom f a b -> Cod f (f a) (f b)
 
diff --git a/src/Lude/These.hs b/src/Lude/These.hs
@@ -0,0 +1,7 @@
+module Lude.These (
+
+) where
+
+-- TODO
+
+--------------------------------------------------------------------------------