Imported Upstream version 0.5

1 files changed, 32 insertions, 20 deletions

diff --git a/src/Relation/Binary/List/Pointwise.agda b/src/Relation/Binary/List/Pointwise.agda
index d0314f0..04a4fe0 100644
--- a/src/Relation/Binary/List/Pointwise.agda
+++ b/src/Relation/Binary/List/Pointwise.agda
@@ -2,6 +2,8 @@
 -- Pointwise lifting of relations to lists
 ------------------------------------------------------------------------
 
+{-# OPTIONS --universe-polymorphism #-}
+
 module Relation.Binary.List.Pointwise where
 
 open import Function
@@ -13,47 +15,54 @@ open import Relation.Binary renaming (Rel to Rel₂)
 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
 
 private
- module Dummy {A : Set} where
+ module Dummy {a} {A : Set a} where
 
   infixr 5 _∷_
 
-  data Rel (_∼_ : Rel₂ A zero) : List A → List A → Set where
+  data Rel {ℓ} (_∼_ : Rel₂ A ℓ) : List A → List A → Set (ℓ ⊔ a) where
     []  : Rel _∼_ [] []
     _∷_ : ∀ {x xs y ys} (x∼y : x ∼ y) (xs∼ys : Rel _∼_ xs ys) →
           Rel _∼_ (x ∷ xs) (y ∷ ys)
 
-  head : ∀ {_∼_ x y xs ys} → Rel _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y
+  head : ∀ {ℓ} {_∼_ : Rel₂ A ℓ} {x y xs ys} →
+         Rel _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y
   head (x∼y ∷ xs∼ys) = x∼y
 
-  tail : ∀ {_∼_ x y xs ys} → Rel _∼_ (x ∷ xs) (y ∷ ys) → Rel _∼_ xs ys
+  tail : ∀ {ℓ} {_∼_ : Rel₂ A ℓ} {x y xs ys} →
+         Rel _∼_ (x ∷ xs) (y ∷ ys) → Rel _∼_ xs ys
   tail (x∼y ∷ xs∼ys) = xs∼ys
 
-  reflexive : ∀ {_≈_ _∼_} → _≈_ ⇒ _∼_ → Rel _≈_ ⇒ Rel _∼_
+  reflexive : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} →
+              _≈_ ⇒ _∼_ → Rel _≈_ ⇒ Rel _∼_
   reflexive ≈⇒∼ []            = []
   reflexive ≈⇒∼ (x≈y ∷ xs≈ys) = ≈⇒∼ x≈y ∷ reflexive ≈⇒∼ xs≈ys
 
-  refl : ∀ {_∼_} → Reflexive _∼_ → Reflexive (Rel _∼_)
+  refl : ∀ {ℓ} {_∼_ : Rel₂ A ℓ} →
+         Reflexive _∼_ → Reflexive (Rel _∼_)
   refl rfl {[]}     = []
   refl rfl {x ∷ xs} = rfl ∷ refl rfl
 
-  symmetric : ∀ {_∼_} → Symmetric _∼_ → Symmetric (Rel _∼_)
+  symmetric : ∀ {ℓ} {_∼_ : Rel₂ A ℓ} →
+              Symmetric _∼_ → Symmetric (Rel _∼_)
   symmetric sym []            = []
   symmetric sym (x∼y ∷ xs∼ys) = sym x∼y ∷ symmetric sym xs∼ys
 
-  transitive : ∀ {_∼_} → Transitive _∼_ → Transitive (Rel _∼_)
+  transitive : ∀ {ℓ} {_∼_ : Rel₂ A ℓ} →
+               Transitive _∼_ → Transitive (Rel _∼_)
   transitive trans []            []            = []
   transitive trans (x∼y ∷ xs∼ys) (y∼z ∷ ys∼zs) =
     trans x∼y y∼z ∷ transitive trans xs∼ys ys∼zs
 
-  antisymmetric : ∀ {_≈_ _≤_} → Antisymmetric _≈_ _≤_ →
+  antisymmetric : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel₂ A ℓ₁} {_≤_ : Rel₂ A ℓ₂} →
+                  Antisymmetric _≈_ _≤_ →
                   Antisymmetric (Rel _≈_) (Rel _≤_)
   antisymmetric antisym []            []            = []
   antisymmetric antisym (x∼y ∷ xs∼ys) (y∼x ∷ ys∼xs) =
     antisym x∼y y∼x ∷ antisymmetric antisym xs∼ys ys∼xs
 
