lude

commit c51de6c4ed7d00cb31ae98967e2573af4f785a29
parent a07f4375ece67cad8086befcddeb67c3ee41e50c
Author: Robert Russell <robert@rr3.xyz>
Date:   Mon, 14 Sep 2026 14:28:58 -0700

Lude.Algebra.Category: add nmap

Diffstat:
M
src/Lude/Algebra/Category/Core.hs
 | 
6
++++++

1 file changed, 6 insertions(+), 0 deletions(-)
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -19,6 +19,7 @@ module Lude.Algebra.Category.Core (
     EndofunctorialOn,
     ObjArg,
     preservesObj,
+    nmap,
     --
     NT (..),
     type (==>),
@@ -142,11 +143,16 @@ type ObjArg f = Obj (Dom f)
 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
+nmap f = comp (map f)
+
 --------------------------------------------------------------------------------
 -- Natural Transformations
 
 -- TODO: Add NT-like type *alias* (like ~> and :~, but with the Obj constraint)
 
+-- TODO: Better name for comp, and infix alias
+
 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}