lude

commit 6a6bc2fced739398e38609dd0639600aae6ae5c4
parent 09b256dd8eba4800366607c20f9d632900be4a28
Author: Robert Russell <robert@rr3.xyz>
Date:   Mon, 14 Sep 2026 15:51:32 -0700

Haskell.Category: add binatural transformations

Diffstat:
M
src/Lude/Haskell/Category.hs
 | 
12
+++++++++++-

1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/src/Lude/Haskell/Category.hs b/src/Lude/Haskell/Category.hs
@@ -2,11 +2,13 @@ module Lude.Haskell.Category (
     Cat,
     Function,
     type (~>),
+    type (~~>),
     identityFunction,
     composeFunction,
     Entailment (..),
     (:-),
     (:~),
+    (:~~),
     identityEntailment,
     composeEntailment,
     --
@@ -59,7 +61,7 @@ import Lude.Haskell.Type
 
 --------------------------------------------------------------------------------
 
-infixr 1 ~>, :-, :~, :|=, :|-
+infixr 1 ~>, ~~>, :-, :~, :~~, :|=, :|-
 infixl 1 \\
 
 --------------------------------------------------------------------------------
@@ -77,6 +79,10 @@ type Function = (->)
 type (~>) :: forall i r. Cat (i -> Type @r)
 type f ~> g = forall x. f x -> g x
 
+-- | Binatural transformations to `Function`/`->`
+type (~~>) :: forall i j r. Cat (i -> j -> Type @r)
+type f ~~> g = forall x y. f x y -> g x y
+
 identityFunction :: forall a. a -> a
 identityFunction = Data.Function.id
 
@@ -95,6 +101,10 @@ type (:-) = Entailment
 type (:~) :: forall i. Cat (i -> Constraint)
 type f :~ g = forall x. f x :- g x
 
+-- | Binatural transformations to `Entailment`/`:-`
+type (:~~) :: forall i j. Cat (i -> j -> Constraint)
+type f :~~ g = forall x y. f x y :- g x y
+
 identityEntailment :: forall a. a :- a
 identityEntailment = Entail MkEvidence