lude

commit 05d8beadfe3a415754aad808574bf9dd89f776c1
parent 80510bab67d9a8e0a48ecd03c88bf1917c58ad7a
Author: Robert Russell <robert@rr3.xyz>
Date:   Tue, 10 Mar 2026 23:53:04 -0700

Add more ideas

Diffstat:
M
src/Lude/Algebra/Category.hs
 | 
25
++++++++++++++++++-------

1 file changed, 18 insertions(+), 7 deletions(-)
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -25,6 +25,12 @@ type Pair1 :: forall i j. Type1 i -> Type1 j -> Type1 (i × j)
 data Pair1 p q a where
     Pair1 :: p a0 -> q a1 -> Pair1 p q '(a0, a1)
 
+fst1 :: Pair1 p q '(i, j) -> p i
+fst1 (Pair1 x _) = x
+
+snd1 :: Pair1 p q '(i, j) -> q j
+snd1 (Pair1 _ y) = y
+
 type (×^) = Pair1
 infixl 7 ×^
 
@@ -73,15 +79,16 @@ instance Category Hask where
 
 --------------------------------------------------------------------------------
 
-type ProdOb :: Cat i -> Cat j -> i × j -> Constraint
-class ProdOb p q a where
-    prodOb :: PairEvidence1 (Ob p) (Ob q) a
-instance (Ob p i, Ob q j) => ProdOb p q '(i, j) where
-    prodOb = Pair1 Evidence1 Evidence1
+-- type ProdOb :: Cat i -> Cat j -> i × j -> Constraint
+-- class ProdOb p q a where
+--     prodOb :: PairEvidence1 (Ob p) (Ob q) a
+-- instance (Ob p i, Ob q j) => ProdOb p q '(i, j) where
+--     prodOb = Pair1 Evidence1 Evidence1
 
 instance (Category p, Category q) => Category (p ×^^ q) where
-    type Ob (p ×^^ q) = ProdOb p q
-    identity @a = case prodOb @_ @_ @p @q @a of
+    -- type Ob (p ×^^ q) = ProdOb p q
+    type Ob (p ×^^ q) = HasPairEvidence1 (Ob p) (Ob q)
+    identity @a = case pairEvidence @_ @_ @(Ob p) @(Ob q) @a of
         Pair1 Evidence1 Evidence1 -> Pair2 identity identity
     compose (Pair2 f0 f1) (Pair2 g0 g1) = Pair2 (compose f0 g0) (compose f1 g1)
 
@@ -118,6 +125,10 @@ data Evidence1 p a = (p a) => Evidence1
 type PairEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Type1 (i × j)
 type PairEvidence1 p q = Pair1 (Evidence1 p) (Evidence1 q)
 
+type HasPairEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Constraint1 (i × j)
+class HasPairEvidence1 p q a where
+    pairEvidence :: PairEvidence1 p q a
+
 -- TODO: pattern
 
 type EitherEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Type1 (i + j)