Adapted Dominique's patches to my taste. Made more things polymorphic.

+ Some definitions were made less polymorphic (one level argument
  instead of several) in order to avoid code duplication.

Author: nad

.boring

@@ -4,4 +4,3 @@
 ^dist($|/)
 ^html($|/)
 ^Everything\.agda$
-dist

LICENCE

@@ -1,7 +1,8 @@
 Copyright (c) 2007-2011 Nils Anders Danielsson, Ulf Norell, Shin-Cheng
 Mu, Samuel Bronson, Dan Doel, Patrik Jansson, Liang-Ting Chen,
 Jean-Philippe Bernardy, Andrés Sicard-Ramírez, Nicolas Pouillard,
-Darin Morrison, Peter Berry, Daniel Brown, Simon Foster, Dominique Devriese
+Darin Morrison, Peter Berry, Daniel Brown, Simon Foster, Dominique
+Devriese
 
 Permission is hereby granted, free of charge, to any person obtaining a
 copy of this software and associated documentation files (the

README.agda

@@ -5,9 +5,9 @@ module README where
 --
 -- Author: Nils Anders Danielsson, with contributions from
 -- Jean-Philippe Bernardy, Peter Berry, Samuel Bronson, Daniel Brown,
--- Liang-Ting Chen, Dan Doel, Simon Foster, Patrik Jansson, Darin
--- Morrison, Shin-Cheng Mu, Ulf Norell, Nicolas Pouillard, Andrés
--- Sicard-Ramírez and Dominique Devriese
+-- Liang-Ting Chen, Dominique Devriese, Dan Doel, Simon Foster, Patrik
+-- Jansson, Darin Morrison, Shin-Cheng Mu, Ulf Norell, Nicolas
+-- Pouillard and Andrés Sicard-Ramírez
 ------------------------------------------------------------------------
 
 -- Note that the development version of the library often requires the

src/Data/List/All.agda

@@ -1,15 +1,16 @@
 ------------------------------------------------------------------------
 -- Lists where all elements satisfy a given property
 ------------------------------------------------------------------------
+
 {-# OPTIONS --universe-polymorphism #-}
 
 module Data.List.All where
 
-open import Level
-open import Function
 open import Data.List as List hiding (map; all)
 open import Data.List.Any as Any using (here; there)
 open Any.Membership-≡ using (_∈_; _⊆_)
+open import Function
+open import Level
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
 open import Relation.Unary using () renaming (_⊆_ to _⋐_)
@@ -19,17 +20,20 @@ open import Relation.Binary.PropositionalEquality
 
 infixr 5 _∷_
 
-data All {p a} {A : Set a} (P : A → Set p) : List A → Set (p ⊔ a) where
+data All {a p} {A : Set a}
+         (P : A → Set p) : List A → Set (p ⊔ a) where
   []  : All P []
   _∷_ : ∀ {x xs} (px : P x) (pxs : All P xs) → All P (x ∷ xs)
 
-head : ∀ {p a} {A : Set a} {P : A → Set p} {x xs} → All P (x ∷ xs) → P x
+head : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} →
+       All P (x ∷ xs) → P x
 head (px ∷ pxs) = px
 
-tail : ∀ {p a} {A : Set a} {P : A → Set p} {x xs} → All P (x ∷ xs) → All P xs
+tail : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} →
+       All P (x ∷ xs) → All P xs
 tail (px ∷ pxs) = pxs
 
-lookup : ∀ {p a} {A : Set a} {P : A → Set p} {xs : List A} →
+lookup : ∀ {a p} {A : Set a} {P : A → Set p} {xs : List A} →
          All P xs → (∀ {x : A} → x ∈ xs → P x)
 lookup []         ()
 lookup (px ∷ pxs) (here refl)  = px
@@ -45,7 +49,7 @@ map : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} →
 map g []         = []
 map g (px ∷ pxs) = g px ∷ map g pxs
 
-all : ∀ {p a} {A : Set a} {P : A → Set p} →
+all : ∀ {a p} {A : Set a} {P : A → Set p} →
       (∀ x → Dec (P x)) → (xs : List A) → Dec (All P xs)
 all p []       = yes []
 all p (x ∷ xs) with p x

src/Data/List/All/Properties.agda

@@ -1,6 +1,7 @@
 ------------------------------------------------------------------------
 -- Properties relating All to various list functions
 ------------------------------------------------------------------------
