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

A carrier A equipped with a structure map F<A> -> A. More...

Concept definition

template<typename Carrier, typename Structure, typename Functor>
concept dedekind::category::IsFAlgebra =
IsEndofunctor<Functor> && IsArrow<Structure> &&
std::same_as<Dom<Structure>, typename Functor::template Shape<Carrier>> &&
std::same_as<Cod<Structure>, Carrier>
dedekind::category::IsArrow
A type that knows its own Domain (A) and Codomain (B), objects it maps between: called at the domain'...
Definition morphism.cppm:168
dedekind::category::IsEndofunctor
A structure-preserving mapping from a Category back to itself (F : 𝒞 → 𝒞).
Definition functor.cppm:474
dedekind::category::IsFAlgebra
A carrier A equipped with a structure map F<A> -> A.
Definition functor.cppm:502

Detailed Description

A carrier A equipped with a structure map F<A> -> A.

See also
dedekind.algebra:universal (IsAlgebra<T, Ops...>) for the universal-algebra (A, F) reading. Per the textbook isomorphism Alg(Σ) ≅ F_Σ-Alg (Pierce 1991, Basic Category Theory for Computer Scientists §2.2): every universal-algebra IsAlgebra<T, Ops...> corresponds to an IsFAlgebra here for the polynomial endofunctor F_Σ generated by the signature Σ = (Ops...).