Splitting off levels of generality by morality.

README.md

@@ -1 +1,34 @@
 # monoids-in-the-categoy-of-endofunctors
+
+Abstract nonsense in Haskell: category theory, recursion schemes, dependent data types, etc.
+The current version only contains category theory.
+
+## Category theory morality
+Each morality level re-defines the typeclasses of the level before it in a more general way.
+This generality comes at the cost of the typeclasses being more difficult to understand and use, which is why the excessively general, incomprehensible, and virtually unusable stuff is called 'evil'.
+
+### Good
+The 'good' alignment contains more-or-less standard Haskell that any Haskeller should be able to understand.
+It works exclusively in the category of types.
+
+### Neutral
+The 'neutral' alignment is more abstract, and allows working with categories other than Type.
+This generalization lets us speak of functors which are not endofunctors, the category of constraints or equality, etc..
+
+In this case a category is defined by a hom, and its objects are any value of the type the hom operates on.
+(This is perhaps a confusing wording; as an example, the category defined by `->` has *all* types as objects.)
+
+Here's some stuff we can talk about in neutral but not good:
+* Categories, monoidal categories, and enriched categories.
+* Functors which are not endofunctors (such as `:-`).
+* Natural transformations.
+* Monoids in categories other than Type.
+
+### Evil
+The 'evil' alignment generalizes categories to be defined both by a hom *and* a constraint restricting its objects.
+This broadens what we are allowed to do a *lot*, but Haskell is *really* not meant to be used in this way,
+making actually *doing* these things and using the resultant APIs extremely difficult.
+
+Here are some new things we can describe in evil:
+* `Set` can now finally get a functor instance: it is an endofunctor in the category of ordered types.
+* Monads are directly defined as monoid objects in the monoidal category of endofunctors, rather than as their own special typeclass. (Monad is still available as a convenient alias.)

monoids-in-the-categoy-of-endofunctors.cabal

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 3a1a51f201a4bf26bb1002122fc79d0d4bb421ec1c4f5f4ba69125a18f1444b4
+-- hash: 70278e7afaa766a9a15b6541432b72444f2618e64de1d91dfe39d0af0da80aa7
 
 name:           monoids-in-the-categoy-of-endofunctors
 version:        0.1.0.0
@@ -26,18 +26,18 @@ source-repository head
 
 library
   exposed-modules:
-      Category
-      Category.Applicative
-      Category.Constraint
-      Category.Functor
-      Category.Monoid
-      Category.NaturalTransformation
-      Category.Semigroup
+      Category.Evil
+      Category.Good
+      Category.Neutral
+      Category.Neutral.Enriched
+      Category.Neutral.NaturalTransformation
+      Data.Dict
   other-modules:
       Paths_monoids_in_the_categoy_of_endofunctors
   hs-source-dirs:
       src
-  default-extensions: BlockArguments ConstraintKinds FlexibleContexts FlexibleInstances GADTs InstanceSigs MultiParamTypeClasses NoImplicitPrelude PolyKinds QuantifiedConstraints RankNTypes ScopedTypeVariables TypeApplications TypeFamilies TypeOperators
+  default-extensions: BlockArguments ConstraintKinds DataKinds FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs MultiParamTypeClasses NoImplicitPrelude ScopedTypeVariables TypeApplications TypeFamilies TypeOperators Safe
+  ghc-options: -Weverything -Wno-missing-export-lists -Wno-missing-import-lists
   build-depends:
       base >=4.13 && <5
   default-language: Haskell2010

package.yaml

@@ -14,19 +14,26 @@ description:         Please see the README on GitHub at <https://github.com/jame
 default-extensions:
 - BlockArguments
 - ConstraintKinds
+- DataKinds
 - FlexibleContexts
 - FlexibleInstances
+- FunctionalDependencies
 - GADTs
+- ImportQualifiedPost
 - InstanceSigs
 - MultiParamTypeClasses
 - NoImplicitPrelude
-- PolyKinds
-- QuantifiedConstraints
-- RankNTypes
 - ScopedTypeVariables
 - TypeApplications
 - TypeFamilies
 - TypeOperators
