------------------------------------------------------------------------ -- The Agda standard library -- -- Properties satisfied by preorders ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Bundles using (Preorder; Setoid) module Relation.Binary.Properties.Preorder {p₁ p₂ p₃} (P : Preorder p₁ p₂ p₃) where open import Function.Base using (flip) open import Data.Product.Base as Product using (_×_; _,_; swap) import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd using (isPreorder; preorder) open import Relation.Binary.Structures using (IsPreorder) open Preorder P ------------------------------------------------------------------------ -- The converse relation is also a preorder. converse-isPreorder : IsPreorder _≈_ _≳_ converse-isPreorder = EqAndOrd.isPreorder isPreorder converse-preorder : Preorder p₁ p₂ p₃ converse-preorder = EqAndOrd.preorder P ------------------------------------------------------------------------ -- For every preorder there is an induced equivalence InducedEquivalence : Setoid _ _ InducedEquivalence = record { _≈_ = λ x y → x ≲ y × x ≳ y ; isEquivalence = record { refl = (refl , refl) ; sym = swap ; trans = Product.zip trans (flip trans) } } ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ -- Please use the new names as continuing support for the old names is -- not guaranteed. -- Version 2.0 invIsPreorder = converse-isPreorder {-# WARNING_ON_USAGE invIsPreorder "Warning: invIsPreorder was deprecated in v2.0. Please use converse-isPreorder instead." #-} invPreorder = converse-preorder {-# WARNING_ON_USAGE invPreorder "Warning: invPreorder was deprecated in v2.0. Please use converse-preorder instead." #-}