Merge pull request #5 from sellout/oidification

Categorify a bunch of algebraic structures

README.md

@@ -25,7 +25,7 @@ instance
   map = Data.Functor.fmap
 ```
 
-Which also means that if you're defining your own instances, you'd be well-served to implement them using the type classes from base whenever possible, getting a bunch of Haskerwaul instances for free (e.g., if you implement `Control.Category.Category`, I think you must get at least three separate Haskerwaul instances ([`Magma`](./src/Haskerwaul/Magma.hs), [`Semigroup`](./src/Haskerwaul/Semigroup.hs), and [`UnitalMagma`](./src/Haskerwaul/Magma/Unital.hs) -- things like [`Semigroupoid`](./src/Haskerwaul/Semigroupoid.hs) and [`Category`](./src/Haskerwaul/Category.hs) are either type synonyms or have universal instances already defined. Once you have the instance from base, you can implement richer classes like `CartesianClosedCategory` using Haskerwaul's classes.
+Which also means that if you're defining your own instances, you'd be well-served to implement them using the type classes from base whenever possible, getting a bunch of Haskerwaul instances for free (e.g., if you implement `Control.Category.Category`, I think you must get at least three separate Haskerwaul instances ([`Magma`](./src/Haskerwaul/Magma.hs), [`Semigroup`](./src/Haskerwaul/Semigroup.hs), and [`UnitalMagma`](./src/Haskerwaul/Magma/Unital.hs) -- things like [`Semicategory`](./src/Haskerwaul/Semicategory.hs) and [`Category`](./src/Haskerwaul/Category.hs) are either type synonyms or have universal instances already defined. Once you have the instance from base, you can implement richer classes like `CartesianClosedCategory` using Haskerwaul's classes.
 
 However, this library does not play well with `Prelude`, co-opting a bunch of the same names, so it's helpful to either enable `NoImplicitPrelude` or import Haskerwaul qualified. Unfortunately, [the `Haskerwaul` module](./src/Haskerwaul.hs) is not quite a custom Prelude and I've avoided expanding it into one, because there are a lot of points of contention when designing a Prelude. But perhaps it can be used as the basis of one.
 
@@ -62,6 +62,23 @@ There are a lot of one-character type parameters here, but we try to use them at
 - `a`, `b`, `x`, `y`, `z` -- objects in a category and/or elements of those objects (kind `ok`)
 - `t`, `t'`, `ct`, `dt` -- tensors (kind `ok -> ok -> ok`) in a category (`ct` and `dt` distinguish when we're talking about tensors in categories `c` and `d`)
 
