dedekind::category::IsOrderEmbedding Concept Reference

An order-preserving embedding: a monic, order-preserving arrow of one ordered set into another. Such an embedding is a covariant functor between the two posetal categories, so IsCovariantFunctor is a conjunct — the classification is derived from the two legs (IsEmbeddingFunctor && IsMonotone), not re-declared per carrier (#908). More...

Concept definition

template<typename F, typename Op std::less_equal<>>
concept dedekind::category::IsOrderEmbedding =  IsEmbeddingFunctor<F> && IsCovariantFunctor<F, Op>

Detailed Description

An order-preserving embedding: a monic, order-preserving arrow of one ordered set into another. Such an embedding is a covariant functor between the two posetal categories, so IsCovariantFunctor is a conjunct — the classification is derived from the two legs (IsEmbeddingFunctor && IsMonotone), not re-declared per carrier (#908).

The general rule behind the per-carrier witnesses: the carrier- lattice inclusions ℕ↪ℤ↪ℚ↪ℝ (e.g. :morphologies' embed_sint_ℤ_) each satisfy it, and each is thereby a covariant functor. Naming the composite once lets a downstream site witness IsOrderEmbedding rather than re-deriving both legs, and makes the "order-embedding @c ⟹ covariant functor" inference visible.

Template Parameters

F	the embedding arrow.
Op	the order it preserves; defaults to std::less_equal<>.