+
 {-# OPTIONS --universe-polymorphism #-}
 
 module Data.List.All.Properties where
@@ -19,20 +20,23 @@ open import Relation.Unary using () renaming (_⊆_ to _⋐_)
 
 -- Functions can be shifted between the predicate and the list.
 
-All-map : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p} {f : A → B} {xs} →
+All-map : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
+            {f : A → B} {xs} →
           All (P ∘ f) xs → All P (List.map f xs)
 All-map []       = []
 All-map (p ∷ ps) = p ∷ All-map ps
 
-map-All : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p} {f : A → B} {xs} →
+map-All : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
+            {f : A → B} {xs} →
           All P (List.map f xs) → All (P ∘ f) xs
 map-All {xs = []}    []       = []
 map-All {xs = _ ∷ _} (p ∷ ps) = p ∷ map-All ps
 
 -- A variant of All.map.
 
-gmap : ∀ {a b p q} {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q}
-       {f : A → B} →
+gmap : ∀ {a b p q}
+         {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q}
+         {f : A → B} →
        P ⋐ Q ∘ f → All P ⋐ All Q ∘ List.map f
 gmap g = All-map ∘ All.map g
 

src/Data/List/Any.agda

@@ -1,6 +1,7 @@
 ------------------------------------------------------------------------
 -- Lists where at least one element satisfies a given property
 ------------------------------------------------------------------------
+
 {-# OPTIONS --universe-polymorphism #-}
 
 module Data.List.Any where
@@ -26,7 +27,8 @@ open import Relation.Binary.PropositionalEquality as PropEq
 
 -- Any P xs means that at least one element in xs satisfies P.
 
-data Any {a p : Level} {A : Set a} (P : A → Set p) : List A → Set (a ⊔ p) where
+data Any {a p} {A : Set a}
+         (P : A → Set p) : List A → Set (a ⊔ p) where
   here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)
   there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)
 
@@ -39,14 +41,14 @@ map g (there pxs) = there (map g pxs)
 
 -- If the head does not satisfy the predicate, then the tail will.
 
-tail : ∀ {a} {A : Set a} {x : A} {xs : List A} {P : A → Set} →
+tail : ∀ {a p} {A : Set a} {x : A} {xs : List A} {P : A → Set p} →
        ¬ P x → Any P (x ∷ xs) → Any P xs
 tail ¬px (here  px)  = ⊥-elim (¬px px)
 tail ¬px (there pxs) = pxs
 
 -- Decides Any.
 
-any : {a : Level} {A : Set a} {P : A → Set} →
+any : ∀ {a p} {A : Set a} {P : A → Set p} →
       (∀ x → Dec (P x)) → (xs : List A) → Dec (Any P xs)
 any p []       = no λ()
 any p (x ∷ xs) with p x
@@ -55,7 +57,8 @@ any p (x ∷ xs) | no ¬px = Dec.map′ there (tail ¬px) (any p xs)
 
 -- index x∈xs is the list position (zero-based) which x∈xs points to.
 
-index : ∀ {a} {A : Set a} {P : A → Set} {xs} → Any P xs → Fin (List.length xs)
+index : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
+        Any P xs → Fin (List.length xs)
 index (here  px)  = zero
 index (there pxs) = suc (index pxs)
 
@@ -72,7 +75,8 @@ module Membership {c ℓ : Level} (S : Setoid c ℓ) where
   -- If a predicate P respects the underlying equality then Any P
   -- respects the list equality.
 
-  lift-resp : ∀ {P} → P Respects _≈_ → Any P Respects _≋_
+  lift-resp : ∀ {p} {P : A → Set p} →
+              P Respects _≈_ → Any P Respects _≋_
   lift-resp resp []            ()
   lift-resp resp (x≈y ∷ xs≈ys) (here px)   = here (resp x≈y px)
   lift-resp resp (x≈y ∷ xs≈ys) (there pxs) =
@@ -82,7 +86,7 @@ module Membership {c ℓ : Level} (S : Setoid c ℓ) where
 
   infix 4 _∈_ _∉_
 
-  _∈_ : A → List A → Set (c ⊔ ℓ)
+  _∈_ : A → List A → Set _
   x ∈ xs = Any (_≈_ x) xs
 
   _∉_ : A → List A → Set _
@@ -126,18 +130,20 @@ module Membership {c ℓ : Level} (S : Setoid c ℓ) where
 
   -- A variant of List.map.
 
-  map-with-∈ : ∀ {b} {B : Set b} (xs : List A) → (∀ {x} → x ∈ xs → B) → List B
+  map-with-∈ : ∀ {b} {B : Set b}
+               (xs : List A) → (∀ {x} → x ∈ xs → B) → List B
   map-with-∈ []       f = []
   map-with-∈ (x ∷ xs) f = f (here S.refl) ∷ map-with-∈ xs (f ∘ there)
 
   -- Finds an element satisfying the predicate.
 
