Mostly irrelevant additions: monoidal, unit, void.

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

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 9da0ab5910c39708370abf34bf6550033a06f63815096534e1c3fb9aa07ad25d
+-- hash: cd92b699ef3ea167b65a8294cb6f08cb475d5aba3d96aeb8b85abfb4e90daf99
 
 name:           monoids-in-the-category-of-endofunctors
 version:        0.1.0.0
@@ -32,6 +32,10 @@ library
       Category.Functor
       Category.Functor.Foldable
       Category.Functor.Foldable.TH
+      Category.Monoid
+      Category.Monoidal
+      Category.Unit
+      Category.Void
       Data.Dict
       Data.Fin
       Data.Nat
@@ -42,7 +46,7 @@ library
       Paths_monoids_in_the_category_of_endofunctors
   hs-source-dirs:
       src
-  default-extensions: BlockArguments ConstraintKinds DataKinds DefaultSignatures FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs LambdaCase MultiParamTypeClasses NoImplicitPrelude PolyKinds QuantifiedConstraints RankNTypes ScopedTypeVariables TypeApplications TypeFamilies TypeOperators
+  default-extensions: BlockArguments ConstraintKinds DataKinds DefaultSignatures EmptyCase FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs LambdaCase MultiParamTypeClasses NoImplicitPrelude PolyKinds QuantifiedConstraints RankNTypes ScopedTypeVariables TypeApplications TypeFamilies TypeOperators
   ghc-options: -Weverything -Wno-missing-export-lists -Wno-missing-import-lists -Wno-missing-safe-haskell-mode -Wno-safe -Wno-unsafe
   build-depends:
       base >=4.13 && <5

package.yaml

@@ -16,6 +16,7 @@ default-extensions:
 - ConstraintKinds
 - DataKinds
 - DefaultSignatures
+- EmptyCase
 - FlexibleContexts
 - FlexibleInstances
 - FunctionalDependencies

src/Category/Base.hs

@@ -6,6 +6,9 @@ import Data.Kind (Constraint, Type)
 class Vacuous (a :: i)
 instance Vacuous (a :: i)
 
+class Bottom (a :: i) where
+    bottom :: forall b proxy. proxy a -> b
+
 class Semigroupoid (q :: i -> i -> Type) where
     type Obj q :: i -> Constraint
     type Obj _ = Vacuous
@@ -54,14 +57,3 @@ instance Category (:~:) where
 
 instance Groupoid (:~:) where
     inv Refl = Refl
-
-data Unit a b = Unit
-
-instance Semigroupoid Unit where
-    Unit . Unit = Unit
-
-instance Category Unit where
-    id = Unit
-
-instance Groupoid Unit where
-    inv _ = Unit

src/Category/Functor.hs

@@ -3,6 +3,7 @@ module Category.Functor where
 
 import Category.Base
 import Category.Constraint ((:-) (Sub), Dict (Dict))
+import Data.Either (Either (Left, Right))
 import Data.Kind (Type)
 import Data.Maybe (Maybe (Nothing, Just))
 import Quantifier
@@ -79,6 +80,20 @@ instance Functor ((,) a) where
     type Cod ((,) a) = (->)
     map f (x, y) = (x, f y)
 
+instance Functor Either where
+    type Dom Either = (->)
+    type Cod Either = Nat (->) (->)
+    map_ = Sub Dict
+    map f = Nat \case
+        Left  x -> Left (f x)
+        Right y -> Right y
+
+instance Functor (Either a) where
+    type Dom (Either a) = (->)
+    type Cod (Either a) = (->)
+    map _ (Left x)  = Left x
+    map f (Right y) = Right (f y)
+
 instance Functor Dict where
     type Dom Dict = (:-)
     type Cod Dict = (->)

src/Category/Monoid.hs

@@ -0,0 +1,10 @@
+module Category.Monoid where
+
+import Category.Functor
+import Category.Monoidal
+
+class TensorProduct f => Semigroup (f :: i -> i -> i) (s :: i) where
+    append :: Cod2 f (f s s) s
+
+class Semigroup f m => Monoid f m where
+    empty :: proxy f -> Cod2 f (Unit f) m

