A covariant functor between posetal categories: an order-PRESERVING arrow. This is IsMonotone read categorically (a monotone map is a functor of posets that preserves the direction of composition), the documented covariant pole of functor variance (#908). More...

Concept definition

template<typename F, typename Op std::less_equal<>>

concept dedekind::category::IsCovariantFunctor = IsMonotone<F, Op>

dedekind::category::IsCovariantFunctor

A covariant functor between posetal categories: an order-PRESERVING arrow. This is IsMonotone read ca...

Definition adjunction.cppm:315

dedekind::category::IsMonotone

An arrow F declared to be order-preserving with respect to the ambient order relation Op.

Definition posetal.cppm:406

Detailed Description

A covariant functor between posetal categories: an order-PRESERVING arrow. This is IsMonotone read categorically (a monotone map is a functor of posets that preserves the direction of composition), the documented covariant pole of functor variance (#908).

Inhabited by every monotone arrow: Identity, the dominance inclusion LiftLogic ι:𝔹↪Ω, the comonoid legs Copy / Merge, the product bifunctor Tensor, and any Compose of covariant legs.

Template Parameters

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