User-declared monotonicity witness for an arrow type F with respect to the ambient order relation Op.
More...
Detailed Description
struct dedekind::category::monotone_trait< F, Op >
User-declared monotonicity witness for an arrow type F with respect to the ambient order relation Op.
Monotonicity cannot be verified at compile time in general (it quantifies over all input pairs); users specialise this to true to declare that F preserves the order Op (∀ x, y: Op(x, y) ⇒ Op(F(x), F(y))). The compiler trusts the declaration; the public review process is the audit trail. Mirrors is_monic_arrow_v in :morphism (same opt-in pattern).
Default relation std::less_equal<> matches the partition convention (see partition header).
The trait behind is_monotone_v, a struct so that a downstream module can state the fact for a whole arrow family at once (a partial specialisation on the family's pattern; a variable-template partial specialisation does not fire across module boundaries, a struct's does): the theorem that every Preimage<F> preserves inclusion is stated once, not tagged per instance.
The documentation for this struct was generated from the following file:
- src/main/modules/dedekind/category/posetal.cppm
