: the DIAGONAL notion Δ:A→A×A --- an arrow whose Codomain is the square of its Domain (the comonoid comultiplication / fan-out). Copy is the canonical MODEL; this concept is the matchable "diagonal" handle. Purely structural: it names the crossed A→A×A signature, not that the map is a↦(a,a) (that is Copy's own obligation). Cartesian only: the non-cartesian ⊗ setting needs the carrier generalized past std::pair (#951); a type carrying more than one arrow reading needs the dom/cod contract (#952). More...

Concept definition

template<typename F>

concept dedekind::category::IsCopy = IsArrow<F> && std::same_as<Cod<F>, std::pair<Dom<F>, Dom<F>>>

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::IsCopy

: the DIAGONAL notion Δ:A→A×A --- an arrow whose Codomain is the square of its Domain (the comonoid c...

Definition cartesian_bicategory.cppm:185

dedekind::category::Dom

typename std::remove_cvref_t< F >::Domain Dom

Shorthand to look up the Domain of an Arrow type F.

Definition morphism.cppm:231

Detailed Description

: the DIAGONAL notion Δ:A→A×A --- an arrow whose Codomain is the square of its Domain (the comonoid comultiplication / fan-out). Copy is the canonical MODEL; this concept is the matchable "diagonal" handle. Purely structural: it names the crossed A→A×A signature, not that the map is a↦(a,a) (that is Copy's own obligation). Cartesian only: the non-cartesian ⊗ setting needs the carrier generalized past std::pair (#951); a type carrying more than one arrow reading needs the dom/cod contract (#952).