dedekind::category::IsPairProjection Concept Reference

Whether F is the projection \(\pi_K\) out of a pair: the recogniser the law readers (:cartesian, a product's defining form) and the hyperdoctrine (relational:graph) read. A genuine std::pair only: a pair-like carrier with more state is no product of its two members. More...

Concept definition

template<typename F, std::size_t K>
concept dedekind::category::IsPairProjection = 
    IsArrow<F> &&
    requires {
      typename Dom<F>::first_type;
      typename Dom<F>::second_type;
    } &&
    std::same_as<Dom<F>, std::pair<typename Dom<F>::first_type,
                                   typename Dom<F>::second_type>> &&
    std::same_as<F, Π<K, Dom<F>>>

Detailed Description

Whether F is the projection \(\pi_K\) out of a pair: the recogniser the law readers (:cartesian, a product's defining form) and the hyperdoctrine (relational:graph) read. A genuine std::pair only: a pair-like carrier with more state is no product of its two members.

Template Parameters

F	an arrow.
K	the slot.