Imported Upstream version 0.6

1 files changed, 20 insertions, 26 deletions

diff --git a/src/Data/Fin/Dec.agda b/src/Data/Fin/Dec.agda
index 0bee913..7ac8cb2 100644
--- a/src/Data/Fin/Dec.agda
+++ b/src/Data/Fin/Dec.agda
@@ -19,11 +19,11 @@ open import Data.Product as Prod
 open import Data.Empty
 open import Function
 import Function.Equivalence as Eq
-open import Relation.Binary
+open import Relation.Binary as B
 import Relation.Binary.HeterogeneousEquality as H
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
-open import Relation.Unary using (Pred)
+open import Relation.Unary as U using (Pred)
 
 infix 4 _∈?_
 
@@ -36,17 +36,15 @@ suc n ∈? s ∷ p       with n ∈? p
 
 private
 
-  restrictP : ∀ {n} → (Fin (suc n) → Set) → (Fin n → Set)
+  restrictP : ∀ {p n} → (Fin (suc n) → Set p) → (Fin n → Set p)
   restrictP P f = P (suc f)
 
-  restrict : ∀ {n} {P : Fin (suc n) → Set} →
-             (∀ f → Dec (P f)) →
-             (∀ f → Dec (restrictP P f))
+  restrict : ∀ {p n} {P : Fin (suc n) → Set p} →
+             U.Decidable P → U.Decidable (restrictP P)
   restrict dec f = dec (suc f)
 
 any? : ∀ {n} {P : Fin n → Set} →
-       ((f : Fin n) → Dec (P f)) →
-       Dec (∃ P)
+       U.Decidable P → Dec (∃ P)
 any? {zero}  {P} dec = no (((λ()) ∶ ¬ Fin 0) ∘ proj₁)
 any? {suc n} {P} dec with dec zero | any? (restrict dec)
 ...                  | yes p | _            = yes (_ , p)
@@ -62,17 +60,18 @@ nonempty? p = any? (λ x → x ∈? p)
 
 private
 
-  restrict∈ : ∀ {n} P {Q : Fin (suc n) → Set} →
+  restrict∈ : ∀ {p q n}
+              (P : Fin (suc n) → Set p) {Q : Fin (suc n) → Set q} →
               (∀ {f} → Q f → Dec (P f)) →
               (∀ {f} → restrictP Q f → Dec (restrictP P f))
   restrict∈ _ dec {f} Qf = dec {suc f} Qf
 
-decFinSubset : ∀ {n} {P Q : Fin n → Set} →
-               (∀ f → Dec (Q f)) →
+decFinSubset : ∀ {p q n} {P : Fin n → Set p} {Q : Fin n → Set q} →
+               U.Decidable Q →
                (∀ {f} → Q f → Dec (P f)) →
                Dec (∀ {f} → Q f → P f)
-decFinSubset {zero}          _    _    = yes λ{}
-decFinSubset {suc n} {P} {Q} decQ decP = helper
+decFinSubset {n = zero}          _    _    = yes λ{}
+decFinSubset {n = suc n} {P} {Q} decQ decP = helper
   where
   helper : Dec (∀ {f} → Q f → P f)
   helper with decFinSubset (restrict decQ) (restrict∈ P decP)
@@ -91,21 +90,19 @@ decFinSubset {suc n} {P} {Q} decQ decP = helper
     hlpr zero    q₀ = ⊥-elim (¬q₀ q₀)
     hlpr (suc f) qf = q⟶p qf
 
-all∈? : ∀ {n} {P : Fin n → Set} {q} →
+all∈? : ∀ {n p} {P : Fin n → Set p} {q} →
         (∀ {f} → f ∈ q → Dec (P f)) →
         Dec (∀ {f} → f ∈ q → P f)
 all∈? {q = q} dec = decFinSubset (λ f → f ∈? q) dec
 
-all? : ∀ {n} {P : Fin n → Set} →
-       (∀ f → Dec (P f)) →
-       Dec (∀ f → P f)
+all? : ∀ {n p} {P : Fin n → Set p} →
+       U.Decidable P → Dec (∀ f → P f)
 all? dec with all∈? {q = ⊤} (λ {f} _ → dec f)
 ...      | yes ∀p = yes (λ f → ∀p ∈⊤)
 ...      | no ¬∀p = no  (λ ∀p → ¬∀p (λ {f} _ → ∀p f))
 
 decLift : ∀ {n} {P : Fin n → Set} →
-          (∀ x → Dec (P x)) →
-          (∀ p → Dec (Lift P p))
+          U.Decidable P → U.Decidable (Lift P)
 decLift dec p = all∈? (λ {x} _ → dec x)
 
 private
@@ -114,14 +111,11 @@ private
   restrictSP s P p = P (s ∷ p)
 
   restrictS : ∀ {n} {P : Subset (suc n) → Set} →
-              (s : Side) →
-              (∀ p → Dec (P p)) →
-              (∀ p → Dec (restrictSP s P p))
+              (s : Side) → U.Decidable P → U.Decidable (restrictSP s P)
   restrictS s dec p = dec (s ∷ p)
 
 anySubset? : ∀ {n} {P : Subset n → Set} →
-             (∀ s → Dec (P s)) →
-             Dec (∃ P)
+             U.Decidable P → Dec (∃ P)
 anySubset? {zero} {P} dec with dec []
 ... | yes P[] = yes (_ , P[])
 ... | no ¬P[] = no helper
@@ -142,7 +136,7 @@ anySubset? {suc n} {P} dec with anySubset? (restrictS inside  dec)
 -- then we can find the smallest value for which this is the case.
 
 ¬∀⟶∃¬-smallest :
-  ∀ n {p} (P : Fin n → Set p) → (∀ i → Dec (P i)) →
+  ∀ n {p} (P : Fin n → Set p) → U.Decidable P →
   ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
 ¬∀⟶∃¬-smallest zero    P dec ¬∀iPi = ⊥-elim (¬∀iPi (λ()))
 ¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi with dec zero
@@ -166,7 +160,7 @@ anySubset? {suc n} {P} dec with anySubset? (restrictS inside  dec)
 
 infix 4 _⊆?_
 
-_⊆?_ : ∀ {n} → Decidable (_⊆_ {n = n})
+_⊆?_ : ∀ {n} → B.Decidable (_⊆_ {n = n})
 p₁ ⊆? p₂ =
   Dec.map (Eq.sym NaturalPoset.orders-equivalent) $
   Dec.map′ PropVecEq.to-≡ PropVecEq.from-≡ $