Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::category::IsClosureForcing Concept Referenceexport
module dedekind.category

Composite: structural shape + opt-in canonicality. The full witness that Op is the closure-forcing operator A → B (or A × A → B), with B the canonical recipient. More...

Concept definition

template<typename Op, typename A, typename B>
concept dedekind::category::IsClosureForcing =
HasClosureForcingShape<Op, A, B> && is_closure_forcing_v<Op, A, B>
dedekind::category::HasClosureForcingShape
Structural shape: Op{} sends (A, A) → B (binary) or A → B (unary) with A ≠ B. Pure deducible clause o...
Definition total.cppm:1164
dedekind::category::IsClosureForcing
Composite: structural shape + opt-in canonicality. The full witness that Op is the closure-forcing op...
Definition total.cppm:1202
dedekind::category::is_closure_forcing_v
constexpr bool is_closure_forcing_v
Opt-in trait carrying the universal-property clause of IsClosureForcing — the engineer's honesty obli...
Definition total.cppm:1186

Detailed Description

Composite: structural shape + opt-in canonicality. The full witness that Op is the closure-forcing operator A → B (or A × A → B), with B the canonical recipient.

Operationally: IsClosureForcing<std::negate<>, Cardinality, SignedCardinality> witnesses that -Cardinality (unary) is the Grothendieck embedding's operator-level shadow. Similarly IsClosureForcing<std::minus<>, Cardinality, SignedCardinality> for the binary case.