Detailed Description

template<typename T, typename η_t, typename μ_t>
struct dedekind::category::is_monadic< T, η_t, μ_t >

T : C -> C with η : Id ⟹ T and μ : T² ⟹ T.

monad__Monadic_and_Comonadic_Components

The concrete implementations of η (Unit), μ (Multiplication), ε (Counit), and δ (Comultiplication) are defined in the :natural partition for each supported monad/comonad type (e.g., η for Maybe, Identity, Box). These are specific overloads, not generic template-template helpers.

This design follows the tag dispatch of the :functor partition, avoiding C++ limitations with template-template parameter overloading and maintaining clean partition boundaries.

Textbook alignment:

η (eta): unit/pure [defined in :natural]
μ (mu): multiplication [defined in :natural]
ε (epsilon): counit [defined in :natural]
δ (delta): comultiplication [defined in :natural]

monad__Monad_as_Monoid

We bridge the gap: η (Unit) <--> unit_v (Monoid Unit) μ (Multiplication) <--> Op (Monoid Operation)

In the project's single-species setting, the component laws are checked against an object label c, then transported into the endofunctor context by lifting the identity arrow id_c(c). This is how the type system recovers the object witnesses T(c) and T(T(c)) needed for η and μ.

Textbook note: this concept intentionally requires T to satisfy IsEndofunctor. Therefore, a functor that changes the ambient category (for example Set<T> -> Set<std::optional<T>>) is not admitted as an IsMonad witness in this formalization, even if value-level η/μ/κ behavior exists for its carrier.

Trait: η and μ satisfy the monad laws on T, associativity \(\mu \circ T\mu = \mu \circ \mu T\) and the two unit laws \(\mu \circ T\eta = \mathrm{id} = \mu \circ \eta T\). A certificate, primary false: the two sides of each law are different types that denote one arrow, so no type shows them. Decided without it where both components are identities (the identity monad), by the unit law.

Template Parameters

T	the endofunctor.
η_t
μ_t	its unit and multiplication.

The documentation for this struct was generated from the following file:

src/main/modules/dedekind/category/monad.cppm