An arrow that is both an order-preserving map and a bijection. More...

Concept definition

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

concept dedekind::category::IsOrderIsomorphism = IsBijectiveArrow<F> && IsMonotone<F, Op>

dedekind::category::IsBijectiveArrow

An arrow declared to be both a monomorphism (ι: A ↣ B) and an epimorphism (π: A ↠ B),...

Definition morphism.cppm:1283

dedekind::category::IsMonotone

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

Definition posetal.cppm:406

dedekind::category::IsOrderIsomorphism

An arrow that is both an order-preserving map and a bijection.

Definition posetal.cppm:483

Detailed Description

An arrow that is both an order-preserving map and a bijection.

Composes the categorical bijection certificate (:morphism::IsBijectiveArrow = IsMonicArrow && IsEpicArrow) with the order-preservation trait above. This is the textbook "enabling" class for clean halfspace- pivot transport in :algebra:halfspace_transport: the image of a halfspace under an order-iso is again a halfspace.