------------------------------------------------------------------------ -- The Agda standard library -- -- Convenient syntax for "equational reasoning" using a partial order ------------------------------------------------------------------------ -- Example uses: -- -- u≤x : u ≤ x -- u≤x = begin -- u ≈⟨ u≈v ⟩ -- v ≡⟨ v≡w ⟩ -- w <⟨ w≤x ⟩ -- x ∎ -- -- u<x : u < x -- u<x = begin-strict -- u ≈⟨ u≈v ⟩ -- v ≡⟨ v≡w ⟩ -- w <⟨ w≤x ⟩ -- x ∎ -- -- u<e : u < e -- u<e = begin-strict -- u ≈⟨ u≈v ⟩ -- v ≡⟨ v≡w ⟩ -- w <⟨ w<x ⟩ -- x ≤⟨ x≤y ⟩ -- y <⟨ y<z ⟩ -- z ≡⟨ d≡z ⟨ -- d ≈⟨ e≈d ⟨ -- e ∎ -- -- u≈w : u ≈ w -- u≈w = begin-equality -- u ≈⟨ u≈v ⟩ -- v ≡⟨ v≡w ⟩ -- w ∎ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Bundles using (Poset) module Relation.Binary.Reasoning.PartialOrder {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where open Poset P open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as Strict using (_<_) ------------------------------------------------------------------------ -- Re-export contents of base module open import Relation.Binary.Reasoning.Base.Triple isPreorder (Strict.<-asym antisym) (Strict.<-trans isPartialOrder) (Strict.<-resp-≈ isEquivalence ≤-resp-≈) Strict.<⇒≤ (Strict.<-≤-trans Eq.sym trans antisym ≤-respʳ-≈) (Strict.≤-<-trans trans antisym ≤-respˡ-≈) public