lude

commit f9b36d26aad0e50d184854ea96098c8879bc4155
parent 811fe1fb26404329d105b547b7ea968ac32c6f04
Author: Robert Russell <robert@rr3.xyz>
Date:   Mon,  5 Oct 2026 10:01:00 -0700

Clean up

Diffstat:
M
src/Lude/Algebra/Category/Core.hs
 | 
15
+++++++--------
M
src/Lude/Function.hs
 | 
47
+----------------------------------------------

2 files changed, 8 insertions(+), 54 deletions(-)
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -143,7 +143,12 @@ type ObjArg f = Obj (Dom f)
 
 -- for :: forall {i} {j} (f :: i -> j) (a :: i) (b :: i). (Functorial f) => Dom f i j -> Cod f (f i) (f j)
 
-preservesObj :: forall {i} {j} (p :: Cat i) (q :: Cat j). forall (f :: i -> j) -> (FunctorialOn p q f) => forall (a :: i) -> Obj p a :- Obj q (f a)
+preservesObj
+    :: forall {i} {j} (p :: Cat i) (q :: Cat j)
+     . forall (f :: i -> j)
+    ->(FunctorialOn p q f)
+    => forall (a :: i)
+    ->Obj p a :- Obj q (f a)
 preservesObj _ _ = preservesObj_
 
 nmap :: forall {i} {j} {p :: Cat i} {q :: Cat j} (f :: i -> (j -> Type)) (a :: i) (b :: i). (FunctorialOn p (NT q Function) f) => (a `p` b) -> forall x. (Obj q x) => f a x -> f b x
@@ -170,12 +175,6 @@ type NTCod :: forall {i} {j}. Cat (i -> j) -> Cat j
 type family NTCod _ where
     NTCod (NT p q) = q
 
--- type TNT :: forall {i} r s. Cat i -> Cat (i -> Type @r)
--- type TNT p = NT p Function
-
--- at :: forall {i} {j} (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j). forall (a :: i) -> (Obj p a) => Nt p q f g -> f a `q` g a
--- at _ m = comp m
-
 instance NT p q f g `Witnesses` Mor (NT p q) f g where
     witness (Naturally _) = MkEvidence
 
@@ -216,7 +215,7 @@ instance Categorical Entailment where
     identity = identityEntailment
     compose = composeEntailment
 
-instance Functorial (Entailment a) where
+instance forall (a :: Constraint). Functorial (Entailment a) where
     type Dom (Entailment a) = Entailment
     type Cod (Entailment a) = Function
     map = compose
diff --git a/src/Lude/Function.hs b/src/Lude/Function.hs
@@ -58,7 +58,7 @@ const = lam2# \x _ -> x
 
 flip
     :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s) {t :: Repr} (c :: Type# t)
-     . (Functional# r, Functional# s) => (a -> b -> c) -> (b -> a -> c)
+     . (Functional# r, Functional# s) => (b -> a -> c) -> (a -> b -> c)
 flip f = lam2# \y x -> app2# f x y
 {-# INLINE flip #-}
 
@@ -145,48 +145,3 @@ compose11 = compose11#
 (*.*) = compose11
 {-# INLINE compose11 #-}
 {-# INLINE (*.*) #-}
-
--- compose02,
---     (.**)
---         :: forall {r0 :: Repr} (a0 :: Type# r0) {r1 :: Repr} (a1 :: Type# r1) {r2 :: Repr} (a2 :: Type# r2) {s :: Repr} (b :: Type# s) {t :: Repr} (c :: Type# t)
---          . (Functional# r0, Functional# r1, Functional# r2, Functional# s) => (b -> c) -> (a0 -> a1 -> a2 -> b) -> (a0 -> a1 -> a2 -> c)
--- compose02 g f = lam# \x -> compose01 g (f `app#` x)
--- (.**) = compose02
--- {-# INLINE compose02 #-}
--- {-# INLINE (.**) #-}
-
--- compose12,
---     (*.**)
---         :: forall {r0 :: Repr} (a0 :: Type# r0) {r1 :: Repr} (a1 :: Type# r1) {r2 :: Repr} (a2 :: Type# r2) {s0 :: Repr} (b0 :: Type# s0) {s :: Repr} (b :: Type# s) {t :: Repr} (c :: Type# t)
---          . (Functional# r0, Functional# r1, Functional# r2, Functional# s0, Functional# s) => (b0 -> b -> c) -> (a0 -> a1 -> a2 -> b) -> (b0 -> a0 -> a1 -> a2 -> c)
--- compose12 g f = lam# \y -> compose02 (g `app#` y) f
--- (*.**) = compose12
--- {-# INLINE compose12 #-}
--- {-# INLINE (*.**) #-}
-
--- compose20,
---     (**.)
---         :: forall {r0 :: Repr} (a0 :: Type# r0) {s0 :: Repr} (b0 :: Type# s0) {s1 :: Repr} (b1 :: Type# s1) {s :: Repr} (b :: Type# s) {t :: Repr} (c :: Type# t)
---          . (Functional# r0, Functional# s0, Functional# s1, Functional# s) => (b0 -> b1 -> b -> c) -> (a0 -> b) -> (b0 -> b1 -> a0 -> c)
--- compose20 g f = lam# \y -> compose10 (g `app#` y) f
--- (**.) = compose20
--- {-# INLINE compose20 #-}
--- {-# INLINE (**.) #-}
-
--- compose21,
---     (**.*)
---         :: forall {r0 :: Repr} (a0 :: Type# r0) {r1 :: Repr} (a1 :: Type# r1) {s0 :: Repr} (b0 :: Type# s0) {s1 :: Repr} (b1 :: Type# s1) {s :: Repr} (b :: Type# s) {t :: Repr} (c :: Type# t)
---          . (Functional# r0, Functional# r1, Functional# s0, Functional# s1, Functional# s) => (b0 -> b1 -> b -> c) -> (a0 -> a1 -> b) -> (b0 -> b1 -> a0 -> a1 -> c)
--- compose21 g f = lam# \y -> compose11 (g `app#` y) f
--- (**.*) = compose21
--- {-# INLINE compose21 #-}
--- {-# INLINE (**.*) #-}
-
--- compose22,
---     (**.**)
---         :: forall {r0 :: Repr} (a0 :: Type# r0) {r1 :: Repr} (a1 :: Type# r1) {r2 :: Repr} (a2 :: Type# r2) {s0 :: Repr} (b0 :: Type# s0) {s1 :: Repr} (b1 :: Type# s1) {s :: Repr} (b :: Type# s) {t :: Repr} (c :: Type# t)
---          . (Functional# r0, Functional# r1, Functional# r2, Functional# s0, Functional# s1, Functional# s) => (b0 -> b1 -> b -> c) -> (a0 -> a1 -> a2 -> b) -> (b0 -> b1 -> a0 -> a1 -> a2 -> c)
--- compose22 g f = lam# \y -> compose12 (g `app#` y) f
--- (**.**) = compose22
--- {-# INLINE compose22 #-}
--- {-# INLINE (**.**) #-}