-  respects₂ : ∀ {_≈_ _∼_} →
+  respects₂ : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} →
               _∼_ Respects₂ _≈_ → (Rel _∼_) Respects₂ (Rel _≈_)
-  respects₂ {_≈_} {_∼_} resp =
+  respects₂ {_} {_} {_≈_} {_∼_} resp =
     (λ {xs} {ys} {zs} → resp¹ {xs} {ys} {zs}) ,
     (λ {xs} {ys} {zs} → resp² {xs} {ys} {zs})
     where
@@ -67,7 +76,8 @@ private
     resp² (x≈y ∷ xs≈ys) (x∼z ∷ xs∼zs) =
       proj₂ resp x≈y x∼z ∷ resp² xs≈ys xs∼zs
 
-  decidable : ∀ {_∼_} → Decidable _∼_ → Decidable (Rel _∼_)
+  decidable : ∀ {ℓ} {_∼_ : Rel₂ A ℓ} →
+              Decidable _∼_ → Decidable (Rel _∼_)
   decidable dec []       []       = yes []
   decidable dec []       (y ∷ ys) = no (λ ())
   decidable dec (x ∷ xs) []       = no (λ ())
@@ -77,14 +87,15 @@ private
   ...           | no ¬xs∼ys = no (¬xs∼ys ∘ tail)
   ...           | yes xs∼ys = yes (x∼y ∷ xs∼ys)
 
-  isEquivalence : ∀ {_≈_} → IsEquivalence _≈_ → IsEquivalence (Rel _≈_)
+  isEquivalence : ∀ {ℓ} {_≈_ : Rel₂ A ℓ} →
+                  IsEquivalence _≈_ → IsEquivalence (Rel _≈_)
   isEquivalence eq = record
     { refl  = refl       Eq.refl
     ; sym   = symmetric  Eq.sym
     ; trans = transitive Eq.trans
     } where module Eq = IsEquivalence eq
 
-  isPreorder : ∀ {_≈_ _∼_} →
+  isPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} →
                IsPreorder _≈_ _∼_ → IsPreorder (Rel _≈_) (Rel _∼_)
   isPreorder pre = record
     { isEquivalence = isEquivalence Pre.isEquivalence
@@ -92,14 +103,15 @@ private
     ; trans         = transitive    Pre.trans
     } where module Pre = IsPreorder pre
 
-  isDecEquivalence : ∀ {_≈_} → IsDecEquivalence _≈_ →
+  isDecEquivalence : ∀ {ℓ} {_≈_ : Rel₂ A ℓ} → IsDecEquivalence _≈_ →
                      IsDecEquivalence (Rel _≈_)
   isDecEquivalence eq = record
     { isEquivalence = isEquivalence Dec.isEquivalence
     ; _≟_           = decidable     Dec._≟_
     } where module Dec = IsDecEquivalence eq
 
-  isPartialOrder : ∀ {_≈_ _≤_} → IsPartialOrder _≈_ _≤_ →
+  isPartialOrder : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel₂ A ℓ₁} {_≤_ : Rel₂ A ℓ₂} →
+                   IsPartialOrder _≈_ _≤_ →
                    IsPartialOrder (Rel _≈_) (Rel _≤_)
   isPartialOrder po = record
     { isPreorder = isPreorder    PO.isPreorder
@@ -118,22 +130,22 @@ private
 
 open Dummy public
 
-preorder : Preorder _ _ _ → Preorder _ _ _
+preorder : ∀ {p₁ p₂ p₃} → Preorder p₁ p₂ p₃ → Preorder _ _ _
 preorder p = record
   { isPreorder = isPreorder (Preorder.isPreorder p)
   }
 
-setoid : Setoid _ _ → Setoid _ _
+setoid : ∀ {c ℓ} → Setoid c ℓ → Setoid _ _
 setoid s = record
   { isEquivalence = isEquivalence (Setoid.isEquivalence s)
   }
 
-decSetoid : DecSetoid _ _ → DecSetoid _ _
+decSetoid : ∀ {c ℓ} → DecSetoid c ℓ → DecSetoid _ _
 decSetoid d = record
   { isDecEquivalence = isDecEquivalence (DecSetoid.isDecEquivalence d)
   }
 
-poset : Poset _ _ _ → Poset _ _ _
+poset : ∀ {c ℓ₁ ℓ₂} → Poset c ℓ₁ ℓ₂ → Poset _ _ _
 poset p = record
   { isPartialOrder = isPartialOrder (Poset.isPartialOrder p)
   }