dedekind::category::IsProduct Concept Reference

Categorification of std::pair<A, B> as the categorical product (A × B). More...

Concept definition

template<typename P, typename A, typename B, typename Op AnyOperation>
concept dedekind::category::IsProduct =  requires(P p) {
  
  
  
  
  { π_1(p) } -> std::convertible_to<A>;
  { π_2(p) } -> std::convertible_to<B>;
} && (std::same_as<Op, AnyOperation> || requires(const A& a, const B& b) {
                      
                      
                      
                      
                      { Op{}(a, b) } -> std::convertible_to<P>;
                    })

Detailed Description

Categorification of std::pair<A, B> as the categorical product (A × B).

A product of A and B is an object P equipped with projection morphisms π₁: P → A and π₂: P → B such that for any object X with morphisms f: X → A and g: X → B, there exists a unique morphism u: X → P making the following diagram commute:

        X
       /|\
     f/ | \g
     /  u  \         (u is the unique mediating morphism)
    /   |   \
   v    v    v
   A ←  P  → B
      π₁   π₂
 
commutes:  f = π₁ ∘ u   and   g = π₂ ∘ u

The membership test is against the canonical projections π_1 / π_2 (above), NOT the raw .first / .second: std::pair, Complex and Rational satisfy it through the default .first / .second projection, while Dual satisfies it through its val / der overload — the P-leg is uniform across every product-shaped carrier regardless of storage names.

Template Parameters

Op

The pairing-constructor FACTORY the product commits to, defaulting to AnyOperation (unconstrained; the base case, ignored). A named Op must build the product: Op{}(a,b) is convertible to P (the Haskell pair constructor (,) specialised to P). Its result type is the discriminator, so the lattice AST tells a meet-pairing (MakeMeet, pullback legs) from a join-pairing (MakeJoin, pushout colegs) without a separate concept. #881.