+- Safe
+
+ghc-options:
+- -Weverything
+#- -Werror
+- -Wno-missing-export-lists
+- -Wno-missing-import-lists
 
 dependencies:
 - base >= 4.13 && < 5

src/Category.hs

@@ -1,72 +0,0 @@
-{-# LANGUAGE UndecidableSuperClasses #-}
-module Category where
-
-import Data.Kind (Constraint)
-
-data Dict c where
-    Dict :: c => Dict c
-
-data Proxy a where
-    Proxy :: Proxy a
-
-newtype Identity a = Identity { getIdentity :: a }
-
-class Category (hom :: k -> k -> *) (obj :: k -> Constraint) where
-    identity :: obj a => proxy obj -> a `hom` a
-    compose :: (obj a, obj b, obj c) => proxy obj -> b `hom` c -> a `hom` b -> a `hom` c
-
-instance Category (->) obj where
-    identity _ x = x
-    compose _ f g x = f (g x)
-
-class MonoidalObjects (obj :: k -> Constraint) where
-    type Unit obj :: k
-    type Product obj :: k -> k -> k
-
-instance MonoidalObjects (obj :: * -> Constraint) where
-    type Unit obj = ()
-    type Product obj = (,)
-
-class MonoidalObjects obj => ContainsMonoidalObjects obj where
-    unitObj :: Dict (obj (Unit obj))
-    productObjFactor :: (obj a, obj b) => Dict (obj (Product obj a b))
-    productObjDistribute :: obj (Product obj a b) => Dict (obj a, obj b)
-
-class EveryC a
-instance EveryC a
-
-instance ContainsMonoidalObjects (EveryC :: * -> Constraint) where
-    unitObj = Dict
-    productObjFactor = Dict
-    productObjDistribute = Dict
-
-class (Category hom obj, ContainsMonoidalObjects obj) => MonoidalCategory (hom :: k -> k -> *) (obj :: k -> Constraint) where
-    idLI :: obj a => proxy obj -> a `hom` Product obj a (Unit obj)
-    idLE :: obj a => proxy obj -> Product obj a (Unit obj) `hom` a
-    idRI :: obj a => proxy obj -> a `hom` Product obj (Unit obj) a
-    idRE :: obj a => proxy obj -> Product obj (Unit obj) a `hom` a
-
-    assocL :: (obj a, obj b, obj c) => proxy obj -> Product obj a (Product obj b c) `hom` Product obj (Product obj a b) c
-    assocR :: (obj a, obj b, obj c) => proxy obj -> Product obj (Product obj a b) c `hom` Product obj a (Product obj b c)
-
-instance ContainsMonoidalObjects obj => MonoidalCategory (->) obj where
-    idLI _ x = (x, ())
-    idLE _ (x, ()) = x
-    idRI _ x = ((), x)
-    idRE _ ((), x) = x
-
-    assocL _ (x, (y, z)) = ((x, y), z)
-    assocR _ ((x, y), z) = (x, (y, z))
-
-class (MonoidalCategory overHom overObj) => EnrichedCategory overHom (overObj :: k -> Constraint) (hom :: j -> j -> k) (obj :: j -> Constraint) where
-    homObj :: (obj a, obj b) => proxy overHom -> proxy' obj -> Dict (overObj (a `hom` b))
-    enrichedIdentity :: obj a => proxy overObj -> proxy' obj -> Unit overObj `overHom` (a `hom` a)
-    enrichedCompose :: (obj a, obj b, obj c) => proxy overObj -> proxy' obj -> Product overObj (b `hom` c) (a `hom` b) `overHom` (a `hom` c)
-
-instance Category hom obj => EnrichedCategory (->) EveryC hom obj where
-    homObj _ _ = Dict
-    enrichedIdentity _ px () = identity px
-    enrichedCompose _ px (f, g) = compose px f g
-
-class (c a, d a) => ProductCI c d a
-instance (c a, d a) => ProductCI c d a

src/Category/Applicative.hs

@@ -1,14 +0,0 @@
-module Category.Applicative where
-
-import Category
-import Category.Functor
-import Category.Semigroup ()
-import qualified Prelude
-
-class (MonoidalCategory domHom domObj, MonoidalCategory codHom codObj, Functor domHom domObj codHom codObj f) => Applicative domHom domObj codHom codObj f where
-    unit :: proxy domHom -> proxy' domObj -> proxy'' codHom -> proxy''' codObj -> f (Unit domObj)
-    zip :: proxy domHom -> proxy' domObj -> proxy'' codObj -> proxy''' codObj -> Product codObj (f a) (f b) `codHom` f (Product domObj a b)
-
-instance {-# INCOHERENT #-} Prelude.Applicative f => Applicative (->) EveryC (->) EveryC f where
-    unit _ _ _ _ = Prelude.pure ()
-    zip _ _ _ _ (x, y) = Prelude.fmap (,) x Prelude.<*> y

src/Category/Constraint.hs

@@ -1,13 +0,0 @@
-module Category.Constraint where
-
-import Category
-import Prelude (($))
-
-newtype a :- b = Sub (a => Dict b)
-
-(\\) :: a => (b => r) -> (a :- b) -> r
-r \\ Sub Dict = r
-
-instance Category (:-) obj where
-    identity _ = Sub Dict
-    compose _ f g = Sub $ Dict \\ f \\ g

src/Category/Evil.hs

@@ -0,0 +1,70 @@
+{-# LANGUAGE PolyKinds #-}
+module Category.Evil where
+
+import Category.Good qualified as Good
+import Category.Neutral qualified as Neutral
+import Data.Dict (Dict (Dict), (:-) (Sub))
+import Data.Kind (Constraint, Type)
+
+class Category (hom :: i -> i -> Type) (obj :: i -> Constraint) where
+    identity :: obj a => proxy obj -> hom a a
+    compose :: (obj a, obj b, obj c) => proxy obj -> hom b c -> hom a b -> hom a c
+
+instance Neutral.Category hom => Category hom obj where
+    identity _ = Neutral.identity
+    compose _ = Neutral.compose
+
+class MonoidalObjects k where
+    type Unit obj :: k
+    type Product obj :: k -> k -> k
+
+instance MonoidalObjects Type where
+    type Unit Type = ()
+    type Product Type = (,)
+
+class MonoidalObjects i => ContainsMonoidalObjects (obj :: i -> Constraint) where
+    monObjUnit :: Dict (obj (Unit i))
+    monObjFactor :: (obj a, obj b) => Dict (obj (Product i a b))
+    monObjDistribute :: obj (Product i a b) => Dict (obj a, obj b)
+
+class (Category hom obj, ContainsMonoidalObjects obj) => Monoidal hom (obj :: i -> Constraint) where
+    --monBi :: proxy cat -> Dict (BiEndo cat (Product cat))
+    monIdLI :: obj a => proxy obj -> a `hom` Product i a (Unit i)
+    monIdRI :: obj a => proxy obj -> a `hom` Product i (Unit i) a
+    monIdLE :: obj a => proxy obj -> Product i a (Unit i) `hom` a
+    monIdRE :: obj a => proxy obj -> Product i (Unit i) a `hom` a
+    monAssocL :: (obj a, obj b, obj c) => proxy obj -> Product i (Product i a b) c `hom` Product i a (Product i b c)
+    monAssocR :: (obj a, obj b, obj c) => proxy obj -> Product i a (Product i b c) `hom` Product i (Product i a b) c
+
+instance (Neutral.Monoidal hom, ContainsMonoidalObjects obj, Neutral.Unit hom ~ Unit i, Neutral.Product hom ~ Product i) => Monoidal hom (obj :: i -> Constraint) where
+    monIdLI _ = Neutral.monIdLI
+    monIdRI _ = Neutral.monIdRI
+    monIdLE _ = Neutral.monIdLE
+    monIdRE _ = Neutral.monIdRE
+    monAssocL _ = Neutral.monAssocL
+    monAssocR _ = Neutral.monAssocR
+
+class Category hom obj => Endofunctor hom obj f where
+    endomapObj :: obj a => proxy hom -> Dict (obj (f a))
+
+class Endofunctor hom obj f => CovariantEndo hom obj f where
+    coendomap :: (obj a, obj b) => proxy obj -> hom a b -> hom (f a) (f b)
+
+instance (Endofunctor hom obj f, Neutral.CovariantEndo hom f) => CovariantEndo hom obj f where
+    coendomap _ = Neutral.coendomap
+
+class (Category domHom domObj, Category codHom codObj) => Functor domHom domObj codHom codObj f where
+    mapObj :: domObj a => proxy domHom -> proxy' domObj -> proxy'' codHom -> Dict (codObj (f a))
+
+instance Endofunctor hom obj f => Functor hom obj hom obj f where
+    mapObj _ _ = endomapObj
+
+class Functor domHom domObj codHom codObj f => Covariant domHom domObj codHom codObj f where
+    comap :: (domObj a, domObj b) => proxy domObj -> proxy' codObj -> domHom a b -> codHom (f a) (f b)
+
+instance (Functor domHom domObj codHom codObj f, Neutral.Covariant domHom codHom f) => Covariant domHom domObj codHom codObj f where
+    comap _ _ = Neutral.comap
+
+class (Monoidal domHom domObj, Monoidal codHom codObj, Covariant domHom domObj codHom codObj f) => Applicative domHom domObj codHom codObj (f :: i -> j) where
+    unit :: proxy domHom -> proxy' domObj -> proxy'' codHom -> proxy''' codObj -> codHom (Unit j) (f (Unit i))
+    zip :: proxy domHom -> proxy' domObj -> proxy'' codObj -> codHom (Product j (f a) (f b)) (f (Product i a b))

src/Category/Functor.hs

@@ -1,21 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-module Category.Functor where
-
-import Category
-import qualified Prelude
-
-class (Category domHom domObj, Category codHom codObj) => Functor domHom domObj codHom codObj f where
-    mapObj :: domObj a => proxy domHom -> proxy' domObj -> proxy'' codHom -> Dict (codObj (f a))
-    map :: (domObj a, domObj b) => proxy domObj -> proxy' codObj -> a `domHom` b -> f a `codHom` f b
-
-instance (Category (->) obj, forall a. obj (Identity a)) => Functor (->) obj (->) obj Identity where
-    mapObj _ _ _ = Dict
-    map _ _ f (Identity x) = Identity (f x)
-
-class (Functor hom obj hom obj f) => Endofunctor hom obj f where
-    endomapObj :: obj a => proxy hom -> proxy' obj -> Dict (obj (f a))
-    endomap :: (obj a, obj b) => proxy obj -> a `hom` b -> f a `hom` f b
-
-instance (Functor hom obj hom obj f) => Endofunctor hom obj f where
-    endomapObj pxh pxo = mapObj pxh pxo pxh
-    endomap px = map px px

src/Category/Good.hs

@@ -0,0 +1,47 @@
+module Category.Good where
+
+class Irrelevant f where
+    irrmap :: f a -> f b
+
+-- | A covariant endofunctor in the category of types.
+class Covariant f where
+    comap :: (a -> b) -> (f a -> f b)
+
+-- | A contravariant endofunctor in the category of types.
+class Contravariant f where
+    contramap :: (b -> a) -> (f a -> f b)
+
+-- | An invariant endofunctor in the category of types.
+class Invariant f where
+    invmap :: (a -> b) -> (b -> a) -> (f a -> f b)
+
+-- | A bifunctor in the category of types covariant in both arguments.
+class Bi f where
+    bimap :: (a -> c) -> (b -> d) -> (f a b -> f c d)
+
+instance Bi (,) where
+    bimap f g (x, y) = (f x, g y)
+
+-- | A profunctor in the category of types (contravariant in the left argument, covariant in the right).
+class Pro f where
+    dimap :: (c -> a) -> (b -> d) -> (f a b -> f c d)
+
+instance Pro (->) where
+    dimap f g h x = g (h (f x))
+
+-- | An applicative functor.
+class Covariant f => Applicative f where
+    pure :: a -> f a
+    ap :: f (a -> b) -> f a -> f b
+
+-- | A monoid object in the category of endofunctors in the category of types.
+class Applicative m => Monad m where
+    join :: m (m a) -> m a
+
+-- | A semigroup object in the category of types.
+class Semigroup s where
+    append :: s -> s -> s
+
+-- | A monoid object in the category of types.
+class Semigroup m => Monoid m where
+    empty :: m

src/Category/Monoid.hs

@@ -1,18 +0,0 @@
-{-# LANGUAGE UndecidableSuperClasses #-}
-module Category.Monoid where
-
-import Category
-import Category.Functor
-import Category.NaturalTransformation
-import Category.Semigroup
-import qualified Control.Monad
-import qualified Prelude
-
-class Semigroup hom obj m => Monoid hom obj m where
-    empty :: proxy obj -> Unit obj `hom` m
-
-instance (Semigroup (->) obj m, Prelude.Monoid m) => Monoid (->) obj m where
-    empty _ () = Prelude.mempty
-
-instance (hom ~ Nat (->) EveryC (->) EveryC, MonoidalCategory hom (Endofunctor (->) EveryC), Prelude.Monad m) => Monoid hom (Endofunctor (->) EveryC) m where
-    empty _ = Nat \(Identity x) -> Prelude.return x

src/Category/NaturalTransformation.hs

@@ -1,59 +0,0 @@
-module Category.NaturalTransformation where
-
-import Category
-import Category.Functor
-import Data.Kind (Constraint)
-import Prelude (($), undefined)
-
-data Nat domHom domObj codHom codObj f g where
-    Nat :: (Functor domHom domObj codHom codObj f, Functor domHom domObj codHom codObj g) => (forall a. domObj a => f a `codHom` g a) -> Nat domHom domObj codHom codObj f g
-
-instance (Category domHom domObj, Category codHom codObj) => Category (Nat domHom domObj codHom codObj) (ProductCI (Functor domHom domObj codHom codObj) obj) where
-    -- This type signature is just boilerplate to get `f` into scope, which is necessary to get the `codObj (f a)` instance.
-    identity :: forall f proxy. ProductCI (Functor domHom domObj codHom codObj) obj f => proxy (ProductCI (Functor domHom domObj codHom codObj) obj) -> Nat domHom domObj codHom codObj f f
-    identity _ = Nat f
-        where f :: forall a. domObj a => f a `codHom` f a
-              f = case mapObj (Proxy @domHom) (Proxy @domObj) (Proxy @codHom) :: Dict (codObj (f a)) of Dict -> identity (Proxy @codObj)
-
-    compose :: forall a b c proxy. (ProductCI (Functor domHom domObj codHom codObj) obj a, ProductCI (Functor domHom domObj codHom codObj) obj b, ProductCI (Functor domHom domObj codHom codObj) obj c) => proxy (ProductCI (Functor domHom domObj codHom codObj) obj) -> Nat domHom domObj codHom codObj b c -> Nat domHom domObj codHom codObj a b -> Nat domHom domObj codHom codObj a c
-    compose _ (Nat f) (Nat g) = Nat fg
-        where fg :: forall x. domObj x => a x `codHom` c x
-              fg = case mapObj' (Proxy @a) of
-                  Dict -> case mapObj' (Proxy @b) of
-                      Dict -> case mapObj' (Proxy @c) of
-                          Dict -> compose (Proxy @codObj) f g
-                where mapObj' :: forall f proxy. Functor domHom domObj codHom codObj f => proxy f -> Dict (codObj (f x))
-                      mapObj' _ = mapObj (Proxy @domHom) (Proxy @domObj) (Proxy @codHom) :: Dict (codObj (f x))
-
-data ComposeEndofunctor hom obj f g x where
-    ComposeEndofunctor :: { getComposeEndofunctor :: (Endofunctor hom obj f, Endofunctor hom obj g, obj x) => f (g x) } -> ComposeEndofunctor hom obj f g x
-
-instance {-# INCOHERENT #-} (Category (->) obj, Endofunctor (->) obj f, Endofunctor (->) obj g, forall a. obj (ComposeEndofunctor (->) obj f g a)) => Functor (->) obj (->) obj (ComposeEndofunctor (->) obj f g) where
-    mapObj _ _ _ = Dict
-
-    map :: forall a b proxy proxy'. (obj a, obj b) => proxy obj -> proxy' obj -> (a -> b) -> ComposeEndofunctor (->) obj f g a -> ComposeEndofunctor (->) obj f g b
-    map _ _ f (ComposeEndofunctor x) = ComposeEndofunctor $ case mapObj' (Proxy @a) of
-        Dict -> case mapObj' (Proxy @b) of
-            Dict -> endomap (Proxy @obj) (endomap (Proxy @obj) f) x
-      where mapObj' :: forall x proxy. (Endofunctor (->) obj f, obj x) => proxy x -> Dict (obj (g x))
-            mapObj' _ = mapObj (Proxy @(->)) (Proxy @obj) (Proxy @(->))
-
-instance Category hom obj => MonoidalObjects (Endofunctor hom (obj :: * -> Constraint)) where
-    type Unit (Endofunctor hom obj) = Identity
-    type Product (Endofunctor hom obj) = ComposeEndofunctor hom obj
-
-instance ContainsMonoidalObjects (Endofunctor (->) (EveryC :: * -> Constraint)) where
-    unitObj = Dict
-    productObjFactor = Dict
-    -- FIXME: Implement this
-    productObjDistribute = undefined
-
-instance (obj ~ EveryC, hom ~ Nat (->) obj (->) obj, Category hom (Endofunctor (->) obj)) => MonoidalCategory hom (Endofunctor (->) obj) where
-    idLI _ = Nat \x -> ComposeEndofunctor (endomap (Proxy @obj) Identity x)
-    idLE _ = Nat \(ComposeEndofunctor x) -> endomap (Proxy @obj) getIdentity x
-    idRI _ = Nat \x -> ComposeEndofunctor (Identity x)
-    idRE _ = Nat \(ComposeEndofunctor (Identity x)) -> x
-
-    assocL _ = Nat \(ComposeEndofunctor x) -> ComposeEndofunctor (ComposeEndofunctor (endomap (Proxy @obj) getComposeEndofunctor x))
-    -- FIXME: Finish implementing this
-    assocR _ = Nat \(ComposeEndofunctor (ComposeEndofunctor x)) -> ComposeEndofunctor (endomap (Proxy @obj) ComposeEndofunctor undefined)

src/Category/Neutral.hs

@@ -0,0 +1,151 @@
+{-# LANGUAGE PolyKinds #-}
+module Category.Neutral where
+
+import Category.Good qualified as Good
+import Data.Dict (Dict (Dict), (:-) (Sub), (\\))
+import Data.Kind (Type)
+
+-- | An unenriched hom.
+type family (~>) :: i -> i -> Type
+type instance (~>) = (->)
+type instance (~>) = (:-)
+
+type Dom (a :: i) = (~>) :: i -> i -> Type
+
+-- | An unenriched category.
+class Category cat where
+    identity :: cat a a
+    compose :: cat b c -> cat a b -> cat a c
+
+instance Category (->) where
+    identity x = x
+    compose f g x = f (g x)
+
+instance Category (:-) where
+    identity = Sub Dict
+    compose f g = Sub (Dict \\ f \\ g)
+
+-- | An covariant endofunctor in an unenriched category.
+class Category cat => CovariantEndo cat f where
+    coendomap :: cat a b -> cat (f a) (f b)
+
+instance Good.Covariant f => CovariantEndo (->) f where
+    coendomap = Good.comap
+
+-- | A contravariant endofunctor in an unenriched category.
+class Category cat => ContravariantEndo cat f where
+    contraendomap :: cat b a -> cat (f a) (f b)
+
+instance Good.Contravariant f => ContravariantEndo (->) f where
+    contraendomap = Good.contramap
+
+-- | An invariant endofunctor (if that's even considered a functor) in an unenriched category.
+class Category cat => InvariantEndo cat f where
+    invendomap :: cat a b -> cat b a -> cat (f a) (f b)
+
+instance Good.Invariant f => InvariantEndo (->) f where
+    invendomap = Good.invmap
+
+-- | A bi-endofunctor in an unenriched category covariant in both arguments.
+class Category cat => BiEndo cat f where
+    biendomap :: cat a c -> cat b d -> cat (f a b) (f c d)
+
+instance Good.Bi f => BiEndo (->) f where
+    biendomap = Good.bimap
+
+-- | A pro-endofunctor in an unenriched category (contravariant in the left argument, covariant in the right).
+class Category cat => ProEndo cat f where
+    diendomap :: cat c a -> cat b d -> cat (f a b) (f c d)
+
+instance Good.Pro f => ProEndo (->) f where
+    diendomap = Good.dimap
+
+-- | A covariant functor between unenriched categories.
+class (Category dom, Category cod) => Covariant dom cod f where
+    comap :: dom a b -> cod (f a) (f b)
+
+instance CovariantEndo cat f => Covariant cat cat f where
+    comap = coendomap
+
+-- | A contravariant functor between unenriched categories.
+class (Category dom, Category cod) => Contravariant dom cod f where
+    contramap :: dom b a -> cod (f a) (f b)
+
+instance ContravariantEndo cat f => Contravariant cat cat f where
+    contramap = contraendomap
+
+-- | An invariant functor (if that's even considered a functor) between unenriched categories.
+class (Category dom, Category cod) => Invariant dom cod f where
+    invmap :: dom a b -> dom b a -> cod (f a) (f b)
+
+instance InvariantEndo cat f => Invariant cat cat f where
+    invmap = invendomap
+
+-- | A bifunctor in an unenriched category covariant in both arguments.
+class (Category dom, Category cod) => Bi dom cod f where
+    bimap :: dom a c -> dom b d -> cod (f a b) (f c d)
+
+instance BiEndo cat f => Bi cat cat f where
+    bimap = biendomap
+
+-- | A profunctor in an unenriched category (contravariant in the left argument, covariant in the right).
+class (Category dom, Category cod) => Pro dom cod f where
+    dimap :: dom c a -> dom b d -> cod (f a b) (f c d)
+
+instance ProEndo cat f => Pro cat cat f where
+    dimap = diendomap
+
+instance Pro (:-) (->) (:-) where
+    dimap f g h = compose g (compose h f)
+
+class Category cat => Monoidal (cat :: i -> i -> Type) where
+    type Unit cat :: i
+    type Product cat :: i -> i -> i
+    monBi :: proxy cat -> Dict (BiEndo cat (Product cat))
+    monIdLI :: a `cat` Product cat a (Unit cat)
+    monIdRI :: a `cat` Product cat (Unit cat) a
+    monIdLE :: Product cat a (Unit cat) `cat` a
+    monIdRE :: Product cat (Unit cat) a `cat` a
+    monAssocL :: Product cat (Product cat a b) c `cat` Product cat a (Product cat b c)
+    monAssocR :: Product cat a (Product cat b c) `cat` Product cat (Product cat a b) c
+
+instance Monoidal (->) where
+    type Unit (->) = ()
+    type Product (->) = (,)
+    monBi _ = Dict
+    monIdLI x = (x, ())
+    monIdRI x = ((), x)
+    monIdLE (x, ()) = x
+    monIdRE ((), x) = x
+    monAssocL ((x, y), z) = (x, (y, z))
+    monAssocR (x, (y, z)) = ((x, y), z)
+
+-- | A semigroup object in a monoidal unenriched category.
+class Monoidal cat => Semigroup cat s where
+    append :: Product cat s s `cat` s
+
+instance Good.Semigroup s => Semigroup (->) s where
+    append (x, y) = Good.append x y
+
+-- | A monoid object in a monoidal unenriched category.
+class Semigroup cat s => Monoid cat s where
+    empty :: Unit cat `cat` s
+
+instance Good.Monoid s => Monoid (->) s where
+    empty () = Good.empty
+
+-- | An applicative functor.
+class (Monoidal cat, CovariantEndo cat f) => Applicative cat f where
+    pure :: a `cat` f a
+    ap :: Product cat (f (a `cat` b)) (f a) `cat` f b
+
+instance Good.Applicative f => Applicative (->) f where
+    pure = Good.pure
+    ap (f, x) = Good.ap f x
+
+-- | A monoid object in the category of endofunctors in a monoidal unenriched category.
+class Applicative cat m => Monad cat m where
+    join :: m (m a) `cat` m a
+
+instance Good.Monad m => Monad (->) m where
+    join = Good.join

src/Category/Neutral/Enriched.hs

@@ -0,0 +1,11 @@
+module Category.Neutral.Enriched where
+
+import Category.Neutral qualified as Neutral
+
+class Neutral.Monoidal under => Category under cat where
+    identity :: Neutral.Unit under `under` cat a a
+    compose :: Neutral.Product under (cat b c) (cat a b) `under` cat a c
+
+instance Neutral.Category cat => Category (->) cat where
+    identity () = Neutral.identity
+    compose (f, g) = Neutral.compose f g

src/Category/Neutral/NaturalTransformation.hs

@@ -0,0 +1,20 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Category.Neutral.NaturalTransformation where
+
+import Category.Neutral
+import Data.Kind (Type)
+
+-- f , g :: i -> j
+-- (~>) :: j -> j -> Type
+-- Nat :: (i -> j) -> (i -> j) -> Type
+newtype Nat f g = Nat { runNat :: forall a. f a ~> g a }
+
+type instance (~>) = Nat
+
+type D (hom :: (i -> j) -> (i -> j) -> Type) = (~>) :: j -> j -> Type
+
+instance (nat ~ Nat, Category (D nat)) => Category (nat :: (i -> j) -> (i -> j) -> Type) where
+    identity = Nat identity
+    compose (Nat f) (Nat g) = Nat (compose f g)

src/Category/Semigroup.hs

@@ -1,22 +0,0 @@
-{-# LANGUAGE UndecidableSuperClasses #-}
-module Category.Semigroup where
-
-import Category
-import Category.Functor
-import Category.NaturalTransformation
-import qualified Control.Monad
-import Prelude (uncurry)
-import qualified Prelude
-
-class (MonoidalCategory hom obj, obj m) => Semigroup hom obj m where
-    append :: proxy obj -> Product obj m m `hom` m
-
-instance {-# INCOHERENT #-} Prelude.Functor f => Functor (->) EveryC (->) EveryC f where
-    mapObj _ _ _ = Dict
-    map _ _ = Prelude.fmap
-
-instance {-# OVERLAPPABLE #-} (MonoidalCategory (->) obj, obj m, Prelude.Semigroup m) => Semigroup (->) obj m where
-    append _ = uncurry (Prelude.<>)
-
-instance {-# OVERLAPPABLE #-} (hom ~ Nat (->) EveryC (->) EveryC, MonoidalCategory hom (Endofunctor (->) EveryC), Prelude.Monad m) => Semigroup hom (Endofunctor (->) EveryC) m where
-    append _ = Nat \(ComposeEndofunctor x) -> Control.Monad.join x

src/Data/Dict.hs

@@ -0,0 +1,10 @@
+{-# LANGUAGE RankNTypes #-}
+module Data.Dict where
+
+data Dict c where
+    Dict :: c => Dict c
+
+newtype a :- b = Sub (a => Dict b)
+
+(\\) :: a => (b => c) -> (a :- b) -> c
+r \\ Sub Dict = r

stack.yaml

@@ -1,4 +1,5 @@
-resolver: lts-16.11
+# Required to use GHC 8.10, which is required for ImportQualifiedPost.
+resolver: nightly-2020-10-20
 
 packages:
 - .