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

Concept definition

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

concept dedekind::category::IsOrderAntiIsomorphism = IsBijectiveArrow<F> && IsAntiMonotone<F, Op>

dedekind::category::IsAntiMonotone

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

Definition posetal.cppm:432

dedekind::category::IsBijectiveArrow

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

Definition morphism.cppm:1283

dedekind::category::IsOrderAntiIsomorphism

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

Definition posetal.cppm:496

Detailed Description

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

Composes IsBijectiveArrow with IsAntiMonotone. Under this class, halfspace-pivot transport remains clean but the direction (Upward / Downward) is flipped — the structural reason multiplicative scaling by a negative scalar on an ordered field flips the halfspace's direction.