dedekind::category::HasAdjunctionShape Concept Reference

Structural shape: F and U have the categorical signature of an adjoint pair F ⊣ U — F : 𝒟 → 𝒞 (left, free) and U : 𝒞 → 𝒟 (right, forgetful). More...

Concept definition

template<typename F, typename U>
concept dedekind::category::HasAdjunctionShape = 
    IsShapedFunctor<F> && IsShapedFunctor<U> &&
    std::same_as<typename F::Σ_cat,
                 typename U::Τ_cat> &&  
    std::same_as<typename F::Τ_cat,
                 typename U::Σ_cat>

Detailed Description

Structural shape: F and U have the categorical signature of an adjoint pair F ⊣ U — F : 𝒟 → 𝒞 (left, free) and U : 𝒞 → 𝒟 (right, forgetful).

Concept-level test: both are functors, and their categorical signatures are compatible — F's source category equals U's target category (both are 𝒟), and F's target category equals U's source category (both are 𝒞).

Relationship to IsAdjunction (defined below): IsAdjunction is the stronger 4-parameter witness <Left, Right, Unit, Counit> that requires explicit unit / counit arrows and exercises the typed triangle-identity surface. HasAdjunctionShape is the structural-only 2-parameter form that names just the signatures of the adjoint pair, leaving the unit / counit unspecified. Used in the directional aliases IsFreeFunctor / IsForgetfulFunctor below, where the directional reading is what's load-bearing rather than the unit / counit content.

The content of the adjunction (the natural isomorphism, the triangle identities) is universal-property territory that the type-checker cannot quantify over; engineers asserting "this F, U pair forms an adjunction" either provide the explicit unit / counit (use IsAdjunction) or carry the proof obligation as an opt-in trait (the HasAdjunctionShape route).