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

Structural shape: η is the unit of an adjunction F ⊣ U — a natural transformation id_𝒟 ⇒ U ∘ F. More...

Concept definition

template<typename Eta, typename F, typename U>
concept dedekind::category::IsUnitOfAdjunction =
HasAdjunctionShape<F, U> &&
IsNaturalTransformation<Eta, identity_functor<typename F::Σ_cat>,
composite_functor<F, U>>
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::IsNaturalTransformation
A family of components, one per object, whose square commutes at every arrow of the source: for eac...
Definition natural.cppm:342
dedekind::category::IsUnitOfAdjunction
Structural shape: η is the unit of an adjunction F ⊣ U — a natural transformation id_𝒟 ⇒ U ∘ F.
Definition adjunction.cppm:177
dedekind::category::composite_functor
Composite Functor G . F (Maps CatS -> CatT -> CatU).
Definition functor.cppm:344

Detailed Description

Structural shape: η is the unit of an adjunction F ⊣ U — a natural transformation id_𝒟 ⇒ U ∘ F.

Composes the existing IsNaturalTransformation (in :natural) with HasAdjunctionShape. The triangle identities — the actual content of the adjunction — remain universal-property territory (engineer's honesty obligation; not deducible by the type-checker).

In carrier-lattice terms, η_d : d → U(F(d)) is the canonical embedding of d into the underlying object of its free construction — for example, η_ℕ : ℕ ↪ ℤ is the variant-level analog of embed_uint_sint_. Closes #434.