commit b91992333672bdeaf9c6749b62ded2023baac0e4
parent ee026033bc4bcc8e78989a739eeffa085c8369db
Author: Robert Russell <robert@rr3.xyz>
Date: Wed, 9 Sep 2026 17:31:48 -0700
Algebra.Category.Bifunctor: add class aliases
Diffstat:
2 files changed, 33 insertions(+), 27 deletions(-)
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -21,6 +21,6 @@ import Lude.Algebra.Category.Terminal as X
-- TODO: Eilenberg-Moore (co)algebras?
--- TODO: Bifunctors? Profunctors? Etc... (other kinds of functors?)
--- That would allow being a functor in multiple ways (without losing coherence).
+-- TODO: Profunctors? Other special kinds of functors, given distinct names?
+-- That would allow being a functor in multiple ways without losing coherence.
-- E.g., lists could be mappable "normally" and filterable (choose is map).
diff --git a/src/Lude/Algebra/Category/Bifunctor.hs b/src/Lude/Algebra/Category/Bifunctor.hs
@@ -23,42 +23,48 @@ import Lude.Haskell
-- some reason the constraint solver can't safely deduce that.
type Bifunctorial :: forall {i} {j} {k}. (i -> j -> k) -> Constraint
-class (Functorial p, Cod p ~ NT (BidomR p) (Bicod p), Categorical (BidomR p), Categorical (Bicod p)) => Bifunctorial p
-instance (Functorial p, Cod p ~ NT (BidomR p) (Bicod p), Categorical (BidomR p), Categorical (Bicod p)) => Bifunctorial p
+class (Functorial f, Cod f ~ NT (BidomR f) (Bicod f), Categorical (BidomR f), Categorical (Bicod f)) => Bifunctorial f
+instance (Functorial f, Cod f ~ NT (BidomR f) (Bicod f), Categorical (BidomR f), Categorical (Bicod f)) => Bifunctorial f
+
+type BifunctorialOn :: forall {i} {j} {k}. Cat i -> Cat j -> Cat k -> (i -> j -> k) -> Constraint
+class (Bifunctorial f, BidomL f ~ p, BidomR f ~ q, Bicod f ~ r) => BifunctorialOn p q r f
+instance (Bifunctorial f, BidomL f ~ p, BidomR f ~ q, Bicod f ~ r) => BifunctorialOn p q r f
+
+type Biendofunctorial :: forall {i}. Biendo i -> Constraint
+class (Bifunctorial f, BidomL f ~ BidomR f, BidomR f ~ Bicod f) => Biendofunctorial f
+instance (Bifunctorial f, BidomL f ~ BidomR f, BidomR f ~ Bicod f) => Biendofunctorial f
+
+type BiendofunctorialOn :: forall {i}. Cat i -> Biendo i -> Constraint
+class (BifunctorialOn p p p f) => BiendofunctorialOn p f
+instance (BifunctorialOn p p p f) => BiendofunctorialOn p f
type BidomL :: forall {i} {j} {k}. (i -> j -> k) -> Cat i
-type BidomL p = Dom p
+type BidomL f = Dom f
type BidomR :: forall {i} {j} {k}. (i -> j -> k) -> Cat j
-type BidomR p = NTDom (Cod p)
+type BidomR f = NTDom (Cod f)
type Bicod :: forall {i} {j} {k}. (i -> j -> k) -> Cat k
-type Bicod p = NTCod (Cod p)
+type Bicod f = NTCod (Cod f)
bimap
- :: forall {i} {j} {k} (p :: i -> j -> k) la lb ra rb
- . (Bifunctorial p)
- => BidomL p la lb
- -> BidomR p ra rb
- -> Bicod p (p la ra) (p lb rb)
+ :: forall {i} {j} {k} (f :: i -> j -> k) la lb ra rb
+ . (Bifunctorial f)
+ => BidomL f la lb
+ -> BidomR f ra rb
+ -> Bicod f (f la ra) (f lb rb)
bimap lf rf = (lmap lf \\ witnessMor rf) . (rmap rf \\ witnessMor lf)
lmap
- :: forall {i} {j} {k} (p :: i -> j -> k) la lb r
- . (Bifunctorial p, Obj (BidomR p) r)
- => BidomL p la lb
- -> Bicod p (p la r) (p lb r)
+ :: forall {i} {j} {k} (f :: i -> j -> k) la lb r
+ . (Bifunctorial f, Obj (BidomR f) r)
+ => BidomL f la lb
+ -> Bicod f (f la r) (f lb r)
lmap lf = comp (map lf)
rmap
- :: forall {i} {j} {k} (p :: i -> j -> k) l ra rb
- . (Bifunctorial p, Obj (BidomL p) l)
- => BidomR p ra rb
- -> Bicod p (p l ra) (p l rb)
-rmap rf = map rf \\ p `preservesObj` l
-
---------------------------------------------------------------------------------
-
-type Homfunctorial :: forall {i}. (Cat i) -> Constraint
-class (Categorical p, Bifunctorial p, BidomL p ~ Dual p, BidomR p ~ p, Bicod p ~ Function) => Homfunctorial p
-instance (Categorical p, Bifunctorial p, BidomL p ~ Dual p, BidomR p ~ p, Bicod p ~ Function) => Homfunctorial p
+ :: forall {i} {j} {k} (f :: i -> j -> k) l ra rb
+ . (Bifunctorial f, Obj (BidomL f) l)
+ => BidomR f ra rb
+ -> Bicod f (f l ra) (f l rb)
+rmap rf = map rf \\ f `preservesObj` l
