commit 459ae6ab64ab937751af969f91b9c03b09b1d4ce
parent 4c301d31006a7912a4d51d0b2ce91d4dcba71097
Author: Robert Russell <robert@rr3.xyz>
Date: Thu, 10 Sep 2026 17:56:39 -0700
Algebra.Category: rename Natural to Naturally
Diffstat:
9 files changed, 18 insertions(+), 18 deletions(-)
diff --git a/Todo/Category.hs b/Todo/Category.hs
@@ -63,7 +63,7 @@
-- instance Functorial Either where
-- type Dom Either = Function
-- type Cod Either = Function ==> Function
--- map f = Natural \case
+-- map f = Naturally \case
-- L x -> L (f x)
-- R y -> R y
diff --git a/Todo/Const.hs b/Todo/Const.hs
@@ -34,11 +34,11 @@ instance (Categorical p) => HasConstFunctor p Entailment where
instance (HasTerminalObject q, HasConstFunctor p q) => HasTerminalObject (NT p q) where
type Terminal (NT p q) = ConstOn p q (Terminal q)
- terminate @f = Natural \ @a -> mkConstOn @p . terminate \\ f `preservesObj` a
+ terminate @f = Naturally \ @a -> mkConstOn @p . terminate \\ f `preservesObj` a
instance (HasInitialObject q, HasConstFunctor p q) => HasInitialObject (NT p q) where
type Initial (NT p q) = ConstOn p q (Initial q)
- initiate @f = Natural \ @a -> initiate . unConstOn @p \\ f `preservesObj` a
+ initiate @f = Naturally \ @a -> initiate . unConstOn @p \\ f `preservesObj` a
test :: forall p f. (FunctorialOn p Entailment f) => NT p Entailment f (Tautology p Verum)
test = terminate
diff --git a/src/Lude/Algebra/Category/Algebra.hs b/src/Lude/Algebra/Category/Algebra.hs
@@ -43,7 +43,7 @@ class DefaultRecursive p f r where
instance (Coalgebraic Function f r) => DefaultRecursive Function f r where
defaultCata f = h where h = f . map h . peel
instance (Categorical p, Categorical q, Coalgebraic (p ==> q) f r) => DefaultRecursive (NT p q) f r where
- defaultCata f@(Natural _) = h where h = Natural (comp f . comp (map h) . comp peel) \\ witnessMor (wrap @(p ==> q) @f @r)
+ defaultCata f@(Naturally _) = h where h = Naturally (comp f . comp (map h) . comp peel) \\ witnessMor (wrap @(p ==> q) @f @r)
-- | A type equipped with an initial algebra for an endofunctor.
type Recursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
@@ -72,7 +72,7 @@ class DefaultCorecursive p g s where
instance (Algebraic Function g s) => DefaultCorecursive Function g s where
defaultAna g = h where h = wrap . map h . g
instance (Categorical p, Categorical q, Algebraic (p ==> q) g s) => DefaultCorecursive (p ==> q) g s where
- defaultAna g@(Natural _) = h where h = Natural (comp wrap . comp (map h) . comp g) \\ witnessMor (peel @(p ==> q) @g @s)
+ defaultAna g@(Naturally _) = h where h = Naturally (comp wrap . comp (map h) . comp g) \\ witnessMor (peel @(p ==> q) @g @s)
-- | A type equipped with a final coalgebra for an endofunctor.
type Corecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
diff --git a/src/Lude/Algebra/Category/Bifunctor.hs b/src/Lude/Algebra/Category/Bifunctor.hs
@@ -127,7 +127,7 @@ type Pair :: Type -> Type -> Type
data Pair a b = MkPair a b
instance Functorial (Pair a) where map f = \(MkPair x y) -> MkPair x (f y)
-instance Functorial Pair where map f = Natural \(MkPair x y) -> MkPair (f x) y
+instance Functorial Pair where map f = Naturally \(MkPair x y) -> MkPair (f x) y
instance SemigroupalFunctorial Pair where
assoc = MkIso to fro
diff --git a/src/Lude/Algebra/Category/Constrained.hs b/src/Lude/Algebra/Category/Constrained.hs
@@ -31,4 +31,4 @@ instance (Categorical p) => Functorial (Constrained c p a) where
instance (Categorical p) => Functorial (Constrained c p) where
type Dom (Constrained c p) = Dual (Constrained c p)
type Cod (Constrained c p) = (Constrained c p) ==> Function
- map (MkDual f) = Natural (. f)
+ map (MkDual f) = Naturally (. f)
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -97,7 +97,7 @@ instance (Categorical p) => Functorial (Dual p a) where
instance (Categorical p) => Functorial (Dual p) where
type Dom (Dual p) = Dual (Dual p)
type Cod (Dual p) = Dual p ==> Function
- map (MkDual f) = Natural (. f)
+ map (MkDual f) = Naturally (. f)
--------------------------------------------------------------------------------
-- Functors
@@ -141,7 +141,7 @@ preservesObj _ _ = preservesObj_
-- TODO: Add NT-like type *alias* (like ~> and :~, but with the Obj constraint)
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) => Natural {comp :: forall a. (Obj p a) => f a `q` g a}
+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 (==>) :: forall {i} {j}. Cat i -> Cat j -> Cat (i -> j)
type (==>) = NT
@@ -161,12 +161,12 @@ type family NTCod _ where
-- at _ m = comp m
instance NT p q f g `Witnesses` Mor (NT p q) f g where
- witness (Natural _) = MkEvidence
+ witness (Naturally _) = MkEvidence
instance (Categorical p, Categorical q) => Categorical (NT p q) where
type Obj (NT p q) = FunctorialOn p q
- identity @f = Natural \ @a -> identity \\ f `preservesObj` a
- compose (Natural a) (Natural b) = Natural (compose a b)
+ identity @f = Naturally \ @a -> identity \\ f `preservesObj` a
+ compose (Naturally a) (Naturally b) = Naturally (compose a b)
witnessMor = witness
instance (Categorical p, Categorical q) => Functorial (NT p q a) where
@@ -177,7 +177,7 @@ instance (Categorical p, Categorical q) => Functorial (NT p q a) where
instance (Categorical p, Categorical q) => Functorial (NT p q) where
type Dom (NT p q) = Dual (NT p q)
type Cod (NT p q) = NT p q ==> Function
- map (MkDual f) = Natural (. f)
+ map (MkDual f) = Naturally (. f)
--------------------------------------------------------------------------------
-- Haskell
@@ -194,7 +194,7 @@ instance Functorial (Function a) where
instance Functorial Function where
type Dom Function = Dual Function
type Cod Function = Function ==> Function
- map (MkDual f) = Natural (. f)
+ map (MkDual f) = Naturally (. f)
instance Categorical Entailment where
identity = identityEntailment
@@ -208,7 +208,7 @@ instance Functorial (Entailment a) where
instance Functorial Entailment where
type Dom Entailment = Dual Entailment
type Cod Entailment = Entailment ==> Function
- map (MkDual f) = Natural (. f)
+ map (MkDual f) = Naturally (. f)
instance Functorial Evidence where
type Dom Evidence = Entailment
diff --git a/src/Lude/Algebra/Category/Discrete.hs b/src/Lude/Algebra/Category/Discrete.hs
@@ -25,4 +25,4 @@ instance Functorial (Discrete a) where
instance Functorial Discrete where
type Dom Discrete = Dual Discrete
type Cod Discrete = Discrete ==> Function
- map (MkDual f) = Natural (. f)
+ map (MkDual f) = Naturally (. f)
diff --git a/src/Lude/Algebra/Category/Hom.hs b/src/Lude/Algebra/Category/Hom.hs
@@ -35,4 +35,4 @@ instance (Categorical p) => Functorial (Hom p a) where
instance (Categorical p) => Functorial (Hom p) where
type Dom (Hom p) = Dual (Hom p)
type Cod (Hom p) = Hom p ==> Function
- map (MkDual f) = Natural (. f)
+ map (MkDual f) = Naturally (. f)
diff --git a/src/Lude/Algebra/Category/Iso.hs b/src/Lude/Algebra/Category/Iso.hs
@@ -36,4 +36,4 @@ instance (Categorical p) => Functorial (Iso p a) where
instance (Categorical p) => Functorial (Iso p) where
type Dom (Iso p) = Dual (Iso p)
type Cod (Iso p) = Iso p ==> Function
- map (MkDual f) = Natural (. f)
+ map (MkDual f) = Naturally (. f)