-  find : ∀ {p} {P : A → Set p} {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
+  find : ∀ {p} {P : A → Set p} {xs} →
+         Any P xs → ∃ λ x → x ∈ xs × P x
   find (here px)   = (_ , here S.refl , px)
   find (there pxs) = Prod.map id (Prod.map there id) (find pxs)
 
-  lose : ∀ {p} {P : A → Set p} {x xs} → P Respects _≈_ →
-         x ∈ xs → P x → Any P xs
+  lose : ∀ {p} {P : A → Set p} {x xs} →
+         P Respects _≈_ → x ∈ xs → P x → Any P xs
   lose resp x∈xs px = map (flip resp px) x∈xs
 
 -- The code above instantiated (and slightly changed) for
@@ -149,12 +155,13 @@ module Membership-≡ where
     open module M {a} {A : Set a} = Membership (PropEq.setoid A) public
       hiding (lift-resp; lose; ⊆-preorder; module ⊆-Reasoning)
 
-  lose : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} → x ∈ xs → P x → Any P xs
+  lose : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} →
+         x ∈ xs → P x → Any P xs
   lose {P = P} = M.lose (PropEq.subst P)
 
   -- _⊆_ is a preorder.
 
-  ⊆-preorder : {a : Level} → Set a → Preorder _ _ _
+  ⊆-preorder : ∀ {a} → Set a → Preorder _ _ _
   ⊆-preorder A = Ind.InducedPreorder₂ (PropEq.setoid (List A)) _∈_
                                       (PropEq.subst (_∈_ _))
 
@@ -163,17 +170,17 @@ module Membership-≡ where
   open Inv public
     using (Kind) renaming (equivalent to set; inverse to bag)
 
-  [_]-Equality : Kind → {a : Level} → Set a → Setoid _ _
+  [_]-Equality : Kind → ∀ {a} → Set a → Setoid _ _
   [ k ]-Equality A = Inv.InducedEquivalence₂ k (_∈_ {A = A})
 
   infix 4 _≈[_]_
 
-  _≈[_]_ : {a : Level} {A : Set a} → List A → Kind → List A → Set _
-  _≈[_]_ {a} {A} xs k ys = Setoid._≈_ ([ k ]-Equality A) xs ys
+  _≈[_]_ : ∀ {a} {A : Set a} → List A → Kind → List A → Set _
+  _≈[_]_ {A = A} xs k ys = Setoid._≈_ ([ k ]-Equality A) xs ys
 
   -- Bag equality implies set equality.
 
-  bag-=⇒set-= : {a : Level} {A : Set a} {xs ys : List A} →
+  bag-=⇒set-= : ∀ {a} {A : Set a} {xs ys : List A} →
                 xs ≈[ bag ] ys → xs ≈[ set ] ys
   bag-=⇒set-= xs≈ys = Inv.⇿⇒ xs≈ys
 
@@ -182,17 +189,17 @@ module Membership-≡ where
   module ⊆-Reasoning where
     import Relation.Binary.PreorderReasoning as PreR
     private
-      open module PR {A : Set} = PreR (⊆-preorder A) public
+      open module PR {a} {A : Set a} = PreR (⊆-preorder A) public
         renaming (_∼⟨_⟩_ to _⊆⟨_⟩_; _≈⟨_⟩_ to _≡⟨_⟩_)
 
     infixr 2 _≈⟨_⟩_
     infix  1 _∈⟨_⟩_
 
-    _∈⟨_⟩_ : ∀ {A : Set} x {xs ys : List A} →
+    _∈⟨_⟩_ : ∀ {a} {A : Set a} x {xs ys : List A} →
              x ∈ xs → xs IsRelatedTo ys → x ∈ ys
     x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs
 
-    _≈⟨_⟩_ : ∀ {k} {A : Set} xs {ys zs : List A} →
+    _≈⟨_⟩_ : ∀ {k a} {A : Set a} xs {ys zs : List A} →
              xs ≈[ k ] ys → ys IsRelatedTo zs → xs IsRelatedTo zs
     xs ≈⟨ xs≈ys ⟩ ys≈zs =
       xs ⊆⟨ _⟨$⟩_ (Equivalent.to (Inv.⇒⇔ xs≈ys)) ⟩ ys≈zs
@@ -202,5 +209,6 @@ module Membership-≡ where
 
 -- If any element satisfies P, then P is satisfied.
 
-satisfied : ∀ {a p} {A : Set a} {P : A → Set p} {xs} → Any P xs → ∃ P
+satisfied : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
+            Any P xs → ∃ P
 satisfied = Prod.map id Prod.proj₂ ∘ Membership-≡.find