dedekind::category::IsCoproduct Concept Reference

Categorification of std::variant<A, B> as the categorical coproduct (A + B). More...

Concept definition

template<typename T, typename A, typename B, typename Op AnyOperation>
concept dedekind::category::IsCoproduct = 
    
    
    (std::same_as<Op, AnyOperation> &&
     requires(A a, B b) {
       { T(a) } -> std::same_as<T>;
       { T(b) } -> std::same_as<T>;
     }) ||
    
    
    
    
    
    
    
    requires(const A& a, const B& b) {
      { Op::inl(a) } -> std::convertible_to<T>;
      { Op::inr(b) } -> std::convertible_to<T>;
    }

Detailed Description

Categorification of std::variant<A, B> as the categorical coproduct (A + B).

A coproduct of A and B is an object C equipped with injection morphisms ι₁: A → C and ι₂: B → C such that for any object X with morphisms f: A → X and g: B → X, there exists a unique morphism v: C → X making the following diagram commute:

A       B
 \     /
 ι₁   ι₂
   \ /
    C
   / \
  f   g
 /     \
X       X

std::variant<A, B> satisfies this concept: any value of type A or B can be injected into the variant, and std::visit provides the universal elimination morphism.

Note

(#881) The Op-refinement (the injection factory Op::inl / Op::inr) is landed here for symmetry with IsProduct's pairing factory, but its consumer is not the set join (which is product-shaped). Its home is the set-expression collapse: the reduced-form outcome space {Ø, Singleton, Interval, Set, U} is a coproduct and each collapse rule is an injection into one summand (see #865, and the boundary injections Set{AlwaysTrue/False} == U/Ø in #685). The recursive case (fold over an initial F-algebra, ℕ = μX.1+X) is #449. Until one of those lands, the Op parameter is exercised only by its own witnesses.