lude

commit 01719e7037df80215b5de677206f63e01c3b9b51
parent efb61710da76df73fd3edd4122942495aeb11c88
Author: Robert Russell <robert@rr3.xyz>
Date:   Mon,  5 Oct 2026 09:51:37 -0700

Algebra.Category.Bifunctor: add Binaturally and bicomp

Diffstat:
M
src/Lude/Algebra/Category/Bifunctor.hs
 | 
36
++++++++++++++++++++++++++++++++++++

1 file changed, 36 insertions(+), 0 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,
+    pattern Binaturally,
+    bicomp,
 ) where
 
 import Lude.Algebra.Category.Core
@@ -76,6 +78,40 @@ rmap rf = map rf \\ f `preservesObj` l
 
 --------------------------------------------------------------------------------
 
+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}
+
+toBiNT'
+    :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) (f :: i -> j -> k) (g :: i -> j -> k)
+     . (Categorical p, Categorical q, Categorical r)
+    => NT p (NT q r) f g
+    -> BiNT' p q r f g
+toBiNT' (Naturally m) = Binaturally' \ @a @b -> comp (m @a) @b
+
+ofBiNT'
+    :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) (f :: i -> j -> k) (g :: i -> j -> k)
+     . (Categorical p, Categorical q, Categorical r)
+    => BiNT' p q r f g
+    -> NT p (NT q r) f g
+ofBiNT' (Binaturally' m) = Naturally \ @a -> Naturally m \\ f `preservesObj` a \\ g `preservesObj` a
+
+pattern Binaturally
+    :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) (f :: i -> j -> k) (g :: i -> j -> k)
+     . (Categorical p, Categorical q, Categorical r)
+    => (BifunctorialOn p q r f, BifunctorialOn p q r g)
+    => (forall (a :: i) (b :: j). (Obj p a, Obj q b) => f a b `r` g a b)
+    -> NT p (NT q r) f g
+pattern Binaturally n <- (toBiNT' -> Binaturally' n) where Binaturally n = ofBiNT' (Binaturally' n)
+{-# COMPLETE Binaturally #-}
+
+bicomp
+    :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) (f :: i -> j -> k) (g :: i -> j -> k)
+     . NT p (NT q r) f g
+    -> (forall (a :: i) (b :: j). (Obj p a, Obj q b) => f a b `r` g a b)
+bicomp m = comp (comp m)
+
+--------------------------------------------------------------------------------
+
 -- | A semigroup structure on a category, represented as a bifunctor
 --
 -- TODO: Laws