+## [horizontal categorification](https://ncatlab.org/nlab/show/horizontal+categorification) / oidification
+
+Horizontally categorified concepts are generally defined via type synonyms.
+E.g., the most central concept in this library is `Category`, which is defined
+simply as
+
+```haskell
+type Category = HorizontalCategorification Monoid
+```
+
+See [the
+examples](https://ncatlab.org/nlab/show/horizontal+categorification#examples)
+for a more comprehensive list.
+
+In cases where we can't simply use type synonyms, the Haddock should describe
+why.
+
 ## law checking
 
 Haskerwaul attempts to make it as easy and flexible as possible to test laws

haskerwaul/haskerwaul.cabal

@@ -187,9 +187,11 @@ library
     Haskerwaul.Band.Rectangular
     Haskerwaul.Bifunctor
     Haskerwaul.Bimonoid
+    Haskerwaul.Categorification.Horizontal
     Haskerwaul.Category
     Haskerwaul.Category.Bicartesian
     Haskerwaul.Category.Boolean
+    Haskerwaul.Category.Cancellative
     Haskerwaul.Category.Closed
     Haskerwaul.Category.Closed.Bicartesian
     Haskerwaul.Category.Closed.Cartesian
@@ -228,6 +230,7 @@ library
     Haskerwaul.Category.Opposite
     Haskerwaul.Category.Over
     Haskerwaul.Category.Pointed
+    Haskerwaul.Category.Presheaves
     Haskerwaul.Category.Product
     Haskerwaul.Category.Regular
     Haskerwaul.Category.Ribbon
@@ -237,6 +240,7 @@ library
     Haskerwaul.Category.Rig.ColaxDistributive.Right
     Haskerwaul.Category.Semigroupal
     Haskerwaul.Category.Semigroupal.Laws
+    Haskerwaul.Category.Small
     Haskerwaul.Category.Small.Locally
     Haskerwaul.Category.Terminal
     Haskerwaul.Category.Under
@@ -324,15 +328,20 @@ library
     Haskerwaul.Law.Symmetry
     Haskerwaul.Loop
     Haskerwaul.Loop.Commutative
+    Haskerwaul.Loopoid
     Haskerwaul.Magma
     Haskerwaul.Magma.Commutative
     Haskerwaul.Magma.Commutative.Laws
+    Haskerwaul.Magma.Flexible
     Haskerwaul.Magma.Invertible
     Haskerwaul.Magma.Invertible.Commutative
     Haskerwaul.Magma.Invertible.Left
     Haskerwaul.Magma.Invertible.Right
     Haskerwaul.Magma.Unital
     Haskerwaul.Magma.Unital.Laws
+    Haskerwaul.Magmoid
+    Haskerwaul.Magmoid.Flexible
+    Haskerwaul.Magmoid.Unital
     Haskerwaul.Meadow
     Haskerwaul.Meadow.Cancellation
     Haskerwaul.Meadow.NonInvolutive
@@ -344,6 +353,7 @@ library
     Haskerwaul.Monad.Codensity
     Haskerwaul.Monad.Frobenius
     Haskerwaul.Monoid
+    Haskerwaul.Monoid.Cancellative
     Haskerwaul.Monoid.Commutative
     Haskerwaul.Monoid.Commutative.Laws
     Haskerwaul.Monoid.Commutative.Monus
@@ -375,16 +385,20 @@ library
     -- __TODO__: eliminate the Orphans module
     Haskerwaul.Orphans
     Haskerwaul.Preorder
+    Haskerwaul.Presheaf
     Haskerwaul.Profunctor
     Haskerwaul.Pullback
     Haskerwaul.Pushout
     Haskerwaul.Quandle
     Haskerwaul.Quasigroup
+    Haskerwaul.Quasigroup.Associative
     Haskerwaul.Quasigroup.Commutative
     Haskerwaul.Quasigroup.Invertible
     Haskerwaul.Quasigroup.Invertible.Commutative
     Haskerwaul.Quasigroup.Left
     Haskerwaul.Quasigroup.Right
+    Haskerwaul.Quasigroupoid
+    Haskerwaul.Quasigroupoid.Associative
     Haskerwaul.Quasiorder
     Haskerwaul.Rack
     -- Haskerwaul.RebindableSyntax
@@ -416,6 +430,9 @@ library
     Haskerwaul.Ring.Boolean
     Haskerwaul.Ring.Commutative
     Haskerwaul.Ring.Nonunital
+    Haskerwaul.Semicategory
+    Haskerwaul.Semicategory.Laws
+    Haskerwaul.Semifunctor
     Haskerwaul.Semigroup
     Haskerwaul.Semigroup.Commutative
     Haskerwaul.Semigroup.Commutative.Laws
@@ -425,8 +442,7 @@ library
     Haskerwaul.Semilattice.Bounded
     Haskerwaul.Semilattice.Bounded.Laws
     Haskerwaul.Semilattice.Laws
-    Haskerwaul.Semigroupoid
-    Haskerwaul.Semigroupoid.Laws
+    Haskerwaul.Semipresheaf
     Haskerwaul.Semiring
     Haskerwaul.Semiring.Idempotent
     Haskerwaul.Semiring.MaxPlus

haskerwaul/src/Haskerwaul.hs

@@ -24,9 +24,11 @@ module Haskerwaul
     module Haskerwaul.Band.Rectangular,
 
     -- * categories
+    module Haskerwaul.Categorification.Horizontal,
     module Haskerwaul.Category,
     module Haskerwaul.Category.Bicartesian,
     module Haskerwaul.Category.Boolean,
+    module Haskerwaul.Category.Cancellative,
     module Haskerwaul.Category.Coherent,
     module Haskerwaul.Category.CoKleisli,
     module Haskerwaul.Category.Complete.Finitely,
@@ -42,6 +44,7 @@ module Haskerwaul
     module Haskerwaul.Category.Opposite,
     module Haskerwaul.Category.Over,
     module Haskerwaul.Category.Pointed,
+    module Haskerwaul.Category.Presheaves,
     module Haskerwaul.Category.Product,
     module Haskerwaul.Category.Regular,
     module Haskerwaul.Category.Ribbon,
@@ -50,6 +53,7 @@ module Haskerwaul
     module Haskerwaul.Category.Rig.ColaxDistributive.Left,
     module Haskerwaul.Category.Rig.ColaxDistributive.Right,
     module Haskerwaul.Category.Semigroupal,
+    module Haskerwaul.Category.Small,
     module Haskerwaul.Category.Small.Locally,
     module Haskerwaul.Category.Terminal,
     module Haskerwaul.Category.Under,
@@ -119,7 +123,10 @@ module Haskerwaul
     module Haskerwaul.Functor.Hom,
     module Haskerwaul.Functor.Hom.Internal,
     module Haskerwaul.Functor.Strong,
+    module Haskerwaul.Presheaf,
     module Haskerwaul.Profunctor,
+    module Haskerwaul.Semifunctor,
+    module Haskerwaul.Semipresheaf,
 
     -- ** monoidal functors
     module Haskerwaul.Functor.Monoidal.Closed,
@@ -173,15 +180,20 @@ module Haskerwaul
 
     -- * loops
     module Haskerwaul.Loop,
+    module Haskerwaul.Loopoid,
 
     -- * magmas
     module Haskerwaul.Magma,
     module Haskerwaul.Magma.Commutative,
+    module Haskerwaul.Magma.Flexible,
     module Haskerwaul.Magma.Invertible,
     module Haskerwaul.Magma.Invertible.Commutative,
     module Haskerwaul.Magma.Invertible.Left,
     module Haskerwaul.Magma.Invertible.Right,
     module Haskerwaul.Magma.Unital,
+    module Haskerwaul.Magmoid,
+    module Haskerwaul.Magmoid.Flexible,
+    module Haskerwaul.Magmoid.Unital,
 
     -- * meadows
     module Haskerwaul.Meadow,
@@ -204,6 +216,7 @@ module Haskerwaul
     module Haskerwaul.Bimonoid,
     module Haskerwaul.Comonoid,
     module Haskerwaul.Monoid,
+    module Haskerwaul.Monoid.Cancellative,
     module Haskerwaul.Monoid.Commutative,
     module Haskerwaul.Monoid.Commutative.Monus,
     module Haskerwaul.Monoid.Frobenius,
@@ -247,11 +260,14 @@ module Haskerwaul
 
     -- * quasigroups
     module Haskerwaul.Quasigroup,
+    module Haskerwaul.Quasigroup.Associative,
     module Haskerwaul.Quasigroup.Commutative,
     module Haskerwaul.Quasigroup.Invertible,
     module Haskerwaul.Quasigroup.Invertible.Commutative,
     module Haskerwaul.Quasigroup.Left,
     module Haskerwaul.Quasigroup.Right,
+    module Haskerwaul.Quasigroupoid,
+    module Haskerwaul.Quasigroupoid.Associative,
 
     -- * racks
     module Haskerwaul.Quandle,
@@ -297,14 +313,14 @@ module Haskerwaul
     module Haskerwaul.Ring.Nonunital,
 
     -- * semigroups
+    module Haskerwaul.Semicategory,
     module Haskerwaul.Semigroup,
     module Haskerwaul.Semigroup.Commutative,
     module Haskerwaul.Semigroup.Inverse,
 
     -- * semilattices
     module Haskerwaul.Semilattice,
     module Haskerwaul.Semilattice.Bounded,
-    module Haskerwaul.Semigroupoid,
 
     -- * semirings
     module Haskerwaul.Semiring,
@@ -344,9 +360,11 @@ import Haskerwaul.Band.LeftRegular
 import Haskerwaul.Band.Rectangular
 import Haskerwaul.Bifunctor
 import Haskerwaul.Bimonoid
+import Haskerwaul.Categorification.Horizontal
 import Haskerwaul.Category
 import Haskerwaul.Category.Bicartesian
 import Haskerwaul.Category.Boolean
+import Haskerwaul.Category.Cancellative
 import Haskerwaul.Category.Closed
 import Haskerwaul.Category.Closed.Bicartesian
 import Haskerwaul.Category.Closed.Cartesian
@@ -382,6 +400,7 @@ import Haskerwaul.Category.MonoidalUnit
 import Haskerwaul.Category.Opposite
 import Haskerwaul.Category.Over
 import Haskerwaul.Category.Pointed
+import Haskerwaul.Category.Presheaves
 import Haskerwaul.Category.Product
 import Haskerwaul.Category.Regular
 import Haskerwaul.Category.Ribbon
@@ -390,6 +409,7 @@ import Haskerwaul.Category.Rig.ColaxDistributive
 import Haskerwaul.Category.Rig.ColaxDistributive.Left
 import Haskerwaul.Category.Rig.ColaxDistributive.Right
 import Haskerwaul.Category.Semigroupal
+import Haskerwaul.Category.Small
 import Haskerwaul.Category.Small.Locally
 import Haskerwaul.Category.Terminal
 import Haskerwaul.Category.Under
@@ -472,13 +492,18 @@ import Haskerwaul.Law.Reflexivity
 import Haskerwaul.Law.Symmetry
 import Haskerwaul.Loop
 import Haskerwaul.Loop.Commutative
+import Haskerwaul.Loopoid
 import Haskerwaul.Magma
 import Haskerwaul.Magma.Commutative
+import Haskerwaul.Magma.Flexible
 import Haskerwaul.Magma.Invertible
 import Haskerwaul.Magma.Invertible.Commutative
 import Haskerwaul.Magma.Invertible.Left
 import Haskerwaul.Magma.Invertible.Right
 import Haskerwaul.Magma.Unital
+import Haskerwaul.Magmoid
+import Haskerwaul.Magmoid.Flexible
+import Haskerwaul.Magmoid.Unital
 import Haskerwaul.Meadow
 import Haskerwaul.Meadow.Cancellation
 import Haskerwaul.Meadow.NonInvolutive
@@ -490,6 +515,7 @@ import Haskerwaul.Monad
 import Haskerwaul.Monad.Codensity
 import Haskerwaul.Monad.Frobenius
 import Haskerwaul.Monoid
+import Haskerwaul.Monoid.Cancellative
 import Haskerwaul.Monoid.Commutative
 import Haskerwaul.Monoid.Commutative.Monus
 import Haskerwaul.Monoid.Frobenius
@@ -517,16 +543,20 @@ import Haskerwaul.Order.Partial
 import Haskerwaul.Order.Prefix
 import Haskerwaul.Order.Total
 import Haskerwaul.Preorder
+import Haskerwaul.Presheaf
 import Haskerwaul.Profunctor
 import Haskerwaul.Pullback
 import Haskerwaul.Pushout
 import Haskerwaul.Quandle
 import Haskerwaul.Quasigroup
+import Haskerwaul.Quasigroup.Associative
 import Haskerwaul.Quasigroup.Commutative
 import Haskerwaul.Quasigroup.Invertible
 import Haskerwaul.Quasigroup.Invertible.Commutative
 import Haskerwaul.Quasigroup.Left
 import Haskerwaul.Quasigroup.Right
+import Haskerwaul.Quasigroupoid
+import Haskerwaul.Quasigroupoid.Associative
 import Haskerwaul.Quasiorder
 import Haskerwaul.Rack
 import Haskerwaul.Relation.Apartness
@@ -555,12 +585,14 @@ import Haskerwaul.Ring
 import Haskerwaul.Ring.Boolean
 import Haskerwaul.Ring.Commutative
 import Haskerwaul.Ring.Nonunital
+import Haskerwaul.Semicategory
+import Haskerwaul.Semifunctor
 import Haskerwaul.Semigroup
 import Haskerwaul.Semigroup.Commutative
 import Haskerwaul.Semigroup.Inverse
-import Haskerwaul.Semigroupoid
 import Haskerwaul.Semilattice
 import Haskerwaul.Semilattice.Bounded
+import Haskerwaul.Semipresheaf
 import Haskerwaul.Semiring
 import Haskerwaul.Semiring.Idempotent
 import Haskerwaul.Semiring.MaxPlus

haskerwaul/src/Haskerwaul/Bifunctor.hs

@@ -54,7 +54,7 @@ instance Bifunctor (->) c (->) Const where
   bimap f _ = Const . f . getConst
 
 instance
-  (d ~ (->), Semigroupoid d, Bifunctor c1 c2 d t) =>
+  (d ~ (->), Semicategory d, Bifunctor c1 c2 d t) =>
   Bifunctor
     (NaturalTransformation c' c1)
     (NaturalTransformation c' c2)
@@ -82,7 +82,7 @@ instance
       )
 
 instance
-  (Ob c1 ~ All, Ob c2 ~ All, d ~ (->), Semigroupoid d, Bifunctor c1 c2 d t) =>
+  (Ob c1 ~ All, Ob c2 ~ All, d ~ (->), Semicategory d, Bifunctor c1 c2 d t) =>
   Bifunctor
     (DinaturalTransformation c1)
     (DinaturalTransformation c2)
@@ -124,6 +124,10 @@ instance
   where
   op = Const . op . bimap getConst getConst
 
+instance
+  (c ~ (->), Bifunctor c c c t, FlexibleMagma c t a) =>
+  FlexibleMagma c t (Const a b)
+
 instance
   (c ~ (->), Bifunctor c c c t, Semigroup c t a) =>
   Semigroup c t (Const a b)
@@ -145,6 +149,15 @@ instance
   where
   op = NT (op . lowerFTensor)
 
+instance
+  ( d ~ (->),
+    MonoidalCategory' d dt,
+    Bifunctor d d d dt,
+    u ~ Unit d dt,
+    FlexibleMagma d dt u
+  ) =>
+  FlexibleMagma (NaturalTransformation c d) (FTensor dt) (Const u)
+
 instance
   ( d ~ (->),
     MonoidalCategory' d dt,
@@ -171,6 +184,10 @@ instance
   where
   op = BConst . op . bimap getBConst getBConst
 
+instance
+  (c ~ (->), Bifunctor c c c t, FlexibleMagma c t a) =>
+  FlexibleMagma c t (BConst a b d)
+
 instance
   (c ~ (->), Bifunctor c c c t, Semigroup c t a) =>
   Semigroup c t (BConst a b d)
@@ -192,6 +209,15 @@ instance
   where
   op = DT (op . lowerBTensor)
 
+instance
+  ( d ~ (->),
+    MonoidalCategory' d dt,
+    Bifunctor d d d dt,
+    u ~ Unit d dt,
+    FlexibleMagma d dt u
+  ) =>
+  FlexibleMagma (DinaturalTransformation d) (BTensor dt) (BConst u)
+
 instance
   ( d ~ (->),
     MonoidalCategory' d dt,