src/Category/Monoidal.hs

@@ -0,0 +1,49 @@
+module Category.Monoidal where
+
+import Category.Base
+import Category.Constraint
+import Category.Functor
+import Data.Either (Either (Left, Right))
+import Data.Void (Void, absurd)
+
+class Bifunctor f => TensorProduct (f :: i -> i -> i) where
+    type Unit f :: i
+    unitObj :: proxy f -> Dict (Obj (Dom f) (Unit f))
+
+    unitLI  :: Dom f a (f a (Unit f))
+    unitRI  :: Dom f a (f (Unit f) a)
+    unitLE  :: Dom f (f a (Unit f)) a
+    unitRE  :: Dom f (f (Unit f) a) a
+
+    assocL  :: Dom f (f a (f b c)) (f (f a b) c)
+    assocR  :: Dom f (f (f a b) c) (f a (f b c))
+
+instance TensorProduct (,) where
+    type Unit (,) = ()
+    unitObj _ = Dict
+
+    unitLI x = (x, ())
+    unitRI x = ((), x)
+    unitLE (x, _) = x
+    unitRE (_, x) = x
+
+    assocL (x, (y, z)) = ((x, y), z)
+    assocR ((x, y), z) = (x, (y, z))
+
+instance TensorProduct Either where
+    type Unit Either = Void
+    unitObj _ = Dict
+
+    unitLI = Left
+    unitRI = Right
+    unitLE (Left x) = x
+    unitLE (Right x) = absurd x
+    unitRE (Left x) = absurd x
+    unitRE (Right x) = x
+
+    assocL (Left x) = Left (Left x)
+    assocL (Right (Left x)) = Left (Right x)
+    assocL (Right (Right x)) = Right x
+    assocR (Left (Left x)) = Left x
+    assocR (Left (Right x)) = Right (Left x)
+    assocR (Right x) = Right (Right x)

src/Category/Unit.hs

@@ -0,0 +1,14 @@
+module Category.Unit where
+
+import Category.Base
+
+data Unit (a :: ()) (b :: ()) = Unit
+
+instance Semigroupoid Unit where
+    _ . _ = Unit
+
+instance Category Unit where
+    id = Unit
+
+instance Groupoid Unit where
+    inv _ = Unit

src/Category/Void.hs

@@ -0,0 +1,16 @@
+module Category.Void where
+
+import Category.Base
+import Data.Proxy
+import Data.Void qualified as V
+
+data Void (a :: V.Void) (b :: V.Void)
+
+instance Semigroupoid Void where
+    type Obj Void = Bottom
+    observe = \case {}
+    (.) = \case {}
+
+instance Category Void where
+    id :: forall a. Bottom a => Void a a
+    id = bottom (Proxy @a)

src/Data/Nat.hs

@@ -2,13 +2,15 @@ module Data.Nat where
 
 import Category
 import Category.Functor.Foldable
-import Category.Functor.Foldable.TH
 import Data.Kind (Type)
 import Data.Maybe (Maybe (Nothing, Just))
 import Quantifier
 
 data N = Z | S N
 
+inf :: N
+inf = S inf
+
 instance Pi N where
     data Ty N :: N -> Type where
         ZTy :: Ty N 'Z
@@ -65,3 +67,15 @@ instance Corecursive (Ty N) where
     embed = Nat \case
         ZTyF -> ZTy
         (STyF r) -> STy r
+
+type family (:+) (m :: N) (n :: N) :: N where
+    'Z   :+ n =          n
+    'S m :+ n = 'S (m :+ n)
+
+injective :: forall m n. Ty N m -> ('S m ~ 'S n) :- (m ~ n)
+injective ZTy = Sub Dict
+injective (STy i) = case injective i of Sub Dict -> Sub Dict
+
+rightZero :: forall m. Ty N m -> Dict ((m :+ 'Z) ~ m)
+rightZero ZTy = Dict
+rightZero (STy i) = case rightZero i of Dict -> Dict