lude

commit 745933b8b13cf4c99883b4437e6ad58c284d3671
parent 54e567bd598043672529bafca8d9d586e1e9d1e4
Author: Robert Russell <robert@rr3.xyz>
Date:   Fri,  9 Oct 2026 11:51:55 -0700

Algebra.Category: add NT_ and BiNT_

Diffstat:
M
src/Lude/Algebra/Category/Bifunctor.hs
 | 
7
++++++-
M
src/Lude/Algebra/Category/Core.hs
 | 
17
++++++++++-------

2 files changed, 16 insertions(+), 8 deletions(-)
diff --git a/src/Lude/Algebra/Category/Bifunctor.hs b/src/Lude/Algebra/Category/Bifunctor.hs
@@ -11,6 +11,8 @@ module Lude.Algebra.Category.Bifunctor (
     bimap,
     lmap,
     rmap,
+    --
+    BiNT_,
     pattern Binaturally,
     bicomp,
     ($^^),
@@ -84,8 +86,11 @@ rmap rf = map rf \\ f `preservesObj` l
 
 --------------------------------------------------------------------------------
 
+type BiNT_ :: forall i j k. Cat i -> Cat j -> Cat k -> Cat (i -> j -> k)
+type BiNT_ @i @j p q r f g = forall (x :: i) (y :: j). (Obj p x, Obj q y) => f x y `r` g x y
+
 type BiNT' :: forall {i} {j} {k}. Cat i -> Cat j -> Cat k -> Cat (i -> j -> k)
-data BiNT' p q r f g = (BifunctorialOn p q r f, BifunctorialOn p q r g) => Binaturally' {bicomp' :: forall a b. (Obj p a, Obj q b) => f a b `r` g a b}
+data BiNT' p q r f g = (BifunctorialOn p q r f, BifunctorialOn p q r g) => Binaturally' {bicomp' :: BiNT_ p q r f g}
 
 toBiNT'
     :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) (f :: i -> j -> k) (g :: i -> j -> k)
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -21,6 +21,7 @@ module Lude.Algebra.Category.Core (
     preservesObj,
     nmap,
     --
+    NT_,
     NT (..),
     type (==>),
     NTDom,
@@ -153,27 +154,29 @@ preservesObj
     ->Obj p a :- Obj q (f a)
 preservesObj _ _ = preservesObj_
 
+-- TODO: Is this named correctly? Should it be "map1"?
 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
 nmap f = comp (map f)
 
 --------------------------------------------------------------------------------
 -- Natural Transformations
 
--- TODO: Add NT-like type *alias* (like ~> and :~, but with the Obj constraint)
+-- TODO: Better names for all this
 
--- TODO: Better name for comp, and infix alias
+type NT_ :: forall i j. Cat i -> Cat j -> Cat (i -> j)
+type NT_ @i p q f g = forall (x :: i). (Obj p x) => f x `q` g x
 
-type NT :: forall {i} {j}. Cat i -> Cat j -> Cat (i -> j)
-data NT p q f g = (FunctorialOn p q f, FunctorialOn p q g) => Naturally {comp :: forall a. (Obj p a) => f a `q` g a}
+type NT :: forall i j. Cat i -> Cat j -> Cat (i -> j)
+data NT p q f g = (FunctorialOn p q f, FunctorialOn p q g) => Naturally {comp :: NT_ p q f g}
 
-type (==>) :: forall {i} {j}. Cat i -> Cat j -> Cat (i -> j)
+type (==>) :: forall i j. Cat i -> Cat j -> Cat (i -> j)
 type (==>) = NT
 
-type NTDom :: forall {i} {j}. Cat (i -> j) -> Cat i
+type NTDom :: forall i j. Cat (i -> j) -> Cat i
 type family NTDom _ where
     NTDom (NT p q) = p
 
-type NTCod :: forall {i} {j}. Cat (i -> j) -> Cat j
+type NTCod :: forall i j. Cat (i -> j) -> Cat j
 type family NTCod _ where
     NTCod (NT p q) = q