monad.cppm File Reference

Monads and Comonads (Context as Algebra). More...

#include <concepts>
#include <functional>
#include <type_traits>
import dedekind.category:morphism;

Include dependency graph for monad.cppm:

Classes
struct	dedekind::category::is_monadic< T, η_t, μ_t >
	T : C -> C with η : Id ⟹ T and μ : T² ⟹ T. More...
struct	dedekind::category::is_comonadic< W, ε_t, δ_t >
	Trait: the comonad laws for ε and δ on W, the duals. More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsMonad
concept	dedekind::category::IsComonad
	The Unified Comonadic Proof: Co-Kleisli Action as Contextual Being.

Detailed Description

Monads and Comonads (Context as Algebra).

@partition :monad

This partition internalizes monads and comonads as endofunctor-level algebraic structure. Because categories in this library are specialized to a single Species type, the object witness used by the laws is always recovered through the identity arrow id_c(x) rather than through a separate textbook object universe.

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

Note

"The introduction of the digit 0 or the group concept was general nonsense too, and mathematics was more or less stagnating for thousands of years because nobody was around to take such childish steps." – Alexander Grothendieck, letter to Ronald Brown (5 May 1982)