Wailing into the primordial ooze of category theory
Wailing into the primordial ooze of category theory.
This requires either Dhall 1.18 or 1.20+ (it will not work on Dhall 1.19).
Fundamentally, there are very few things here
Adjunction
Semigroup
, Monoid
, Group
, and Semilattice
(with commutative and ordered variants)Functor
Lan
and Ran
)Compose
, Either
, Identity
, Tuple
) to be able to model particular monoidsMany of the other types are defined as specializations
Functor
→ Bifunctor
, Endofunctor
, Profunctor
Group
→ Groupoid
Monoid
→ Category
, Comonad
, Comonoid
, Monad
Semigroup
→ Cosemigroup
, Semigroupoid
Lan
→ Day
, Density
, Coyoneda
Ran
→ Codensity
, Yoneda
or ways of combining other types
Bimonoid
(and Bimonad
),Duoid
,Lattice,
Functor/Monoidal
,Semiring
, Rig
, Ring
, and Field
.As much as possible, these are defined at multiple levels. E.g.
./Monoid/Type
is a kind-polymorphic monoid at the type level, where instances are defined for specific types (or type constructors), like 0
/+
or Some
/join
;./Monoid/Kind
is kind-level monoid, where instances are defined for specific kinds, like {}
/./Tuple/Type
for the kind Type
; andkProduct
at the top of most files is a sort-level monoid (well, a semigroup, since we have no unit kind), which is usually ./Tuple/Kind
, but may also be ./Either/Kind
.Things at the sort level can’t be “grouped” (or even bound) in any way, so we talk about kCat
forming a sort-level monoidal category (with Kind
as the objects and an undefinable unit), but can’t organize them any better than that.
As that last sentence implies, everything lives within a “Kind
-level” monoidal category, which you can think of as an approximation of Cat. The object of the category is implicitly Kind
, but we can’t specify that explicitly. We also have no way of representing common monoidal identities at the Kind-level (e.g., {}
and <>
have no Kind
-level equivalent), so there is no cat.unit
for the monoidal category. It actually forms a rig category, with ./Tuple/Kind
and ./Either/Kind
, but mostly you just see a monoidal view of it.
We also use a v…
convention when talking about enriched categories – like vObject
, vArrow
, etc. At least so far, the enriching category is always Set, so vObject = Type
and v = ./Category/Set
, but the convention helps us keep track of why we’re using those types.
Types as documentation: https://sellout.github.io/caterwaul/ (there actually are some docs there, but pretty minimal at the moment.)