dedekind::category::IsComonad Concept Reference

The Unified Comonadic Proof: Co-Kleisli Action as Contextual Being. More...

Concept definition

template<typename W, typename ε_t, typename δ_t>
concept dedekind::category::IsComonad = 
    IsEndofunctor<W> &&
    
    IsNaturalTransformation<ε_t, W, identity_functor<typename W::Σ_cat>> &&
    
    IsNaturalTransformation<δ_t, W, composite_functor<W, W>> &&
 
    (requires(ε_t ε, δ_t δ, typename W::Σ_cat::Arrow::Domain c) {
      requires IsIdentityArrow<decltype(ε(c))> &&
                   IsIdentityArrow<decltype(δ(c))>;
    } || is_comonadic<W, ε_t, δ_t>::value)

Detailed Description

The Unified Comonadic Proof: Co-Kleisli Action as Contextual Being.

monad__Comonadic_Morphisms

This concept bridges the dual formal definitions:

1. Co-Kleisli Triple (Action): Existence of ε (Extract) and <<= (Extend).
2. Comonoid in Endofunctors (Structure): F is a Functor with δ (Duplicate).

As with IsMonad, the laws are stated over a single object label from the source category. The corresponding contextual objects are recovered through identity lifting, which is the canonical witness mechanism in this library's single-species categories.

monad__The_Mereological_Pull

Following the Dedekind posture, we do not require δ (Duplicate/Coreturn) to be explicitly defined if <<= (Extend) is present, as δ is the "Self-Extend": δ(w) = w <<= id.