Carrier A is the initial F-algebra for endofunctor F with structure map α. More...

Concept definition

template<typename F, typename A, typename α>
concept dedekind::category::IsInitialFAlgebra = 
    IsFAlgebra<A, α, F> && is_initial_f_algebra_v<F, A, α>

Detailed Description

Carrier A is the initial F-algebra for endofunctor F with structure map α.

Combines the structural-shape clause IsFAlgebra (from :functor) with the universal-property opt-in trait above. The structural part is mechanically checked; the universal-property part is the engineer's honesty obligation.

The catamorphism cata(β) : A → B for any F-algebra (B, β) is the unique morphism guaranteed by initiality; its operational discharge is filed as a sibling concern.