Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::category::IsAdjunction Concept Referenceexport
module dedekind.category

A typed unit/counit witness relating a left and right functor. More...

Concept definition

template<typename Left, typename Right, typename Unit, typename Counit>
concept dedekind::category::IsAdjunction =
HasAdjunctionShape<Left, Right> && IsUnitOfAdjunction<Unit, Left, Right> &&
IsCounitOfAdjunction<Counit, Left, Right>
dedekind::category::HasAdjunctionShape
Structural shape: F and U have the categorical signature of an adjoint pair F ⊣ U — F : 𝒟 → 𝒞 (left,...
Definition adjunction.cppm:122
dedekind::category::IsAdjunction
A typed unit/counit witness relating a left and right functor.
Definition adjunction.cppm:211
dedekind::category::IsCounitOfAdjunction
Structural shape: ε is the counit of an adjunction F ⊣ U — a natural transformation F ∘ U ⇒ id_𝒞....
Definition adjunction.cppm:189
dedekind::category::IsUnitOfAdjunction
Structural shape: η is the unit of an adjunction F ⊣ U — a natural transformation id_𝒟 ⇒ U ∘ F.
Definition adjunction.cppm:177

Detailed Description

A typed unit/counit witness relating a left and right functor.

Tightened (#434) to require the unit and counit to be natural transformations, not raw arrows. Per Mac Lane (Ch. IV) / Milewski (Category Theory for Programmers, Ch. on Adjunctions): an adjunction is defined by natural transformations; the earlier arrow-based form (pre-#434) was structurally under-strict. The arrow-shape constraints on Unit / Counit are retained via IsNaturalTransformation's own requirements.

The triangle identities — (εF) ∘ (Fη) = 1_F and (Gε) ∘ (ηG) = 1_G — remain universal-property territory; they're the engineer's honesty obligation at the witness site.