Imported Upstream version 0.4

1 files changed, 70 insertions, 4 deletions

diff --git a/src/Relation/Binary.agda b/src/Relation/Binary.agda
index 1940876..c5aaed4 100644
--- a/src/Relation/Binary.agda
+++ b/src/Relation/Binary.agda
@@ -8,11 +8,12 @@ module Relation.Binary where
 
 open import Data.Product
 open import Data.Sum
-open import Data.Function
+open import Function
 open import Level
 import Relation.Binary.PropositionalEquality.Core as PropEq
 open import Relation.Binary.Consequences
 open import Relation.Binary.Core as Core using (_≡_)
+import Relation.Binary.Indexed.Core as I
 
 ------------------------------------------------------------------------
 -- Simple properties and equivalence relations
@@ -31,13 +32,16 @@ record IsPreorder {a ℓ₁ ℓ₂} {A : Set a}
     -- Reflexivity is expressed in terms of an underlying equality:
     reflexive     : _≈_ ⇒ _∼_
     trans         : Transitive _∼_
-    ∼-resp-≈      : _∼_ Respects₂ _≈_
 
   module Eq = IsEquivalence isEquivalence
 
   refl : Reflexive _∼_
   refl = reflexive Eq.refl
 
+  ∼-resp-≈ : _∼_ Respects₂ _≈_
+  ∼-resp-≈ = (λ x≈y z∼x → trans z∼x (reflexive x≈y))
+           , (λ x≈y x∼z → trans (reflexive $ Eq.sym x≈y) x∼z)
+
 record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≈_ _∼_
   field
@@ -67,12 +71,24 @@ record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
     { isEquivalence = PropEq.isEquivalence
     ; reflexive     = reflexive
     ; trans         = trans
-    ; ∼-resp-≈      = PropEq.resp₂ _≈_
     }
 
-  preorder : Preorder c zero ℓ
+  preorder : Preorder c c ℓ
   preorder = record { isPreorder = isPreorder }
 
+  -- A trivially indexed setoid.
+
+  indexedSetoid : ∀ {i} {I : Set i} → I.Setoid I c _
+  indexedSetoid = record
+    { Carrier = λ _ → Carrier
+    ; _≈_     = _≈_
+    ; isEquivalence = record
+      { refl  = refl
+      ; sym   = sym
+      ; trans = trans
+      }
+    }
+
 ------------------------------------------------------------------------
 -- Decidable equivalence relations
 
@@ -126,6 +142,56 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   preorder = record { isPreorder = isPreorder }
 
 ------------------------------------------------------------------------
+-- Decidable partial orders
+
+record IsDecPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
+                         (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
+                         Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+  infix 4 _≟_ _≤?_
+  field
+    isPartialOrder : IsPartialOrder _≈_ _≤_
+    _≟_            : Decidable _≈_
+    _≤?_           : Decidable _≤_
+
+  private
+    module PO = IsPartialOrder isPartialOrder
+  open PO public hiding (module Eq)
+
+  module Eq where
+
+    isDecEquivalence : IsDecEquivalence _≈_
+    isDecEquivalence = record
+      { isEquivalence = PO.isEquivalence
+      ; _≟_           = _≟_
+      }
+
+    open IsDecEquivalence isDecEquivalence public
+
+record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≤_
+  field
+    Carrier           : Set c
+    _≈_               : Rel Carrier ℓ₁
+    _≤_               : Rel Carrier ℓ₂
+    isDecPartialOrder : IsDecPartialOrder _≈_ _≤_
+
+  private
+    module DPO = IsDecPartialOrder isDecPartialOrder
+  open DPO public hiding (module Eq)
+
+  poset : Poset c ℓ₁ ℓ₂
+  poset = record { isPartialOrder = isPartialOrder }
+
+  open Poset poset public using (preorder)
+
+  module Eq where
+
+    decSetoid : DecSetoid c ℓ₁
+    decSetoid = record { isDecEquivalence = DPO.Eq.isDecEquivalence }
+
+    open DecSetoid decSetoid public
+
+------------------------------------------------------------------------
 -- Strict partial orders
 
 record IsStrictPartialOrder {a ℓ₁ ℓ₂} {A : Set a}