dedekind::category::IsVariant Concept Reference

An arrow with a definite variance: order-preserving (IsMonotone) or order-reversing (IsAntiMonotone). The leg-shape of a Galois connection, whose adjoints are always one or the other. Mirrors :limit::IsBoundaryObject's "X @c || @c dual" disjunction shape. More...

Concept definition

template<typename F, typename Op std::less_equal<>>
concept dedekind::category::IsVariant = 
    
    
    
    IsArrow<F> &&
    
    
    
    
    
    (
        requires(Op op, Dom<F> a) { op(a, a); } ||
        requires(Op op, Cod<F> c) { op(c, c); }) &&
    (IsMonotone<F, Op> || IsAntiMonotone<F, Op>)

Detailed Description

An arrow with a definite variance: order-preserving (IsMonotone) or order-reversing (IsAntiMonotone). The leg-shape of a Galois connection, whose adjoints are always one or the other. Mirrors :limit::IsBoundaryObject's "X @c || @c dual" disjunction shape.

Note

Variance is DERIVED for the structured arrows and ASSERTED for the irreducible leaf maps (#908). Derived: Identity and the negation NegationArrow (below), and the spider Copy / Merge whose monotonicity is a theorem gated on IsOrderMeetSemilattice (:cartesian_bicategory). Asserted: atomic order-preserving maps (the ℕ↪ℤ / sint / uint embeddings) register is_monotone_v directly, since their variance is a fact about that specific map, not a consequence of its type ("inference composes, tagging explodes": tag only the irreducible leaves). A general op-derived variance-composition law (co∘co=co, antitone∘antitone=monotone) awaits a reified composition arrow; the two-axis (contravariant-domain / covariant-codomain) reading is the hyperdoctrine extension.