lude

commit 2ddecefe35c1321a67e88cfd3b6515f7c2dce5f8
parent 1526357302ee8f276421363b7d7387de52c71041
Author: Robert Russell <robert@rr3.xyz>
Date:   Sun,  6 Sep 2026 20:49:22 -0700

Algebra.Category: simplify preserveObj

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

1 file changed, 1 insertion(+), 16 deletions(-)
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -10,7 +10,6 @@ module Lude.Algebra.Category.Core (
     Mor,
     (.),
     --
-    DefaultFunctorial (..),
     Functorial (..),
     FunctorialOn,
     Endofunctorial,
@@ -81,19 +80,6 @@ instance (Obj p a, Obj p b) => Mor p a b
 --------------------------------------------------------------------------------
 -- Functors
 
-type DefaultFunctorial :: forall {i} {j}. Cat i -> Cat j -> (i -> j) -> Constraint
-class DefaultFunctorial p q f where
-    defaultPreserveObj :: (Functorial f, Dom f ~ p, Cod f ~ q) => forall a. Obj p a :- Obj q (f a)
-
--- TODO: Should these be incoherent?
-instance DefaultFunctorial p Function f where
-    defaultPreserveObj = always
-instance DefaultFunctorial p Entailment f where
-    defaultPreserveObj = always
-
--- instance (forall a. (Obj p a) => FunctorialOn q r (f a)) => DefaultFunctorial p (Nt q r) f where
---     defaultPreserveObj = entails
-
 type Functorial :: forall {i} {j}. (i -> j) -> Constraint
 class (Categorical (Dom f), Categorical (Cod f)) => Functorial (f :: i -> j) where
     type Dom f :: Cat i
@@ -105,8 +91,7 @@ class (Categorical (Dom f), Categorical (Cod f)) => Functorial (f :: i -> j) whe
     map :: forall a b. Dom f a b -> Cod f (f a) (f b)
 
     preserveObj :: forall a. Obj (Dom f) a :- Obj (Cod f) (f a)
-    default preserveObj :: (DefaultFunctorial (Dom f) (Cod f) f) => forall a. Obj (Dom f) a :- Obj (Cod f) (f a)
-    preserveObj = defaultPreserveObj
+    preserveObj = MkEntailment (MkEvidence \\ witnessMor (map @f (identity :: Dom f a a)))
 
 type FunctorialOn :: forall {k} {l}. Cat k -> Cat l -> (k -> l) -> Constraint
 class (Functorial f, Dom f ~ p, Cod f ~ q) => FunctorialOn p q f | f -> p q