Imported Upstream version 0.3

1 files changed, 287 insertions, 0 deletions

diff --git a/src/Relation/Binary.agda b/src/Relation/Binary.agda
new file mode 100644
index 0000000..1940876
--- /dev/null
+++ b/src/Relation/Binary.agda
@@ -0,0 +1,287 @@
+------------------------------------------------------------------------
+-- Properties of homogeneous binary relations
+------------------------------------------------------------------------
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Relation.Binary where
+
+open import Data.Product
+open import Data.Sum
+open import Data.Function
+open import Level
+import Relation.Binary.PropositionalEquality.Core as PropEq
+open import Relation.Binary.Consequences
+open import Relation.Binary.Core as Core using (_≡_)
+
+------------------------------------------------------------------------
+-- Simple properties and equivalence relations
+
+open Core public hiding (_≡_; refl; _≢_)
+
+------------------------------------------------------------------------
+-- Preorders
+
+record IsPreorder {a ℓ₁ ℓ₂} {A : Set a}
+                  (_≈_ : Rel A ℓ₁) -- The underlying equality.
+                  (_∼_ : Rel A ℓ₂) -- The relation.
+                  : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    isEquivalence : IsEquivalence _≈_
+    -- Reflexivity is expressed in terms of an underlying equality:
+    reflexive     : _≈_ ⇒ _∼_
+    trans         : Transitive _∼_
+    ∼-resp-≈      : _∼_ Respects₂ _≈_
+
+  module Eq = IsEquivalence isEquivalence
+
+  refl : Reflexive _∼_
+  refl = reflexive Eq.refl
+
+record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _∼_
+  field
+    Carrier    : Set c
+    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
+    _∼_        : Rel Carrier ℓ₂  -- The relation.
+    isPreorder : IsPreorder _≈_ _∼_
+
+  open IsPreorder isPreorder public
+
+------------------------------------------------------------------------
+-- Setoids
+
+-- Equivalence relations are defined in Relation.Binary.Core.
+
+record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix 4 _≈_
+  field
+    Carrier       : Set c
+    _≈_           : Rel Carrier ℓ
+    isEquivalence : IsEquivalence _≈_
+
+  open IsEquivalence isEquivalence public
+
+  isPreorder : IsPreorder _≡_ _≈_
+  isPreorder = record
+    { isEquivalence = PropEq.isEquivalence
+    ; reflexive     = reflexive
+    ; trans         = trans
+    ; ∼-resp-≈      = PropEq.resp₂ _≈_
+    }
+
+  preorder : Preorder c zero ℓ
+  preorder = record { isPreorder = isPreorder }
+
+------------------------------------------------------------------------
+-- Decidable equivalence relations
+
+record IsDecEquivalence {a ℓ} {A : Set a}
+                        (_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where
+  infix 4 _≟_
+  field
+    isEquivalence : IsEquivalence _≈_
+    _≟_           : Decidable _≈_
+
+  open IsEquivalence isEquivalence public
+
+record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix 4 _≈_
+  field
+    Carrier          : Set c
+    _≈_              : Rel Carrier ℓ
+    isDecEquivalence : IsDecEquivalence _≈_
+
+  open IsDecEquivalence isDecEquivalence public
+
+  setoid : Setoid c ℓ
+  setoid = record { isEquivalence = isEquivalence }
+
+  open Setoid setoid public using (preorder)
+
+------------------------------------------------------------------------
+-- Partial orders
+
+record IsPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
+                      (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
+                      Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    isPreorder : IsPreorder _≈_ _≤_
+    antisym    : Antisymmetric _≈_ _≤_
+
+  open IsPreorder isPreorder public
+         renaming (∼-resp-≈ to ≤-resp-≈)
+
+record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≤_
+  field
+    Carrier        : Set c
+    _≈_            : Rel Carrier ℓ₁
+    _≤_            : Rel Carrier ℓ₂
+    isPartialOrder : IsPartialOrder _≈_ _≤_
+
+  open IsPartialOrder isPartialOrder public
+
+  preorder : Preorder c ℓ₁ ℓ₂
+  preorder = record { isPreorder = isPreorder }
+
+------------------------------------------------------------------------
+-- Strict partial orders
+
+record IsStrictPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
+                            (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
+                            Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    isEquivalence : IsEquivalence _≈_
+    irrefl        : Irreflexive _≈_ _<_
+    trans         : Transitive _<_
+    <-resp-≈      : _<_ Respects₂ _≈_
+
+  module Eq = IsEquivalence isEquivalence
+
+record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _<_
+  field
+    Carrier              : Set c
+    _≈_                  : Rel Carrier ℓ₁
+    _<_                  : Rel Carrier ℓ₂
+    isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
+
+  open IsStrictPartialOrder isStrictPartialOrder public
+
+------------------------------------------------------------------------
+-- Total orders
+
+record IsTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
+                    (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
+                    Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    isPartialOrder : IsPartialOrder _≈_ _≤_
+    total          : Total _≤_
+
+  open IsPartialOrder isPartialOrder public
+
+record TotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≤_
+  field
+    Carrier      : Set c
+    _≈_          : Rel Carrier ℓ₁
+    _≤_          : Rel Carrier ℓ₂
+    isTotalOrder : IsTotalOrder _≈_ _≤_
+
+  open IsTotalOrder isTotalOrder public
+
+  poset : Poset c ℓ₁ ℓ₂
+  poset = record { isPartialOrder = isPartialOrder }
+
+  open Poset poset public using (preorder)
+
+------------------------------------------------------------------------
+-- Decidable total orders
+
+record IsDecTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
+                       (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
+                       Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+  infix 4 _≟_ _≤?_
+  field
+    isTotalOrder : IsTotalOrder _≈_ _≤_
+    _≟_          : Decidable _≈_
+    _≤?_         : Decidable _≤_
+
+  private
+    module TO = IsTotalOrder isTotalOrder
+  open TO public hiding (module Eq)
+
+  module Eq where
+
+    isDecEquivalence : IsDecEquivalence _≈_
+    isDecEquivalence = record
+      { isEquivalence = TO.isEquivalence
+      ; _≟_           = _≟_
+      }
+
+    open IsDecEquivalence isDecEquivalence public
+
+record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≤_
+  field
+    Carrier         : Set c
+    _≈_             : Rel Carrier ℓ₁
+    _≤_             : Rel Carrier ℓ₂
+    isDecTotalOrder : IsDecTotalOrder _≈_ _≤_
+
+  private
+    module DTO = IsDecTotalOrder isDecTotalOrder
+  open DTO public hiding (module Eq)
+
+  totalOrder : TotalOrder c ℓ₁ ℓ₂
+  totalOrder = record { isTotalOrder = isTotalOrder }
+
+  open TotalOrder totalOrder public using (poset; preorder)
+
+  module Eq where
+
+    decSetoid : DecSetoid c ℓ₁
+    decSetoid = record { isDecEquivalence = DTO.Eq.isDecEquivalence }
+
+    open DecSetoid decSetoid public
+
+------------------------------------------------------------------------
+-- Strict total orders
+
+-- Note that these orders are decidable (see compare).
+
+record IsStrictTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
+                          (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
+                          Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    isEquivalence : IsEquivalence _≈_
+    trans         : Transitive _<_
+    compare       : Trichotomous _≈_ _<_
+    <-resp-≈      : _<_ Respects₂ _≈_
+
+  infix 4 _≟_ _<?_
+
+  _≟_ : Decidable _≈_
+  _≟_ = tri⟶dec≈ compare
+
+  _<?_ : Decidable _<_
+  _<?_ = tri⟶dec< compare
+
+  isDecEquivalence : IsDecEquivalence _≈_
+  isDecEquivalence = record
+    { isEquivalence = isEquivalence
+    ; _≟_           = _≟_
+    }
+
+  module Eq = IsDecEquivalence isDecEquivalence
+
+  isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
+  isStrictPartialOrder = record
+    { isEquivalence = isEquivalence
+    ; irrefl        = tri⟶irr <-resp-≈ Eq.sym compare
+    ; trans         = trans
+    ; <-resp-≈      = <-resp-≈
+    }
+
+  open IsStrictPartialOrder isStrictPartialOrder public using (irrefl)
+
+record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _<_
+  field
+    Carrier            : Set c
+    _≈_                : Rel Carrier ℓ₁
+    _<_                : Rel Carrier ℓ₂
+    isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
+
+  open IsStrictTotalOrder isStrictTotalOrder public
+    hiding (module Eq)
+
+  strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
+  strictPartialOrder =
+    record { isStrictPartialOrder = isStrictPartialOrder }
+
+  decSetoid : DecSetoid c ℓ₁
+  decSetoid = record { isDecEquivalence = isDecEquivalence }
+
+  module Eq = DecSetoid decSetoid