Imported Upstream version 0.6

34 files changed, 1093 insertions, 262 deletions

diff --git a/Everything.agda b/Everything.agda
index 68c42b8..e637ad7 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -192,9 +192,15 @@ import Data.Graph.Acyclic
 -- Integers
 import Data.Integer
 
+-- Properties related to addition of integers
+import Data.Integer.Addition.Properties
+
 -- Divisibility and coprimality
 import Data.Integer.Divisibility
 
+-- Properties related to multiplication of integers
+import Data.Integer.Multiplication.Properties
+
 -- Some properties about integers
 import Data.Integer.Properties
 
diff --git a/LICENCE b/LICENCE
index 158f19b..5c7fc6e 100644
--- a/LICENCE
+++ b/LICENCE
@@ -2,7 +2,7 @@ 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, Andreas Abel, Alcatel-Lucent
+Devriese, Andreas Abel, Alcatel-Lucent, Eric Mertens
 
 Permission is hereby granted, free of charge, to any person obtaining a
 copy of this software and associated documentation files (the
diff --git a/README.agda b/README.agda
index 578c7eb..b92e92b 100644
--- a/README.agda
+++ b/README.agda
@@ -1,19 +1,19 @@
 module README where
 
 ------------------------------------------------------------------------
--- The Agda standard library
+-- The Agda standard library, version 0.6
 --
 -- Author: Nils Anders Danielsson, with contributions from Andreas
 -- Abel, Jean-Philippe Bernardy, Peter Berry, Samuel Bronson, Daniel
 -- Brown, Liang-Ting Chen, Dominique Devriese, Dan Doel, Simon Foster,
--- Patrik Jansson, Alan Jeffrey, Darin Morrison, Shin-Cheng Mu, Ulf
--- Norell, Nicolas Pouillard and Andrés Sicard-Ramírez
+-- Patrik Jansson, Alan Jeffrey, Eric Mertens, 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
--- latest development version of Agda.
+-- This version of the library has been tested using Agda 2.3.0.
 
--- Note also that no guarantees are currently made about forwards or
+-- Note that no guarantees are currently made about forwards or
 -- backwards compatibility, the library is still at an experimental
 -- stage.
 
@@ -252,10 +252,12 @@ import IO
 -- More documentation
 ------------------------------------------------------------------------
 
--- Some examples showing where the natural numbers and some related
--- operations and properties are defined, and how they can be used:
+-- Some examples showing where the natural numbers/integers and some
+-- related operations and properties are defined, and how they can be
+-- used:
 
 import README.Nat
+import README.Integer
 
 -- Some examples showing how the AVL tree module can be used.
 
@@ -285,3 +287,13 @@ import README.Case
 -- For short descriptions of every library module, see Everything:
 
 import Everything
+
+-- Note that the Everything module is generated automatically. If you
+-- have downloaded the library from its darcs repository and want to
+-- type check README then you can (try to) construct Everything by
+-- running "cabal install && GenerateEverything".
+
+-- Note that all library sources are located under src or ffi. The
+-- modules README, README.* and Everything are not really part of the
+-- library, so these modules are located in the top-level directory
+-- instead.
diff --git a/README.txt b/README.txt
deleted file mode 100644
index e02b7a8..0000000
--- a/README.txt
+++ /dev/null
@@ -1,15 +0,0 @@
-------------------------------------------------------------------------
-The Agda standard library
-------------------------------------------------------------------------
-
-For information about the library, see README.agda.
-
-The README module imports the Everything module. This module is
-generated automatically; if you have downloaded the library from its
-darcs repository and want to type check README you can construct
-Everything by running "cabal install && GenerateEverything".
-
-Note that all library sources are located under src or ffi. The
-modules README, README.* and Everything are not really part of the
-library, so these modules are located in the top-level directory
-instead.
diff --git a/README/Integer.agda b/README/Integer.agda
new file mode 100644
index 0000000..c6e3469
--- /dev/null
+++ b/README/Integer.agda
@@ -0,0 +1,70 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some examples showing where the integers and some related
+-- operations and properties are defined, and how they can be used
+------------------------------------------------------------------------
+
+module README.Integer where
+
+-- The integers and various arithmetic operations are defined in
+-- Data.Integer.
+
+open import Data.Integer
+
+-- The +_ function converts natural numbers into integers.
+
+ex₁ : ℤ
+ex₁ = + 2
+
+-- The -_ function negates an integer.
+
+ex₂ : ℤ
+ex₂ = - + 4
+
+-- Some binary operators are also defined, including addition,
+-- subtraction and multiplication.
+
+ex₃ : ℤ
+ex₃ = + 1  +  + 3 * - + 2  -  + 4
+
+-- Propositional equality and some related properties can be found
+-- in Relation.Binary.PropositionalEquality.
+
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+
+ex₄ : ex₃ ≡ - + 9
+ex₄ = P.refl
+
+-- Data.Integer.Properties contains a number of properties related to
+-- integers. Algebra defines what a commutative ring is, among other
+-- things.
+
+open import Algebra
+import Data.Integer.Properties as Integer
+private
+  module CR = CommutativeRing Integer.commutativeRing
+
+ex₅ : ∀ i j → i * j ≡ j * i
+ex₅ i j = CR.*-comm i j
+
+-- The module ≡-Reasoning in Relation.Binary.PropositionalEquality
+-- provides some combinators for equational reasoning.
+
+open P.≡-Reasoning
+open import Data.Product
+
+ex₆ : ∀ i j → i * (j + + 0) ≡ j * i
+ex₆ i j = begin
+  i * (j + + 0)  ≡⟨ P.cong (_*_ i) (proj₂ CR.+-identity j) ⟩
+  i * j          ≡⟨ CR.*-comm i j ⟩
+  j * i          ∎
+
+-- The module RingSolver in Data.Integer.Properties contains a solver
+-- for integer equalities involving variables, constants, _+_, _*_, -_
+-- and _-_.
+
+ex₇ : ∀ i j → i * - j - j * i ≡ - + 2 * i * j
+ex₇ = solve 2 (λ i j → i :* :- j :- j :* i  :=  :- con (+ 2) :* i :* j)
+              P.refl
+  where open Integer.RingSolver
diff --git a/README/Nat.agda b/README/Nat.agda
index 5e6496b..4a2e978 100644
--- a/README/Nat.agda
+++ b/README/Nat.agda
@@ -48,7 +48,8 @@ ex₄ m n = begin
   n * m        ∎
 
 -- The module SemiringSolver in Data.Nat.Properties contains a solver
--- for natural number equalities involving constants, _+_ and _*_.
+-- for natural number equalities involving variables, constants, _+_
+-- and _*_.
 
 open Nat.SemiringSolver
 
diff --git a/lib.cabal b/lib.cabal
index a0c40cd..d5584bd 100644
--- a/lib.cabal
+++ b/lib.cabal
@@ -1,5 +1,5 @@
 name:            lib
-version:         0.0.2
+version:         0.1
 cabal-version:   >= 1.8
 build-type:      Simple
 description:     Helper programs.
diff --git a/release-notes b/release-notes
index fe54e58..a1ddf90 100644
--- a/release-notes
+++ b/release-notes
@@ -1,4 +1,26 @@
 ------------------------------------------------------------------------
+Version 0.6
+------------------------------------------------------------------------
+
+Version 0.6 of the standard library has now been released, see
+http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary.
+
+The library has been tested using Agda version 2.3.0.
+
+Note that no guarantees are made about backwards or forwards
+compatibility, the library is still at an experimental stage.
+
+If you want to compile the library using the MAlonzo compiler, then
+you should first install some supporting Haskell code, for instance as
+follows:
+
+  cd ffi
+  cabal install
+
+Currently the library does not support the Epic or JavaScript compiler
+backends.
+
+------------------------------------------------------------------------
 Version 0.5
 ------------------------------------------------------------------------
 
diff --git a/src/Algebra/Props/AbelianGroup.agda b/src/Algebra/Props/AbelianGroup.agda
index 37ecb5c..87d62a0 100644
--- a/src/Algebra/Props/AbelianGroup.agda
+++ b/src/Algebra/Props/AbelianGroup.agda
@@ -9,10 +9,15 @@ open import Algebra
 module Algebra.Props.AbelianGroup
          {g₁ g₂} (G : AbelianGroup g₁ g₂) where
 
-open AbelianGroup G
-import Relation.Binary.EqReasoning as EqR; open EqR setoid
-open import Function
+import Algebra.Props.Group as GP
 open import Data.Product
+open import Function
+import Relation.Binary.EqReasoning as EqR
+
+open AbelianGroup G
+open EqR setoid
+
+open GP group public
 
 private
   lemma : ∀ x y → x ∙ y ∙ x ⁻¹ ≈ y
@@ -23,8 +28,8 @@ private
     y ∙ ε           ≈⟨ proj₂ identity _ ⟩
     y               ∎
 
--‿∙-comm : ∀ x y → x ⁻¹ ∙ y ⁻¹ ≈ (x ∙ y) ⁻¹
--‿∙-comm x y = begin
+⁻¹-∙-comm : ∀ x y → x ⁻¹ ∙ y ⁻¹ ≈ (x ∙ y) ⁻¹
+⁻¹-∙-comm x y = begin
   x ⁻¹ ∙ y ⁻¹                         ≈⟨ comm _ _ ⟩
   y ⁻¹ ∙ x ⁻¹                         ≈⟨ sym $ lem ⟨ ∙-cong ⟩ refl ⟩
   x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹) ∙ x ⁻¹  ≈⟨ lemma _ _ ⟩
diff --git a/src/Algebra/Props/Ring.agda b/src/Algebra/Props/Ring.agda
index 61f1278..b48862a 100644
--- a/src/Algebra/Props/Ring.agda
+++ b/src/Algebra/Props/Ring.agda
@@ -8,10 +8,23 @@ open import Algebra
 
 module Algebra.Props.Ring {r₁ r₂} (R : Ring r₁ r₂) where
 
-open Ring R
-import Relation.Binary.EqReasoning as EqR; open EqR setoid
-open import Function
+import Algebra.Props.AbelianGroup as AGP
 open import Data.Product
+open import Function
+import Relation.Binary.EqReasoning as EqR
+
+open Ring R
+open EqR setoid
+
+open AGP +-abelianGroup public
+  renaming ( ⁻¹-involutive to -‿involutive
+           ; left-identity-unique to +-left-identity-unique
+           ; right-identity-unique to +-right-identity-unique
+           ; identity-unique to +-identity-unique
+           ; left-inverse-unique to +-left-inverse-unique
+           ; right-inverse-unique to +-right-inverse-unique
+           ; ⁻¹-∙-comm to -‿+-comm
+           )
 
 -‿*-distribˡ : ∀ x y → - x * y ≈ - (x * y)
 -‿*-distribˡ x y = begin
diff --git a/src/Algebra/RingSolver/AlmostCommutativeRing.agda b/src/Algebra/RingSolver/AlmostCommutativeRing.agda
index 802da61..748383b 100644
--- a/src/Algebra/RingSolver/AlmostCommutativeRing.agda
+++ b/src/Algebra/RingSolver/AlmostCommutativeRing.agda
@@ -111,7 +111,7 @@ fromCommutativeRing CR = record
       { isCommutativeSemiring = isCommutativeSemiring
       ; -‿cong                = -‿cong
       ; -‿*-distribˡ          = -‿*-distribˡ
-      ; -‿+-comm              = -‿∙-comm
+      ; -‿+-comm              = ⁻¹-∙-comm
       }
   }
   where
diff --git a/src/Data/Char.agda b/src/Data/Char.agda
index 4c768f4..e9fd661 100644
--- a/src/Data/Char.agda
+++ b/src/Data/Char.agda
@@ -6,11 +6,14 @@
 
 module Data.Char where
 
-open import Data.Nat  using (ℕ)
+open import Data.Nat using (ℕ)
+import Data.Nat.Properties as NatProp
 open import Data.Bool using (Bool; true; false)
 open import Relation.Nullary
 open import Relation.Binary
+import Relation.Binary.On as On
 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
+open import Relation.Binary.PropositionalEquality.TrustMe
 
 ------------------------------------------------------------------------
 -- The type
@@ -40,12 +43,16 @@ _==_ = primCharEquality
 _≟_ : Decidable {A = Char} _≡_
 s₁ ≟ s₂ with s₁ == s₂
 ... | true  = yes trustMe
-  where postulate trustMe : _
-... | false = no trustMe
-  where postulate trustMe : _
+... | false = no whatever
+  where postulate whatever : _
 
 setoid : Setoid _ _
 setoid = PropEq.setoid Char
 
 decSetoid : DecSetoid _ _
 decSetoid = PropEq.decSetoid _≟_
+
+-- An ordering induced by the toNat function.
+
+strictTotalOrder : StrictTotalOrder _ _ _
+strictTotalOrder = On.strictTotalOrder NatProp.strictTotalOrder toNat
diff --git a/src/Data/Fin.agda b/src/Data/Fin.agda
index 7bfa320..1f6be16 100644
--- a/src/Data/Fin.agda
+++ b/src/Data/Fin.agda
@@ -102,7 +102,7 @@ inject≤ (suc i) (Nat.s≤s le) = suc (inject≤ i le)
 ------------------------------------------------------------------------
 -- Operations
 
--- Fold.
+-- Folds.
 
 fold : ∀ (T : ℕ → Set) {m} →
        (∀ {n} → T n → T (suc n)) →
@@ -111,6 +111,15 @@ fold : ∀ (T : ℕ → Set) {m} →
 fold T f x zero    = x
 fold T f x (suc i) = f (fold T f x i)
 
+fold′ : ∀ {n t} (T : Fin (suc n) → Set t) →
+        (∀ i → T (inject₁ i) → T (suc i)) →
+        T zero →
+        ∀ i → T i
+fold′             T f x zero     = x
+fold′ {n = zero}  T f x (suc ())
+fold′ {n = suc n} T f x (suc i)  =
+  f i (fold′ (T ∘ inject₁) (f ∘ inject₁) x i)
+
 -- Lifts functions.
 
 lift : ∀ {m n} k → (Fin m → Fin n) → Fin (k N+ m) → Fin (k N+ n)
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-≡ $
diff --git a/src/Data/Integer.agda b/src/Data/Integer.agda
index f33484f..9d94cac 100644
--- a/src/Data/Integer.agda
+++ b/src/Data/Integer.agda
@@ -128,25 +128,7 @@ _+_ : ℤ → ℤ → ℤ
 -- Subtraction.
 
 _-_ : ℤ → ℤ → ℤ
--[1+ m ] - -[1+ n ] = n ⊖ m
--[1+ m ] - +    n   = -[1+ n ℕ+ m ]
-+    m   - -[1+ n ] = + (ℕ.suc n ℕ+ m)
-+    m   - +    n   = m ⊖ n
-
-private
-
-  -- Note that the definition i - j = - j + i evaluates differently
-  -- from the definition above. For instance, the following property
-  -- would require a nontrivial proof with the alternative definition:
-
-  +-+ : ∀ m n → + m - + n ≡ m ⊖ n
-  +-+ m n = refl
-
-  -- The proof is still easy, though.
-
-  -++ : ∀ m n → - + n + + m ≡ m ⊖ n
-  -++ m ℕ.zero    = refl
-  -++ m (ℕ.suc n) = refl
+i - j = i + - j
 
 -- Successor.
 
@@ -164,7 +146,7 @@ private
 -- Predecessor.
 
 pred : ℤ → ℤ
-pred i = i - + 1
+pred i = - + 1 + i
 
 private
 
diff --git a/src/Data/Integer/Addition/Properties.agda b/src/Data/Integer/Addition/Properties.agda
new file mode 100644
index 0000000..d4cd9c3
--- /dev/null
+++ b/src/Data/Integer/Addition/Properties.agda
@@ -0,0 +1,117 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties related to addition of integers
+------------------------------------------------------------------------
+
+module Data.Integer.Addition.Properties where
+
+open import Algebra
+import Algebra.FunctionProperties
+open import Algebra.Structures
+open import Data.Integer hiding (suc)
+open import Data.Nat using (suc; zero) renaming (_+_ to _ℕ+_)
+import Data.Nat.Properties as ℕ
+open import Relation.Binary.PropositionalEquality
+
+open Algebra.FunctionProperties (_≡_ {A = ℤ})
+open CommutativeSemiring ℕ.commutativeSemiring
+  using (+-comm; +-assoc; +-identity)
+
+------------------------------------------------------------------------
+-- Addition and zero form a commutative monoid
+
+private
+
+  comm : Commutative _+_
+  comm -[1+ a ] -[1+ b ] rewrite +-comm a b = refl
+  comm (+   a ) (+   b ) rewrite +-comm a b = refl
+  comm -[1+ _ ] (+   _ ) = refl
+  comm (+   _ ) -[1+ _ ] = refl
+
+  identityˡ : LeftIdentity (+ 0) _+_
+  identityˡ -[1+ _ ] = refl
+  identityˡ (+   _ ) = refl
+
+  identityʳ : RightIdentity (+ 0) _+_
+  identityʳ x rewrite comm x (+ 0) = identityˡ x
+
+  distribˡ-⊖-+-neg : ∀ a b c → b ⊖ c + -[1+ a ] ≡ b ⊖ (suc c ℕ+ a)
+  distribˡ-⊖-+-neg _ zero    zero    = refl
+  distribˡ-⊖-+-neg _ zero    (suc _) = refl
+  distribˡ-⊖-+-neg _ (suc _) zero    = refl
+  distribˡ-⊖-+-neg a (suc b) (suc c) = distribˡ-⊖-+-neg a b c
+
+  distribʳ-⊖-+-neg : ∀ a b c → -[1+ a ] + (b ⊖ c) ≡ b ⊖ (suc a ℕ+ c)
+  distribʳ-⊖-+-neg a b c
+    rewrite comm -[1+ a ] (b ⊖ c)
+          | distribˡ-⊖-+-neg a b c
+          | +-comm a c
+          = refl
+
+  distribˡ-⊖-+-pos : ∀ a b c → b ⊖ c + + a ≡ b ℕ+ a ⊖ c
+  distribˡ-⊖-+-pos _ zero    zero    = refl
+  distribˡ-⊖-+-pos _ zero    (suc _) = refl
+  distribˡ-⊖-+-pos _ (suc _) zero    = refl
+  distribˡ-⊖-+-pos a (suc b) (suc c) = distribˡ-⊖-+-pos a b c
+
+  distribʳ-⊖-+-pos : ∀ a b c → + a + (b ⊖ c) ≡ a ℕ+ b ⊖ c
+  distribʳ-⊖-+-pos a b c
+    rewrite comm (+ a) (b ⊖ c)
+          | distribˡ-⊖-+-pos a b c
+          | +-comm a b
+          = refl
+
+  assoc : Associative _+_
+  assoc (+ zero) y z rewrite identityˡ      y  | identityˡ (y + z) = refl
+  assoc x (+ zero) z rewrite identityʳ  x      | identityˡ      z  = refl
+  assoc x y (+ zero) rewrite identityʳ (x + y) | identityʳ  y      = refl
+  assoc -[1+ a ]  -[1+ b ]  (+ suc c) = sym (distribʳ-⊖-+-neg a c b)
+  assoc -[1+ a ]  (+ suc b) (+ suc c) = distribˡ-⊖-+-pos (suc c) b a
+  assoc (+ suc a) -[1+ b ]  -[1+ c ]  = distribˡ-⊖-+-neg c a b
+  assoc (+ suc a) -[1+ b ] (+ suc c)
+    rewrite distribˡ-⊖-+-pos (suc c) a b
+          | distribʳ-⊖-+-pos (suc a) c b
+          | sym (+-assoc a 1 c)
+          | +-comm a 1
+          = refl
+  assoc (+ suc a) (+ suc b) -[1+ c ]
+    rewrite distribʳ-⊖-+-pos (suc a) b c
+          | sym (+-assoc a 1 b)
+          | +-comm a 1
+          = refl
+  assoc -[1+ a ] -[1+ b ] -[1+ c ]
+    rewrite sym (+-assoc a 1 (b ℕ+ c))
+          | +-comm a 1
+          | +-assoc a b c
+          = refl
+  assoc -[1+ a ] (+ suc b) -[1+ c ]
+    rewrite distribʳ-⊖-+-neg a b c
+          | distribˡ-⊖-+-neg c b a
+          = refl
+  assoc (+ suc a) (+ suc b) (+ suc c)
+    rewrite +-assoc (suc a) (suc b) (suc c)
+          = refl
+
+  isSemigroup : IsSemigroup _≡_ _+_
+  isSemigroup = record
+    { isEquivalence = isEquivalence
+    ; assoc         = assoc
+    ; ∙-cong        = cong₂ _+_
+    }
+
+  isCommutativeMonoid : IsCommutativeMonoid _≡_ _+_ (+ 0)
+  isCommutativeMonoid = record
+    { isSemigroup = isSemigroup
+    ; identityˡ   = identityˡ
+    ; comm        = comm
+    }
+
+commutativeMonoid : CommutativeMonoid _ _
+commutativeMonoid = record
+  { Carrier             = ℤ
+  ; _≈_                 = _≡_
+  ; _∙_                 = _+_
+  ; ε                   = + 0
+  ; isCommutativeMonoid = isCommutativeMonoid
+  }
diff --git a/src/Data/Integer/Multiplication/Properties.agda b/src/Data/Integer/Multiplication/Properties.agda
new file mode 100644
index 0000000..6729c5e
--- /dev/null
+++ b/src/Data/Integer/Multiplication/Properties.agda
@@ -0,0 +1,91 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties related to multiplication of integers
+------------------------------------------------------------------------
+
+module Data.Integer.Multiplication.Properties where
+
+open import Algebra
+  using (module CommutativeSemiring; CommutativeMonoid)
+import Algebra.FunctionProperties
+open import Algebra.Structures using (IsSemigroup; IsCommutativeMonoid)
+open import Data.Integer
+   using (ℤ; -[1+_]; +_; ∣_∣; sign; _◃_) renaming (_*_ to ℤ*)
+open import Data.Nat
+  using (suc; zero) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
+open import Data.Product using (proj₂)
+import Data.Nat.Properties as ℕ
+open import Data.Sign using () renaming (_*_ to _S*_)
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality
+   using (_≡_; refl; cong; cong₂; isEquivalence)
+
+open Algebra.FunctionProperties (_≡_ {A = ℤ})
+open CommutativeSemiring ℕ.commutativeSemiring
+  using (+-identity; *-comm) renaming (zero to *-zero)
+
+------------------------------------------------------------------------
+-- Multiplication and one form a commutative monoid
+
+private
+
+  identityˡ : LeftIdentity (+ 1) ℤ*
+  identityˡ (+ zero ) = refl
+  identityˡ -[1+  n ] rewrite proj₂ +-identity n = refl
+  identityˡ (+ suc n) rewrite proj₂ +-identity n = refl
+
+  comm : Commutative ℤ*
+  comm -[1+ a ] -[1+ b ] rewrite *-comm (suc a) (suc b) = refl
+  comm -[1+ a ] (+   b ) rewrite *-comm (suc a) b       = refl
+  comm (+   a ) -[1+ b ] rewrite *-comm a       (suc b) = refl
+  comm (+   a ) (+   b ) rewrite *-comm a       b       = refl
+
+  lemma : ∀ a b c → c ℕ+ (b ℕ+ a ℕ* suc b) ℕ* suc c
+                  ≡ c ℕ+ b ℕ* suc c ℕ+ a ℕ* suc (c ℕ+ b ℕ* suc c)
+  lemma =
+    solve 3 (λ a b c → c :+ (b :+ a :* (con 1 :+ b)) :* (con 1 :+ c)
+                    := c :+ b :* (con 1 :+ c) :+
+                       a :* (con 1 :+ (c :+ b :* (con 1 :+ c))))
+            refl
+    where open ℕ.SemiringSolver
+
+  assoc : Associative ℤ*
+  assoc (+ zero) _ _ = refl
+  assoc x (+ zero) _ rewrite proj₂ *-zero ∣ x ∣ = refl
+  assoc x y (+ zero) rewrite
+      proj₂ *-zero ∣ y ∣
+    | proj₂ *-zero ∣ x ∣
+    | proj₂ *-zero ∣ sign x S* sign y ◃ ∣ x ∣ ℕ* ∣ y ∣ ∣
+    = refl
+  assoc -[1+ a  ] -[1+ b  ] (+ suc c) = cong (+_ ∘ suc) (lemma a b c)
+  assoc -[1+ a  ] (+ suc b) -[1+ c  ] = cong (+_ ∘ suc) (lemma a b c)
+  assoc (+ suc a) (+ suc b) (+ suc c) = cong (+_ ∘ suc) (lemma a b c)
+  assoc (+ suc a) -[1+ b  ] -[1+ c  ] = cong (+_ ∘ suc) (lemma a b c)
+  assoc -[1+ a  ] -[1+ b  ] -[1+ c  ] = cong -[1+_]     (lemma a b c)
+  assoc -[1+ a  ] (+ suc b) (+ suc c) = cong -[1+_]     (lemma a b c)
+  assoc (+ suc a) -[1+ b  ] (+ suc c) = cong -[1+_]     (lemma a b c)
+  assoc (+ suc a) (+ suc b) -[1+ c  ] = cong -[1+_]     (lemma a b c)
+
+  isSemigroup : IsSemigroup _ _
+  isSemigroup = record
+    { isEquivalence = isEquivalence
+    ; assoc         = assoc
+    ; ∙-cong        = cong₂ ℤ*
+    }
+
+  isCommutativeMonoid : IsCommutativeMonoid _≡_ ℤ* (+ 1)
+  isCommutativeMonoid = record
+    { isSemigroup = isSemigroup
+    ; identityˡ   = identityˡ
+    ; comm        = comm
+    }
+
+commutativeMonoid : CommutativeMonoid _ _
+commutativeMonoid = record
+  { Carrier             = ℤ
+  ; _≈_                 = _≡_
+  ; _∙_                 = ℤ*
+  ; ε                   = + 1
+  ; isCommutativeMonoid = isCommutativeMonoid
+  }
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 076dad1..654ecc6 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -7,18 +7,49 @@
 module Data.Integer.Properties where
 
 open import Algebra
+import Algebra.FunctionProperties
 import Algebra.Morphism as Morphism
-open import Data.Empty
-open import Function
-open import Data.Integer hiding (suc)
-open import Data.Nat as ℕ renaming (_*_ to _ℕ*_)
-import Data.Nat.Properties as ℕ
+import Algebra.Props.AbelianGroup
+open import Algebra.Structures
+open import Data.Integer hiding (suc; _≤?_)
+import Data.Integer.Addition.Properties as Add
+import Data.Integer.Multiplication.Properties as Mul
+open import Data.Nat
+  using (ℕ; suc; zero; _∸_; _≤?_; _<_; _≥_; _≱_; s≤s; z≤n)
+  renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
+open import Data.Nat.Properties as ℕ using (_*-mono_)
+open import Data.Product using (proj₁; proj₂; _,_)
 open import Data.Sign as Sign using () renaming (_*_ to _S*_)
 import Data.Sign.Properties as SignProp
+open import Function using (_∘_; _$_)
+open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
-open ≡-Reasoning
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Negation using (contradiction)
 
+open Algebra.FunctionProperties (_≡_ {A = ℤ})
+open CommutativeMonoid Add.commutativeMonoid
+  using ()
+  renaming ( assoc to +-assoc; comm to +-comm; identity to +-identity
+           ; isCommutativeMonoid to +-isCommutativeMonoid
+           ; isMonoid to +-isMonoid
+           )
+open CommutativeMonoid Mul.commutativeMonoid
+  using ()
+  renaming ( assoc to *-assoc; comm to *-comm; identity to *-identity
+           ; isCommutativeMonoid to *-isCommutativeMonoid
+           ; isMonoid to *-isMonoid
+           )
+open CommutativeSemiring ℕ.commutativeSemiring
+  using () renaming (zero to *-zero; distrib to *-distrib)
+open DecTotalOrder Data.Nat.decTotalOrder
+  using () renaming (refl to ≤-refl)
 open Morphism.Definitions ℤ ℕ _≡_
+open ℕ.SemiringSolver
+open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- Miscellaneous properties
 
 -- Some properties relating sign and ∣_∣ to _◃_.
 
@@ -52,12 +83,247 @@ abs-cong {s₁} {s₂} {n₁} {n₂} eq = begin
 abs-*-commute : Homomorphic₂ ∣_∣ _*_ _ℕ*_
 abs-*-commute i j = abs-◃ _ _
 
+-- If you subtract a natural from itself, then you get zero.
+
+n⊖n≡0 : ∀ n → n ⊖ n ≡ + 0
+n⊖n≡0 zero    = refl
+n⊖n≡0 (suc n) = n⊖n≡0 n
+
+------------------------------------------------------------------------
+-- The integers form a commutative ring
+
+private
+
+  ----------------------------------------------------------------------
+  -- Additive abelian group.
+
+  inverseˡ : LeftInverse (+ 0) -_ _+_
+  inverseˡ -[1+ n ]  = n⊖n≡0 n
+  inverseˡ (+ zero)  = refl
+  inverseˡ (+ suc n) = n⊖n≡0 n
+
+  inverseʳ : RightInverse (+ 0) -_ _+_
+  inverseʳ i = begin
+    i + - i  ≡⟨ +-comm i (- i) ⟩
+    - i + i  ≡⟨ inverseˡ i ⟩
+    + 0      ∎
+
+  +-isAbelianGroup : IsAbelianGroup _≡_ _+_ (+ 0) -_
+  +-isAbelianGroup = record
+    { isGroup = record
+      { isMonoid = +-isMonoid
+      ; inverse  = inverseˡ , inverseʳ
+      ; ⁻¹-cong  = cong -_
+      }
+    ; comm = +-comm
+    }
+
+  open Algebra.Props.AbelianGroup
+         (record { isAbelianGroup = +-isAbelianGroup })
+    using () renaming (⁻¹-involutive to -‿involutive)
+
+  ----------------------------------------------------------------------
+  -- Distributivity
+
+  -- Various lemmas used to prove distributivity.
+
+  sign-⊖-< : ∀ {m n} → m < n → sign (m ⊖ n) ≡ Sign.-
+  sign-⊖-< {zero}  (s≤s z≤n) = refl
+  sign-⊖-< {suc n} (s≤s m<n) = sign-⊖-< m<n
+
+  sign-⊖-≱ : ∀ {m n} → m ≱ n → sign (m ⊖ n) ≡ Sign.-
+  sign-⊖-≱ = sign-⊖-< ∘ ℕ.≰⇒>
+
+  +-⊖-left-cancel : ∀ a b c → (a ℕ+ b) ⊖ (a ℕ+ c) ≡ b ⊖ c
+  +-⊖-left-cancel zero    b c = refl
+  +-⊖-left-cancel (suc a) b c = +-⊖-left-cancel a b c
+
+  ⊖-swap : ∀ a b → a ⊖ b ≡ - (b ⊖ a)
+  ⊖-swap zero    zero    = refl
+  ⊖-swap (suc _) zero    = refl
+  ⊖-swap zero    (suc _) = refl
+  ⊖-swap (suc a) (suc b) = ⊖-swap a b
+
+  -- Lemmas relating _⊖_ and _∸_.
+
+  ∣⊖∣-< : ∀ {m n} → m < n → ∣ m ⊖ n ∣ ≡ n ∸ m
+  ∣⊖∣-< {zero}  (s≤s z≤n) = refl
+  ∣⊖∣-< {suc n} (s≤s m<n) = ∣⊖∣-< m<n
+
+  ∣⊖∣-≱ : ∀ {m n} → m ≱ n → ∣ m ⊖ n ∣ ≡ n ∸ m
+  ∣⊖∣-≱ = ∣⊖∣-< ∘ ℕ.≰⇒>
+
+  ⊖-≥ : ∀ {m n} → m ≥ n → m ⊖ n ≡ + (m ∸ n)
+  ⊖-≥ z≤n       = refl
+  ⊖-≥ (s≤s n≤m) = ⊖-≥ n≤m
+
+  ⊖-< : ∀ {m n} → m < n → m ⊖ n ≡ - + (n ∸ m)
+  ⊖-< {zero}  (s≤s z≤n) = refl
+  ⊖-< {suc m} (s≤s m<n) = ⊖-< m<n
+
+  ⊖-≱ : ∀ {m n} → m ≱ n → m ⊖ n ≡ - + (n ∸ m)
+  ⊖-≱ = ⊖-< ∘ ℕ.≰⇒>
+
+  -- Lemmas working around the fact that _◃_ pattern matches on its
+  -- second argument before its first.
+
+  +‿◃ : ∀ n → Sign.+ ◃ n ≡ + n
+  +‿◃ zero    = refl
+  +‿◃ (suc _) = refl
+
+  -‿◃ : ∀ n → Sign.- ◃ n ≡ - + n
+  -‿◃ zero    = refl
+  -‿◃ (suc _) = refl
+
+  -- The main distributivity proof.
+
+  distrib-lemma :
+    ∀ a b c → (c ⊖ b) * -[1+ a ] ≡ a ℕ+ b ℕ* suc a ⊖ (a ℕ+ c ℕ* suc a)
+  distrib-lemma a b c
+    rewrite +-⊖-left-cancel a (b ℕ* suc a) (c ℕ* suc a)
+          | ⊖-swap (b ℕ* suc a) (c ℕ* suc a)
+    with b ≤? c
+  ... | yes b≤c
+    rewrite ⊖-≥ b≤c
+          | ⊖-≥ (b≤c *-mono (≤-refl {x = suc a}))
+          | -‿◃ ((c ∸ b) ℕ* suc a)
+          | ℕ.*-distrib-∸ʳ (suc a) c b
+          = refl
+  ... | no b≰c
+    rewrite sign-⊖-≱ b≰c
+          | ∣⊖∣-≱ b≰c
+          | +‿◃ ((b ∸ c) ℕ* suc a)
+          | ⊖-≱ (b≰c ∘ ℕ.cancel-*-right-≤ b c a)
+          | -‿involutive (+ (b ℕ* suc a ∸ c ℕ* suc a))
+          | ℕ.*-distrib-∸ʳ (suc a) b c
+          = refl
+
+  distribʳ : _*_ DistributesOverʳ _+_
+
+  distribʳ (+ zero) y z
+    rewrite proj₂ *-zero ∣ y ∣
+          | proj₂ *-zero ∣ z ∣
+          | proj₂ *-zero ∣ y + z ∣
+          = refl
+
+  distribʳ x (+ zero) z
+    rewrite proj₁ +-identity z
+          | proj₁ +-identity (sign z S* sign x ◃ ∣ z ∣ ℕ* ∣ x ∣)
+          = refl
+
+  distribʳ x y (+ zero)
+    rewrite proj₂ +-identity y
+          | proj₂ +-identity (sign y S* sign x ◃ ∣ y ∣ ℕ* ∣ x ∣)
+          = refl
+
+  distribʳ -[1+ a ] -[1+ b ] -[1+ c ] = cong +_ $
+    solve 3 (λ a b c → (con 2 :+ b :+ c) :* (con 1 :+ a)
+                    := (con 1 :+ b) :* (con 1 :+ a) :+
+                       (con 1 :+ c) :* (con 1 :+ a))
+            refl a b c
+
+  distribʳ (+ suc a) (+ suc b) (+ suc c) = cong +_ $
+    solve 3 (λ a b c → (con 1 :+ b :+ (con 1 :+ c)) :* (con 1 :+ a)
+                    := (con 1 :+ b) :* (con 1 :+ a) :+
+                       (con 1 :+ c) :* (con 1 :+ a))
+          refl a b c
+
+  distribʳ -[1+ a ] (+ suc b) (+ suc c) = cong -[1+_] $
+    solve 3 (λ a b c → a :+ (b :+ (con 1 :+ c)) :* (con 1 :+ a)
+                     := (con 1 :+ b) :* (con 1 :+ a) :+
+                        (a :+ c :* (con 1 :+ a)))
+           refl a b c
+
+  distribʳ (+ suc a) -[1+ b ] -[1+ c ] = cong -[1+_] $
+    solve 3 (λ a b c → a :+ (con 1 :+ a :+ (b :+ c) :* (con 1 :+ a))
+                    := (con 1 :+ b) :* (con 1 :+ a) :+
+                       (a :+ c :* (con 1 :+ a)))
+           refl a b c
+
+  distribʳ -[1+ a ] -[1+ b ] (+ suc c) = distrib-lemma a b c
+
+  distribʳ -[1+ a ] (+ suc b) -[1+ c ] = distrib-lemma a c b
+
+  distribʳ (+ suc a) -[1+ b ] (+ suc c)
+    rewrite +-⊖-left-cancel a (c ℕ* suc a) (b ℕ* suc a)
+    with b ≤? c
+  ... | yes b≤c
+    rewrite ⊖-≥ b≤c
+          | +-comm (- (+ (a ℕ+ b ℕ* suc a))) (+ (a ℕ+ c ℕ* suc a))
+          | ⊖-≥ (b≤c *-mono ≤-refl {x = suc a})
+          | ℕ.*-distrib-∸ʳ (suc a) c b
+          | +‿◃ (c ℕ* suc a ∸ b ℕ* suc a)
+          = refl
+  ... | no b≰c
+    rewrite sign-⊖-≱ b≰c
+          | ∣⊖∣-≱ b≰c
+          | -‿◃ ((b ∸ c) ℕ* suc a)
+          | ⊖-≱ (b≰c ∘ ℕ.cancel-*-right-≤ b c a)
+          | ℕ.*-distrib-∸ʳ (suc a) b c
+          = refl
+
+  distribʳ (+ suc c) (+ suc a) -[1+ b ]
+    rewrite +-⊖-left-cancel c (a ℕ* suc c) (b ℕ* suc c)
+    with b ≤? a
+  ... | yes b≤a
+    rewrite ⊖-≥ b≤a
+          | ⊖-≥ (b≤a *-mono ≤-refl {x = suc c})
+          | +‿◃ ((a ∸ b) ℕ* suc c)
+          | ℕ.*-distrib-∸ʳ (suc c) a b
+          = refl
+  ... | no b≰a
+    rewrite sign-⊖-≱ b≰a
+          | ∣⊖∣-≱ b≰a
+          | ⊖-≱ (b≰a ∘ ℕ.cancel-*-right-≤ b a c)
+          | -‿◃ ((b ∸ a) ℕ* suc c)
+          | ℕ.*-distrib-∸ʳ (suc c) b a
+          = refl
+
+  -- The IsCommutativeSemiring module contains a proof of
+  -- distributivity which is used below.
+
+  isCommutativeSemiring : IsCommutativeSemiring _≡_ _+_ _*_ (+ 0) (+ 1)
+  isCommutativeSemiring = record
+    { +-isCommutativeMonoid = +-isCommutativeMonoid
+    ; *-isCommutativeMonoid = *-isCommutativeMonoid
+    ; distribʳ              = distribʳ
+    ; zeroˡ                 = λ _ → refl
+    }
+
+commutativeRing : CommutativeRing _ _
+commutativeRing = record
+  { Carrier           = ℤ
+  ; _≈_               = _≡_
+  ; _+_               = _+_
+  ; _*_               = _*_
+  ; -_                = -_
+  ; 0#                = + 0
+  ; 1#                = + 1
+  ; isCommutativeRing = record
+    { isRing = record
+      { +-isAbelianGroup = +-isAbelianGroup
+      ; *-isMonoid       = *-isMonoid
+      ; distrib          = IsCommutativeSemiring.distrib
+                             isCommutativeSemiring
+      }
+    ; *-comm = *-comm
+    }
+  }
+
+import Algebra.RingSolver.Simple as Solver
+import Algebra.RingSolver.AlmostCommutativeRing as ACR
+module RingSolver =
+  Solver (ACR.fromCommutativeRing commutativeRing)
+
+------------------------------------------------------------------------
+-- More properties
+
 -- Multiplication is right cancellative for non-zero integers.
 
 cancel-*-right : ∀ i j k →
                  k ≢ + 0 → i * k ≡ j * k → i ≡ j
 cancel-*-right i j k            ≢0 eq with signAbs k
-cancel-*-right i j .(+ 0)       ≢0 eq | s ◂ zero  = ⊥-elim (≢0 refl)
+cancel-*-right i j .(+ 0)       ≢0 eq | s ◂ zero  = contradiction refl ≢0
 cancel-*-right i j .(s ◃ suc n) ≢0 eq | s ◂ suc n
   with ∣ s ◃ suc n ∣ | abs-◃ s (suc n) | sign (s ◃ suc n) | sign-◃ s n
 ...  | .(suc n)      | refl            | .s               | refl =
diff --git a/src/Data/List/All.agda b/src/Data/List/All.agda
index bc4debf..4ac8448 100644
--- a/src/Data/List/All.agda
+++ b/src/Data/List/All.agda
@@ -13,7 +13,7 @@ open import Function
 open import Level
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
-open import Relation.Unary using () renaming (_⊆_ to _⋐_)
+open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_)
 open import Relation.Binary.PropositionalEquality
 
 -- All P xs means that all elements in xs satisfy P.
@@ -50,7 +50,7 @@ map g []         = []
 map g (px ∷ pxs) = g px ∷ map g pxs
 
 all : ∀ {a p} {A : Set a} {P : A → Set p} →
-      (∀ x → Dec (P x)) → (xs : List A) → Dec (All P xs)
+      Decidable P → Decidable (All P)
 all p []       = yes []
 all p (x ∷ xs) with p x
 all p (x ∷ xs) | yes px = Dec.map′ (_∷_ px) tail (all p xs)
diff --git a/src/Data/List/All/Properties.agda b/src/Data/List/All/Properties.agda
index 6837a46..03e08ba 100644
--- a/src/Data/List/All/Properties.agda
+++ b/src/Data/List/All/Properties.agda
@@ -8,14 +8,15 @@ module Data.List.All.Properties where
 
 open import Data.Bool
 open import Data.Bool.Properties
+open import Data.List as List
+import Data.List.Any as Any; open Any.Membership-≡
+open import Data.List.All as All using (All; []; _∷_)
+open import Data.Product as Prod
 open import Function
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence using (module Equivalence)
-open import Data.List as List
-import Data.List.Any as Any
-open Any.Membership-≡
-open import Data.List.All as All using (All; []; _∷_)
-open import Data.Product
+open import Function.Inverse using (_↔_)
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Unary using () renaming (_⊆_ to _⋐_)
 
 -- Functions can be shifted between the predicate and the list.
@@ -64,3 +65,38 @@ anti-mono xs⊆ys pys = All.tabulate (All.lookup pys ∘ xs⊆ys)
 all-anti-mono : ∀ {a} {A : Set a} (p : A → Bool) {xs ys} →
                 xs ⊆ ys → T (all p ys) → T (all p xs)
 all-anti-mono p xs⊆ys = All-all p ∘ anti-mono xs⊆ys ∘ all-All p _
+
+-- All P (xs ++ ys) is isomorphic to All P xs and All P ys.
+
+private
+
+  ++⁺ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys : List A} →
+        All P xs → All P ys → All P (xs ++ ys)
+  ++⁺ []         pys = pys
+  ++⁺ (px ∷ pxs) pys = px ∷ ++⁺ pxs pys
+
+  ++⁻ : ∀ {a p} {A : Set a} {P : A → Set p} (xs : List A) {ys} →
+        All P (xs ++ ys) → All P xs × All P ys
+  ++⁻ []       p          = [] , p
+  ++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map (_∷_ px) id $ ++⁻ _ pxs
+
+  ++⁺∘++⁻ : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys}
+            (p : All P (xs ++ ys)) → uncurry′ ++⁺ (++⁻ xs p) ≡ p
+  ++⁺∘++⁻ []       p          = P.refl
+  ++⁺∘++⁻ (x ∷ xs) (px ∷ pxs) = P.cong (_∷_ px) $ ++⁺∘++⁻ xs pxs
+
+  ++⁻∘++⁺ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys}
+            (p : All P xs × All P ys) → ++⁻ xs (uncurry ++⁺ p) ≡ p
+  ++⁻∘++⁺ ([]       , pys) = P.refl
+  ++⁻∘++⁺ (px ∷ pxs , pys) rewrite ++⁻∘++⁺ (pxs , pys) = P.refl
+
+++↔ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} →
+      (All P xs × All P ys) ↔ All P (xs ++ ys)
+++↔ {P = P} {xs = xs} = record
+  { to         = P.→-to-⟶ $ uncurry ++⁺
+  ; from       = P.→-to-⟶ $ ++⁻ xs
+  ; inverse-of = record
+    { left-inverse-of  = ++⁻∘++⁺
+    ; right-inverse-of = ++⁺∘++⁻ xs
+    }
+  }
diff --git a/src/Data/List/Any.agda b/src/Data/List/Any.agda
index 7a19b17..89a0255 100644
--- a/src/Data/List/Any.agda
+++ b/src/Data/List/Any.agda
@@ -17,8 +17,8 @@ open import Data.Product as Prod using (∃; _×_; _,_)
 open import Level using (Level; _⊔_)
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
-open import Relation.Unary using () renaming (_⊆_ to _⋐_)
-open import Relation.Binary
+open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_)
+open import Relation.Binary hiding (Decidable)
 import Relation.Binary.InducedPreorders as Ind
 open import Relation.Binary.List.Pointwise as ListEq using ([]; _∷_)
 open import Relation.Binary.PropositionalEquality as PropEq
@@ -48,7 +48,7 @@ tail ¬px (there pxs) = pxs
 -- Decides Any.
 
 any : ∀ {a p} {A : Set a} {P : A → Set p} →
-      (∀ x → Dec (P x)) → (xs : List A) → Dec (Any P xs)
+      Decidable P → Decidable (Any P)
 any p []       = no λ()
 any p (x ∷ xs) with p x
 any p (x ∷ xs) | yes px = yes (here px)
diff --git a/src/Data/List/Any/Membership.agda b/src/Data/List/Any/Membership.agda
index 2cc230e..321dd53 100644
--- a/src/Data/List/Any/Membership.agda
+++ b/src/Data/List/Any/Membership.agda
@@ -46,6 +46,8 @@ private
 ------------------------------------------------------------------------
 -- Properties relating _∈_ to various list functions
 
+-- Isomorphisms.
+
 map-∈↔ : ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y xs} →
          (∃ λ x → x ∈ xs × y ≡ f x) ↔ y ∈ List.map f xs
 map-∈↔ {a} {b} {f = f} {y} {xs} =
@@ -102,8 +104,20 @@ concat-∈↔ {a} {x = x} {xss} =
       }
     }
 
+-- Other properties.
+
+filter-∈ : ∀ {a} {A : Set a} (p : A → Bool) (xs : List A) {x} →
+           x ∈ xs → p x ≡ true → x ∈ filter p xs
+filter-∈ p []       ()          _
+filter-∈ p (x ∷ xs) (here refl) px≡true rewrite px≡true = here refl
+filter-∈ p (y ∷ xs) (there pxs) px≡true with p y
+... | true  = there (filter-∈ p xs pxs px≡true)
+... | false =        filter-∈ p xs pxs px≡true
+
 ------------------------------------------------------------------------
--- Various functions are monotone
+-- Properties relating _∈_ to various list functions
+
+-- Various functions are monotone.
 
 mono : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} →
        xs ⊆ ys → Any P xs → Any P ys
@@ -178,6 +192,18 @@ map-with-∈-mono {f = f} {g = g} xs⊆ys f≈g {x} =
   _⟨$⟩_ (Inverse.from map-with-∈↔)
   where open P.≡-Reasoning
 
+-- Other properties.
+
+filter-⊆ : ∀ {a} {A : Set a} (p : A → Bool) →
+           (xs : List A) → filter p xs ⊆ xs
+filter-⊆ _ []       = λ ()
+filter-⊆ p (x ∷ xs) with p x | filter-⊆ p xs
+... | false | hyp = there ∘ hyp
+... | true  | hyp =
+  λ { (here  eq)      → here eq
+    ; (there ∈filter) → there (hyp ∈filter)
+    }
+
 ------------------------------------------------------------------------
 -- Other properties
 
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 8b7c72c..ae065b3 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -11,16 +11,20 @@ module Data.List.Properties where
 
 open import Algebra
 open import Category.Monad
+open import Data.Bool
 open import Data.List as List
+open import Data.List.All using (All; []; _∷_)
+open import Data.Maybe using (Maybe; just; nothing)
 open import Data.Nat
 open import Data.Nat.Properties
-open import Data.Bool
-open import Function
 open import Data.Product as Prod hiding (map)
-open import Data.Maybe
+open import Function
+import Relation.Binary.EqReasoning as EqR
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; _≗_; refl)
-import Relation.Binary.EqReasoning as EqR
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (⌊_⌋)
+open import Relation.Unary using (Decidable)
 
 private
   open module LMP {ℓ} = RawMonadPlus (List.monadPlus {ℓ = ℓ})
@@ -235,7 +239,7 @@ span-defn p (x ∷ xs) with p x
 ... | true  = P.cong (Prod.map (_∷_ x) id) (span-defn p xs)
 ... | false = refl
 
--- Partition.
+-- Partition, filter.
 
 partition-defn : ∀ {a} {A : Set a} (p : A → Bool) →
                  partition p ≗ < filter p , filter (not ∘ p) >
@@ -245,6 +249,14 @@ partition-defn p (x ∷ xs)
 ...  | true  | (ys , zs) | eq = P.cong (Prod.map (_∷_ x) id) eq
 ...  | false | (ys , zs) | eq = P.cong (Prod.map id (_∷_ x)) eq
 
+filter-filters : ∀ {a p} {A : Set a} →
+                 (P : A → Set p) (dec : Decidable P) (xs : List A) →
+                 All P (filter (⌊_⌋ ∘ dec) xs)
+filter-filters P dec []       = []
+filter-filters P dec (x ∷ xs) with dec x
+filter-filters P dec (x ∷ xs) | yes px = px ∷ filter-filters P dec xs
+filter-filters P dec (x ∷ xs) | no ¬px = filter-filters P dec xs
+
 -- Inits, tails, and scanr.
 
 scanr-defn : ∀ {a b} {A : Set a} {B : Set b}
diff --git a/src/Data/Maybe.agda b/src/Data/Maybe.agda
index 4d590f3..858c601 100644
--- a/src/Data/Maybe.agda
+++ b/src/Data/Maybe.agda
@@ -94,7 +94,7 @@ monadPlus {f} = record
 -- Equality
 
 open import Relation.Nullary
-open import Relation.Binary
+open import Relation.Binary as B
 
 data Eq {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) : Rel (Maybe A) (a ⊔ ℓ) where
   just    : ∀ {x y} (x≈y : x ≈ y) → Eq _≈_ (just x) (just y)
@@ -138,7 +138,7 @@ decSetoid D = record
     }
   }
   where
-  _≟_ : Decidable (Eq (DecSetoid._≈_ D))
+  _≟_ : B.Decidable (Eq (DecSetoid._≈_ D))
   just x  ≟ just y  with DecSetoid._≟_ D x y
   just x  ≟ just y  | yes x≈y = yes (just x≈y)
   just x  ≟ just y  | no  x≉y = no (x≉y ∘ drop-just)
@@ -151,6 +151,7 @@ decSetoid D = record
 
 open import Data.Empty using (⊥)
 import Relation.Nullary.Decidable as Dec
+open import Relation.Unary as U
 
 data Any {a} {A : Set a} (P : A → Set a) : Maybe A → Set a where
   just : ∀ {x} (px : P x) → Any P (just x)
@@ -173,12 +174,10 @@ private
   drop-just-All : ∀ {A} {P : A → Set} {x} → All P (just x) → P x
   drop-just-All (just px) = px
 
-anyDec : ∀ {A} {P : A → Set} →
-         (∀ x → Dec (P x)) → (x : Maybe A) → Dec (Any P x)
+anyDec : ∀ {A} {P : A → Set} → U.Decidable P → U.Decidable (Any P)
 anyDec p nothing  = no λ()
 anyDec p (just x) = Dec.map′ just drop-just-Any (p x)
 
-allDec : ∀ {A} {P : A → Set} →
-         (∀ x → Dec (P x)) → (x : Maybe A) → Dec (All P x)
+allDec : ∀ {A} {P : A → Set} → U.Decidable P → U.Decidable (All P)
 allDec p nothing  = yes nothing
 allDec p (just x) = Dec.map′ just drop-just-All (p x)
diff --git a/src/Data/Nat.agda b/src/Data/Nat.agda
index 95eed21..5029913 100644
--- a/src/Data/Nat.agda
+++ b/src/Data/Nat.agda
@@ -32,7 +32,7 @@ data ℕ : Set where
 {-# BUILTIN ZERO    zero #-}
 {-# BUILTIN SUC     suc  #-}
 
-infix 4 _≤_ _<_ _≥_ _>_
+infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_
 
 data _≤_ : Rel ℕ Level.zero where
   z≤n : ∀ {n}                 → zero  ≤ n
@@ -47,6 +47,18 @@ m ≥ n = n ≤ m
 _>_ : Rel ℕ Level.zero
 m > n = n < m
 
+_≰_ : Rel ℕ Level.zero
+a ≰ b = ¬ a ≤ b
+
+_≮_ : Rel ℕ Level.zero
+a ≮ b = ¬ a < b
+
+_≱_ : Rel ℕ Level.zero
+a ≱ b = ¬ a ≥ b
+
+_≯_ : Rel ℕ Level.zero
+a ≯ b = ¬ a > b
+
 -- The following, alternative definition of _≤_ is more suitable for
 -- well-founded induction (see Induction.Nat).
 
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index 3ea1faf..b632f9e 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -14,6 +14,7 @@ open import Data.Nat.Divisibility
 open import Relation.Nullary
 open import Relation.Nullary.Decidable
 open import Relation.Nullary.Negation
+open import Relation.Unary
 
 -- Definition of primality.
 
@@ -24,7 +25,7 @@ Prime (suc (suc n)) = (i : Fin n) → ¬ (2 + Fin.toℕ i ∣ 2 + n)
 
 -- Decision procedure for primality.
 
-prime? : ∀ n → Dec (Prime n)
+prime? : Decidable Prime
 prime? 0             = no λ()
 prime? 1             = no λ()
 prime? (suc (suc n)) = all? λ _ → ¬? (_ ∣? _)
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 4682ca0..2fac22f 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -429,6 +429,12 @@ m≤m⊔n (suc m) (suc n) = s≤s $ m≤m⊔n m n
   1 + j  ≤⟨ j<k ⟩
   k      □
 
+≰⇒> : _≰_ ⇒ _>_
+≰⇒> {zero}          z≰n with z≰n z≤n
+... | ()
+≰⇒> {suc m} {zero}  _   = s≤s z≤n
+≰⇒> {suc m} {suc n} m≰n = s≤s (≰⇒> (m≰n ∘ s≤s))
+
 ------------------------------------------------------------------------
 -- (ℕ, _≡_, _<_) is a strict total order
 
@@ -494,6 +500,10 @@ m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n
 [m∸n]⊓[n∸m]≡0 (suc m) zero    = refl
 [m∸n]⊓[n∸m]≡0 (suc m) (suc n) = [m∸n]⊓[n∸m]≡0 m n
 
+[i+j]∸[i+k]≡j∸k : ∀ i j k → (i + j) ∸ (i + k) ≡ j ∸ k
+[i+j]∸[i+k]≡j∸k zero    j k = refl
+[i+j]∸[i+k]≡j∸k (suc i) j k = [i+j]∸[i+k]≡j∸k i j k
+
 -- TODO: Can this proof be simplified? An automatic solver which can
 -- handle ∸ would be nice...
 
@@ -566,6 +576,10 @@ cancel-+-left : ∀ i {j k} → i + j ≡ i + k → j ≡ k
 cancel-+-left zero    eq = eq
 cancel-+-left (suc i) eq = cancel-+-left i (cong pred eq)
 
+cancel-+-left-≤ : ∀ i {j k} → i + j ≤ i + k → j ≤ k
+cancel-+-left-≤ zero    le       = le
+cancel-+-left-≤ (suc i) (s≤s le) = cancel-+-left-≤ i le
+
 cancel-*-right : ∀ i j {k} → i * suc k ≡ j * suc k → i ≡ j
 cancel-*-right zero    zero        eq = refl
 cancel-*-right zero    (suc j)     ()
@@ -573,22 +587,32 @@ cancel-*-right (suc i) zero        ()
 cancel-*-right (suc i) (suc j) {k} eq =
   cong suc (cancel-*-right i j (cancel-+-left (suc k) eq))
 
+cancel-*-right-≤ : ∀ i j k → i * suc k ≤ j * suc k → i ≤ j
+cancel-*-right-≤ zero    _       _ _  = z≤n
+cancel-*-right-≤ (suc i) zero    _ ()
+cancel-*-right-≤ (suc i) (suc j) k le =
+  s≤s (cancel-*-right-≤ i j k (cancel-+-left-≤ (suc k) le))
+
+*-distrib-∸ʳ : _*_ DistributesOverʳ _∸_
+*-distrib-∸ʳ i zero k = begin
+  (0 ∸ k) * i  ≡⟨ cong₂ _*_ (0∸n≡0 k) refl ⟩
+  0            ≡⟨ sym $ 0∸n≡0 (k * i) ⟩
+  0 ∸ k * i    ∎
+*-distrib-∸ʳ i (suc j) zero    = begin i + j * i ∎
+*-distrib-∸ʳ i (suc j) (suc k) = begin
+  (j ∸ k) * i             ≡⟨ *-distrib-∸ʳ i j k ⟩
+  j * i ∸ k * i           ≡⟨ sym $ [i+j]∸[i+k]≡j∸k i _ _ ⟩
+  i + j * i ∸ (i + k * i) ∎
+
 im≡jm+n⇒[i∸j]m≡n
   : ∀ i j m n →
     i * m ≡ j * m + n → (i ∸ j) * m ≡ n
-im≡jm+n⇒[i∸j]m≡n i       zero    m n eq = eq
-im≡jm+n⇒[i∸j]m≡n zero    (suc j) m n eq =
-  sym $ i+j≡0⇒j≡0 (m + j * m) $ sym eq
-im≡jm+n⇒[i∸j]m≡n (suc i) (suc j) m n eq =
-  im≡jm+n⇒[i∸j]m≡n i j m n (cancel-+-left m eq')
-  where
-  eq' = begin
-    m + i * m
-      ≡⟨ eq ⟩
-    m + j * m + n
-      ≡⟨ +-assoc m (j * m) n ⟩
-    m + (j * m + n)
-      ∎
+im≡jm+n⇒[i∸j]m≡n i j m n eq = begin
+  (i ∸ j) * m            ≡⟨ *-distrib-∸ʳ m i j ⟩
+  (i * m) ∸ (j * m)      ≡⟨ cong₂ _∸_ eq (refl {x = j * m}) ⟩
+  (j * m + n) ∸ (j * m)  ≡⟨ cong₂ _∸_ (+-comm (j * m) n) (refl {x = j * m}) ⟩
+  (n + j * m) ∸ (j * m)  ≡⟨ m+n∸n≡m n (j * m) ⟩
+  n                      ∎
 
 i+1+j≢i : ∀ i {j} → i + suc j ≢ i
 i+1+j≢i i eq = ¬i+1+j≤i i (reflexive eq)
diff --git a/src/Data/String.agda b/src/Data/String.agda
index acf9696..f98df01 100644
--- a/src/Data/String.agda
+++ b/src/Data/String.agda
@@ -9,11 +9,13 @@ module Data.String where
 open import Data.List as List using (_∷_; []; List)
 open import Data.Vec as Vec using (Vec)
 open import Data.Colist as Colist using (Colist)
-open import Data.Char using (Char)
+open import Data.Char as Char using (Char)
 open import Data.Bool using (Bool; true; false)
 open import Function
 open import Relation.Nullary
 open import Relation.Binary
+open import Relation.Binary.List.StrictLex as StrictLex
+import Relation.Binary.On as On
 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
 open import Relation.Binary.PropositionalEquality.TrustMe
 
@@ -80,3 +82,11 @@ setoid = PropEq.setoid String
 
 decSetoid : DecSetoid _ _
 decSetoid = PropEq.decSetoid _≟_
+
+-- Lexicographic ordering of strings.
+
+strictTotalOrder : StrictTotalOrder _ _ _
+strictTotalOrder =
+  On.strictTotalOrder
+    (StrictLex.<-strictTotalOrder Char.strictTotalOrder)
+    toList
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 674b973..ddda8b8 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -12,6 +12,7 @@ open import Category.Monad
 open import Category.Monad.Identity
 open import Data.Vec
 open import Data.Nat
+open import Data.Empty using (⊥-elim)
 import Data.Nat.Properties as Nat
 open import Data.Fin as Fin using (Fin; zero; suc; toℕ; fromℕ)
 open import Data.Fin.Props using (_+′_)
@@ -42,8 +43,9 @@ module UsingVectorEquality {s₁ s₂} (S : Setoid s₁ s₂) where
   map-++-commute f []       = refl _
   map-++-commute f (x ∷ xs) = SS.refl ∷-cong map-++-commute f xs
 
-open import Relation.Binary.PropositionalEquality as PropEq
-open import Relation.Binary.HeterogeneousEquality as HetEq
+open import Relation.Binary.PropositionalEquality as P
+  using (_≡_; _≢_; refl; _≗_)
+open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)
 
 -- lookup is an applicative functor morphism.
 
@@ -78,7 +80,7 @@ lookup∘tabulate f (suc i) = lookup∘tabulate (f ∘ suc) i
 tabulate∘lookup : ∀ {a n} {A : Set a} (xs : Vec A n) →
                   tabulate (flip lookup xs) ≡ xs
 tabulate∘lookup []       = refl
-tabulate∘lookup (x ∷ xs) = PropEq.cong (_∷_ x) $ tabulate∘lookup xs
+tabulate∘lookup (x ∷ xs) = P.cong (_∷_ x) $ tabulate∘lookup xs
 
 -- If you look up an index in allFin n, then you get the index.
 
@@ -121,19 +123,19 @@ lookup-++-+′ (x ∷ xs) ys       i       = lookup-++-+′ xs ys i
 map-cong : ∀ {a b n} {A : Set a} {B : Set b} {f g : A → B} →
            f ≗ g → _≗_ {A = Vec A n} (map f) (map g)
 map-cong f≗g []       = refl
-map-cong f≗g (x ∷ xs) = PropEq.cong₂ _∷_ (f≗g x) (map-cong f≗g xs)
+map-cong f≗g (x ∷ xs) = P.cong₂ _∷_ (f≗g x) (map-cong f≗g xs)
 
 -- map is functorial.
 
 map-id : ∀ {a n} {A : Set a} → _≗_ {A = Vec A n} (map id) id
 map-id []       = refl
-map-id (x ∷ xs) = PropEq.cong (_∷_ x) (map-id xs)
+map-id (x ∷ xs) = P.cong (_∷_ x) (map-id xs)
 
 map-∘ : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c}
         (f : B → C) (g : A → B) →
         _≗_ {A = Vec A n} (map (f ∘ g)) (map f ∘ map g)
 map-∘ f g []       = refl
-map-∘ f g (x ∷ xs) = PropEq.cong (_∷_ (f (g x))) (map-∘ f g xs)
+map-∘ f g (x ∷ xs) = P.cong (_∷_ (f (g x))) (map-∘ f g xs)
 
 -- tabulate can be expressed using map and allFin.
 
@@ -142,7 +144,7 @@ tabulate-∘ : ∀ {n a b} {A : Set a} {B : Set b}
              tabulate (f ∘ g) ≡ map f (tabulate g)
 tabulate-∘ {zero}  f g = refl
 tabulate-∘ {suc n} f g =
-  PropEq.cong (_∷_ (f (g zero))) (tabulate-∘ f (g ∘ suc))
+  P.cong (_∷_ (f (g zero))) (tabulate-∘ f (g ∘ suc))
 
 tabulate-allFin : ∀ {n a} {A : Set a} (f : Fin n → A) →
                   tabulate f ≡ map f (allFin n)
@@ -151,7 +153,7 @@ tabulate-allFin f = tabulate-∘ f id
 -- The positive case of allFin can be expressed recursively using map.
 
 allFin-map : ∀ n → allFin (suc n) ≡ zero ∷ map suc (allFin n)
-allFin-map n = PropEq.cong (_∷_ zero) $ tabulate-∘ suc id
+allFin-map n = P.cong (_∷_ zero) $ tabulate-∘ suc id
 
 -- If you look up every possible index, in increasing order, then you
 -- get back the vector you started with.
@@ -159,10 +161,10 @@ allFin-map n = PropEq.cong (_∷_ zero) $ tabulate-∘ suc id
 map-lookup-allFin : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
                     map (λ x → lookup x xs) (allFin n) ≡ xs
 map-lookup-allFin {n = n} xs = begin
-  map (λ x → lookup x xs) (allFin n) ≡⟨ PropEq.sym $ tabulate-∘ (λ x → lookup x xs) id ⟩
+  map (λ x → lookup x xs) (allFin n) ≡⟨ P.sym $ tabulate-∘ (λ x → lookup x xs) id ⟩
   tabulate (λ x → lookup x xs)       ≡⟨ tabulate∘lookup xs ⟩
   xs                                 ∎
-  where open ≡-Reasoning
+  where open P.≡-Reasoning
 
 -- sum commutes with _++_.
 
@@ -171,13 +173,13 @@ sum-++-commute : ∀ {m n} (xs : Vec ℕ m) {ys : Vec ℕ n} →
 sum-++-commute []            = refl
 sum-++-commute (x ∷ xs) {ys} = begin
   x + sum (xs ++ ys)
-    ≡⟨ PropEq.cong (λ p → x + p) (sum-++-commute xs) ⟩
+    ≡⟨ P.cong (λ p → x + p) (sum-++-commute xs) ⟩
   x + (sum xs + sum ys)
-    ≡⟨ PropEq.sym (+-assoc x (sum xs) (sum ys)) ⟩
+    ≡⟨ P.sym (+-assoc x (sum xs) (sum ys)) ⟩
   sum (x ∷ xs) + sum ys
     ∎
   where
-  open ≡-Reasoning
+  open P.≡-Reasoning
   open CommutativeSemiring Nat.commutativeSemiring hiding (_+_; sym)
 
 -- foldr is a congruence.
@@ -225,10 +227,10 @@ foldr-universal B f {e} h base step (x ∷ xs) = begin
   h (x ∷ xs)
     ≡⟨ step x xs ⟩
   f x (h xs)
-    ≡⟨ PropEq.cong (f x) (foldr-universal B f h base step xs) ⟩
+    ≡⟨ P.cong (f x) (foldr-universal B f h base step xs) ⟩
   f x (foldr B f e xs)
     ∎
-  where open ≡-Reasoning
+  where open P.≡-Reasoning
 
 -- A fusion law for foldr.
 
@@ -252,18 +254,18 @@ proof-irrelevance-[]= : ∀ {a} {A : Set a} {n} {xs : Vec A n} {i x} →
                         (p q : xs [ i ]= x) → p ≡ q
 proof-irrelevance-[]= here            here             = refl
 proof-irrelevance-[]= (there xs[i]=x) (there xs[i]=x') =
-  PropEq.cong there (proof-irrelevance-[]= xs[i]=x xs[i]=x')
+  P.cong there (proof-irrelevance-[]= xs[i]=x xs[i]=x')
 
 -- _[_]=_ can be expressed using lookup and _≡_.
 
 []=↔lookup : ∀ {a n i} {A : Set a} {x} {xs : Vec A n} →
              xs [ i ]= x ↔ lookup i xs ≡ x
 []=↔lookup {i = i} {x = x} {xs} = record
-  { to         = PropEq.→-to-⟶ to
-  ; from       = PropEq.→-to-⟶ (from i xs)
+  { to         = P.→-to-⟶ to
+  ; from       = P.→-to-⟶ (from i xs)
   ; inverse-of = record
     { left-inverse-of  = λ _ → proof-irrelevance-[]= _ _
-    ; right-inverse-of = λ _ → PropEq.proof-irrelevance _ _
+    ; right-inverse-of = λ _ → P.proof-irrelevance _ _
     }
   }
   where
@@ -274,3 +276,52 @@ proof-irrelevance-[]= (there xs[i]=x) (there xs[i]=x') =
   from : ∀ {n} (i : Fin n) xs → lookup i xs ≡ x → xs [ i ]= x
   from zero    (.x ∷ _)  refl = here
   from (suc i) (_  ∷ xs) p    = there (from i xs p)
+
+------------------------------------------------------------------------
+-- Some properties related to _[_]≔_
+
+[]≔-idempotent :
+  ∀ {n a} {A : Set a} (xs : Vec A n) (i : Fin n) {x₁ x₂ : A} →
+  (xs [ i ]≔ x₁) [ i ]≔ x₂ ≡ xs [ i ]≔ x₂
+[]≔-idempotent []       ()
+[]≔-idempotent (x ∷ xs) zero    = refl
+[]≔-idempotent (x ∷ xs) (suc i) = P.cong (_∷_ x) $ []≔-idempotent xs i
+
+[]≔-commutes :
+  ∀ {n a} {A : Set a} (xs : Vec A n) (i j : Fin n) {x y : A} →
+  i ≢ j → (xs [ i ]≔ x) [ j ]≔ y ≡ (xs [ j ]≔ y) [ i ]≔ x
+[]≔-commutes []       ()      ()      _
+[]≔-commutes (x ∷ xs) zero    zero    0≢0 = ⊥-elim $ 0≢0 refl
+[]≔-commutes (x ∷ xs) zero    (suc i) _   = refl
+[]≔-commutes (x ∷ xs) (suc i) zero    _   = refl
+[]≔-commutes (x ∷ xs) (suc i) (suc j) i≢j =
+  P.cong (_∷_ x) $ []≔-commutes xs i j (i≢j ∘ P.cong suc)
+
+[]≔-updates : ∀ {n a} {A : Set a} (xs : Vec A n) (i : Fin n) {x : A} →
+              (xs [ i ]≔ x) [ i ]= x
+[]≔-updates []       ()
+[]≔-updates (x ∷ xs) zero    = here
+[]≔-updates (x ∷ xs) (suc i) = there ([]≔-updates xs i)
+
+[]≔-minimal :
+  ∀ {n a} {A : Set a} (xs : Vec A n) (i j : Fin n) {x y : A} →
+  i ≢ j → xs [ i ]= x → (xs [ j ]≔ y) [ i ]= x
+[]≔-minimal []       ()      ()      _   _
+[]≔-minimal (x ∷ xs) .zero   zero    0≢0 here        = ⊥-elim $ 0≢0 refl
+[]≔-minimal (x ∷ xs) .zero   (suc j) _   here        = here
+[]≔-minimal (x ∷ xs) (suc i) zero    _   (there loc) = there loc
+[]≔-minimal (x ∷ xs) (suc i) (suc j) i≢j (there loc) =
+  there ([]≔-minimal xs i j (i≢j ∘ P.cong suc) loc)
+
+map-[]≔ : ∀ {n a b} {A : Set a} {B : Set b}
+          (f : A → B) (xs : Vec A n) (i : Fin n) {x : A} →
+          map f (xs [ i ]≔ x) ≡ map f xs [ i ]≔ f x
+map-[]≔ f []       ()
+map-[]≔ f (x ∷ xs) zero    = refl
+map-[]≔ f (x ∷ xs) (suc i) = P.cong (_∷_ _) $ map-[]≔ f xs i
+
+[]≔-lookup : ∀ {a} {A : Set a} {n} (xs : Vec A n) (i : Fin n) →
+             xs [ i ]≔ lookup i xs ≡ xs
+[]≔-lookup []       ()
+[]≔-lookup (x ∷ xs) zero    = refl
+[]≔-lookup (x ∷ xs) (suc i) = P.cong (_∷_ x) $ []≔-lookup xs i
diff --git a/src/Relation/Binary/HeterogeneousEquality.agda b/src/Relation/Binary/HeterogeneousEquality.agda
index 29c2ffb..f724d09 100644
--- a/src/Relation/Binary/HeterogeneousEquality.agda
+++ b/src/Relation/Binary/HeterogeneousEquality.agda
@@ -50,7 +50,7 @@ sym refl = refl
 trans : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
           {x : A} {y : B} {z : C} →
         x ≅ y → y ≅ z → x ≅ z
-trans refl refl = refl
+trans refl eq = eq
 
 subst : ∀ {a} {A : Set a} {p} → Substitutive {A = A} (λ x y → x ≅ y) p
 subst P refl p = p
diff --git a/src/Relation/Binary/On.agda b/src/Relation/Binary/On.agda
index 8c86599..e9a7b47 100644
--- a/src/Relation/Binary/On.agda
+++ b/src/Relation/Binary/On.agda
@@ -6,127 +6,201 @@
 
 open import Relation.Binary
 
-module Relation.Binary.On {a b} {A : Set a} {B : Set b}
-                          (f : B → A) where
+module Relation.Binary.On where
 
 open import Function
 open import Data.Product
 
-implies : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) →
-          ≈ ⇒ ∼ → (≈ on f) ⇒ (∼ on f)
-implies _ _ impl = impl
-
-reflexive : ∀ {ℓ} (∼ : Rel A ℓ) → Reflexive ∼ → Reflexive (∼ on f)
-reflexive _ refl = refl
-
-irreflexive : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) →
-              Irreflexive ≈ ∼ → Irreflexive (≈ on f) (∼ on f)
-irreflexive _ _ irrefl = irrefl
-
-symmetric : ∀ {ℓ} (∼ : Rel A ℓ) → Symmetric ∼ → Symmetric (∼ on f)
-symmetric _ sym = sym
-
-transitive : ∀ {ℓ} (∼ : Rel A ℓ) → Transitive ∼ → Transitive (∼ on f)
-transitive _ trans = trans
-
-antisymmetric : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (≤ : Rel A ℓ₂) →
-                Antisymmetric ≈ ≤ → Antisymmetric (≈ on f) (≤ on f)
-antisymmetric _ _ antisym = antisym
-
-asymmetric : ∀ {ℓ} (< : Rel A ℓ) → Asymmetric < → Asymmetric (< on f)
-asymmetric _ asym = asym
-
-respects : ∀ {ℓ p} (∼ : Rel A ℓ) (P : A → Set p) →
-           P Respects ∼ → (P ∘ f) Respects (∼ on f)
-respects _ _ resp = resp
-
-respects₂ : ∀ {ℓ₁ ℓ₂} (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) →
-            ∼₁ Respects₂ ∼₂ → (∼₁ on f) Respects₂ (∼₂ on f)
-respects₂ _ _ (resp₁ , resp₂) =
-  ((λ {_} {_} {_} → resp₁) , λ {_} {_} {_} → resp₂)
-
-decidable : ∀ {ℓ} (∼ : Rel A ℓ) → Decidable ∼ → Decidable (∼ on f)
-decidable _ dec = λ x y → dec (f x) (f y)
-
-total : ∀ {ℓ} (∼ : Rel A ℓ) → Total ∼ → Total (∼ on f)
-total _ tot = λ x y → tot (f x) (f y)
-
-trichotomous : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (< : Rel A ℓ₂) →
-               Trichotomous ≈ < → Trichotomous (≈ on f) (< on f)
-trichotomous _ _ compare = λ x y → compare (f x) (f y)
+private
+ module Dummy {a b} {A : Set a} {B : Set b} (f : B → A) where
+
+  implies : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) →
+            ≈ ⇒ ∼ → (≈ on f) ⇒ (∼ on f)
+  implies _ _ impl = impl
+
+  reflexive : ∀ {ℓ} (∼ : Rel A ℓ) → Reflexive ∼ → Reflexive (∼ on f)
+  reflexive _ refl = refl
+
+  irreflexive : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) →
+                Irreflexive ≈ ∼ → Irreflexive (≈ on f) (∼ on f)
+  irreflexive _ _ irrefl = irrefl
+
+  symmetric : ∀ {ℓ} (∼ : Rel A ℓ) → Symmetric ∼ → Symmetric (∼ on f)
+  symmetric _ sym = sym
+
+  transitive : ∀ {ℓ} (∼ : Rel A ℓ) → Transitive ∼ → Transitive (∼ on f)
+  transitive _ trans = trans
+
+  antisymmetric : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (≤ : Rel A ℓ₂) →
+                  Antisymmetric ≈ ≤ → Antisymmetric (≈ on f) (≤ on f)
+  antisymmetric _ _ antisym = antisym
+
+  asymmetric : ∀ {ℓ} (< : Rel A ℓ) → Asymmetric < → Asymmetric (< on f)
+  asymmetric _ asym = asym
+
+  respects : ∀ {ℓ p} (∼ : Rel A ℓ) (P : A → Set p) →
+             P Respects ∼ → (P ∘ f) Respects (∼ on f)
+  respects _ _ resp = resp
+
+  respects₂ : ∀ {ℓ₁ ℓ₂} (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) →
+              ∼₁ Respects₂ ∼₂ → (∼₁ on f) Respects₂ (∼₂ on f)
+  respects₂ _ _ (resp₁ , resp₂) =
+    ((λ {_} {_} {_} → resp₁) , λ {_} {_} {_} → resp₂)
+
+  decidable : ∀ {ℓ} (∼ : Rel A ℓ) → Decidable ∼ → Decidable (∼ on f)
+  decidable _ dec = λ x y → dec (f x) (f y)
+
+  total : ∀ {ℓ} (∼ : Rel A ℓ) → Total ∼ → Total (∼ on f)
+  total _ tot = λ x y → tot (f x) (f y)
+
+  trichotomous : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (< : Rel A ℓ₂) →
+                 Trichotomous ≈ < → Trichotomous (≈ on f) (< on f)
+  trichotomous _ _ compare = λ x y → compare (f x) (f y)
+
+  isEquivalence : ∀ {ℓ} {≈ : Rel A ℓ} →
+                  IsEquivalence ≈ → IsEquivalence (≈ on f)
+  isEquivalence {≈ = ≈} eq = record
+    { refl  = reflexive  ≈ Eq.refl
+    ; sym   = symmetric  ≈ Eq.sym
+    ; trans = transitive ≈ Eq.trans
+    }
+    where module Eq = IsEquivalence eq
+
+  isPreorder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} →
+               IsPreorder ≈ ∼ → IsPreorder (≈ on f) (∼ on f)
+  isPreorder {≈ = ≈} {∼} pre = record
+    { isEquivalence = isEquivalence Pre.isEquivalence
+    ; reflexive     = implies ≈ ∼ Pre.reflexive
+    ; trans         = transitive ∼ Pre.trans
+    }
+    where module Pre = IsPreorder pre
+
+  isDecEquivalence : ∀ {ℓ} {≈ : Rel A ℓ} →
+                     IsDecEquivalence ≈ → IsDecEquivalence (≈ on f)
+  isDecEquivalence {≈ = ≈} dec = record
+    { isEquivalence = isEquivalence Dec.isEquivalence
+    ; _≟_           = decidable ≈ Dec._≟_
+    }
+    where module Dec = IsDecEquivalence dec
+
+  isPartialOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
+                   IsPartialOrder ≈ ≤ →
+                   IsPartialOrder (≈ on f) (≤ on f)
+  isPartialOrder {≈ = ≈} {≤} po = record
+    { isPreorder = isPreorder Po.isPreorder
+    ; antisym    = antisymmetric ≈ ≤ Po.antisym
+    }
+    where module Po = IsPartialOrder po
+
+  isDecPartialOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
+                      IsDecPartialOrder ≈ ≤ →
+                      IsDecPartialOrder (≈ on f) (≤ on f)
+  isDecPartialOrder dpo = record
+    { isPartialOrder = isPartialOrder DPO.isPartialOrder
+    ; _≟_            = decidable _ DPO._≟_
+    ; _≤?_           = decidable _ DPO._≤?_
+    }
+    where module DPO = IsDecPartialOrder dpo
+
+  isStrictPartialOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
+                         IsStrictPartialOrder ≈ < →
+                         IsStrictPartialOrder (≈ on f) (< on f)
+  isStrictPartialOrder {≈ = ≈} {<} spo = record
+    { isEquivalence = isEquivalence Spo.isEquivalence
+    ; irrefl        = irreflexive ≈ < Spo.irrefl
+    ; trans         = transitive < Spo.trans
+    ; <-resp-≈      = respects₂ < ≈ Spo.<-resp-≈
+    }
+    where module Spo = IsStrictPartialOrder spo
+
+  isTotalOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
+                 IsTotalOrder ≈ ≤ →
+                 IsTotalOrder (≈ on f) (≤ on f)
+  isTotalOrder {≈ = ≈} {≤} to = record
+    { isPartialOrder = isPartialOrder To.isPartialOrder
+    ; total          = total ≤ To.total
+    }
+    where module To = IsTotalOrder to
+
+  isDecTotalOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
+                    IsDecTotalOrder ≈ ≤ →
+                    IsDecTotalOrder (≈ on f) (≤ on f)
+  isDecTotalOrder {≈ = ≈} {≤} dec = record
+    { isTotalOrder = isTotalOrder Dec.isTotalOrder
+    ; _≟_          = decidable ≈ Dec._≟_
+    ; _≤?_         = decidable ≤ Dec._≤?_
+    }
+    where module Dec = IsDecTotalOrder dec
+
+  isStrictTotalOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
+                       IsStrictTotalOrder ≈ < →
+                       IsStrictTotalOrder (≈ on f) (< on f)
+  isStrictTotalOrder {≈ = ≈} {<} sto = record
+    { isEquivalence = isEquivalence Sto.isEquivalence
+    ; trans         = transitive < Sto.trans
+    ; compare       = trichotomous ≈ < Sto.compare
+    ; <-resp-≈      = respects₂ < ≈ Sto.<-resp-≈
+    }
+    where module Sto = IsStrictTotalOrder sto
+
+open Dummy public
+
+preorder : ∀ {p₁ p₂ p₃ b} {B : Set b} (P : Preorder p₁ p₂ p₃) →
+           (B → Preorder.Carrier P) → Preorder _ _ _
+preorder P f = record
+  { isPreorder = isPreorder f (Preorder.isPreorder P)
+  }
 
-isEquivalence : ∀ {ℓ} {≈ : Rel A ℓ} →
-                IsEquivalence ≈ → IsEquivalence (≈ on f)
-isEquivalence {≈ = ≈} eq = record
-  { refl  = reflexive  ≈ Eq.refl
-  ; sym   = symmetric  ≈ Eq.sym
-  ; trans = transitive ≈ Eq.trans
+setoid : ∀ {s₁ s₂ b} {B : Set b} (S : Setoid s₁ s₂) →
+         (B → Setoid.Carrier S) → Setoid _ _
+setoid S f = record
+  { isEquivalence = isEquivalence f (Setoid.isEquivalence S)
   }
-  where module Eq = IsEquivalence eq
-
-isPreorder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} →
-             IsPreorder ≈ ∼ → IsPreorder (≈ on f) (∼ on f)
-isPreorder {≈ = ≈} {∼} pre = record
-  { isEquivalence = isEquivalence Pre.isEquivalence
-  ; reflexive     = implies ≈ ∼ Pre.reflexive
-  ; trans         = transitive ∼ Pre.trans
+
+decSetoid : ∀ {d₁ d₂ b} {B : Set b} (D : DecSetoid d₁ d₂) →
+            (B → DecSetoid.Carrier D) → DecSetoid _ _
+decSetoid D f = record
+  { isDecEquivalence = isDecEquivalence f (DecSetoid.isDecEquivalence D)
   }
-  where module Pre = IsPreorder pre
 
-isDecEquivalence : ∀ {ℓ} {≈ : Rel A ℓ} →
-                   IsDecEquivalence ≈ → IsDecEquivalence (≈ on f)
-isDecEquivalence {≈ = ≈} dec = record
-  { isEquivalence = isEquivalence Dec.isEquivalence
-  ; _≟_           = decidable ≈ Dec._≟_
+poset : ∀ {p₁ p₂ p₃ b} {B : Set b} (P : Poset p₁ p₂ p₃) →
+        (B → Poset.Carrier P) → Poset _ _ _
+poset P f = record
+  { isPartialOrder = isPartialOrder f (Poset.isPartialOrder P)
   }
-  where module Dec = IsDecEquivalence dec
-
-isPartialOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
-                 IsPartialOrder ≈ ≤ →
-                 IsPartialOrder (≈ on f) (≤ on f)
-isPartialOrder {≈ = ≈} {≤} po = record
-  { isPreorder = isPreorder Po.isPreorder
-  ; antisym    = antisymmetric ≈ ≤ Po.antisym
+
+decPoset : ∀ {d₁ d₂ d₃ b} {B : Set b} (D : DecPoset d₁ d₂ d₃) →
+           (B → DecPoset.Carrier D) → DecPoset _ _ _
+decPoset D f = record
+  { isDecPartialOrder =
+      isDecPartialOrder f (DecPoset.isDecPartialOrder D)
   }
-  where module Po = IsPartialOrder po
-
-isStrictPartialOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
-                       IsStrictPartialOrder ≈ < →
-                       IsStrictPartialOrder (≈ on f) (< on f)
-isStrictPartialOrder {≈ = ≈} {<} spo = record
-  { isEquivalence = isEquivalence Spo.isEquivalence
-  ; irrefl        = irreflexive ≈ < Spo.irrefl
-  ; trans         = transitive < Spo.trans
-  ; <-resp-≈      = respects₂ < ≈ Spo.<-resp-≈
+
+strictPartialOrder :
+  ∀ {s₁ s₂ s₃ b} {B : Set b} (S : StrictPartialOrder s₁ s₂ s₃) →
+  (B → StrictPartialOrder.Carrier S) → StrictPartialOrder _ _ _
+strictPartialOrder S f = record
+  { isStrictPartialOrder =
+      isStrictPartialOrder f (StrictPartialOrder.isStrictPartialOrder S)
   }
-  where module Spo = IsStrictPartialOrder spo
-
-isTotalOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
-               IsTotalOrder ≈ ≤ →
-               IsTotalOrder (≈ on f) (≤ on f)
-isTotalOrder {≈ = ≈} {≤} to = record
-  { isPartialOrder = isPartialOrder To.isPartialOrder
-  ; total          = total ≤ To.total
+
+totalOrder : ∀ {t₁ t₂ t₃ b} {B : Set b} (T : TotalOrder t₁ t₂ t₃) →
+             (B → TotalOrder.Carrier T) → TotalOrder _ _ _
+totalOrder T f = record
+  { isTotalOrder = isTotalOrder f (TotalOrder.isTotalOrder T)
   }
-  where module To = IsTotalOrder to
-
-isDecTotalOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
-                  IsDecTotalOrder ≈ ≤ →
-                  IsDecTotalOrder (≈ on f) (≤ on f)
-isDecTotalOrder {≈ = ≈} {≤} dec = record
-  { isTotalOrder = isTotalOrder Dec.isTotalOrder
-  ; _≟_          = decidable ≈ Dec._≟_
-  ; _≤?_         = decidable ≤ Dec._≤?_
+
+decTotalOrder :
+  ∀ {d₁ d₂ d₃ b} {B : Set b} (D : DecTotalOrder d₁ d₂ d₃) →
+  (B → DecTotalOrder.Carrier D) → DecTotalOrder _ _ _
+decTotalOrder D f = record
+  { isDecTotalOrder = isDecTotalOrder f (DecTotalOrder.isDecTotalOrder D)
   }
-  where module Dec = IsDecTotalOrder dec
 
-isStrictTotalOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
-                     IsStrictTotalOrder ≈ < →
-                       IsStrictTotalOrder (≈ on f) (< on f)
-isStrictTotalOrder {≈ = ≈} {<} sto = record
-  { isEquivalence = isEquivalence Sto.isEquivalence
-  ; trans         = transitive < Sto.trans
-  ; compare       = trichotomous ≈ < Sto.compare
-  ; <-resp-≈      = respects₂ < ≈ Sto.<-resp-≈
+strictTotalOrder :
+  ∀ {s₁ s₂ s₃ b} {B : Set b} (S : StrictTotalOrder s₁ s₂ s₃) →
+  (B → StrictTotalOrder.Carrier S) → StrictTotalOrder _ _ _
+strictTotalOrder S f = record
+  { isStrictTotalOrder =
+      isStrictTotalOrder f (StrictTotalOrder.isStrictTotalOrder S)
   }
-  where module Sto = IsStrictTotalOrder sto
diff --git a/src/Relation/Binary/PropositionalEquality/Core.agda b/src/Relation/Binary/PropositionalEquality/Core.agda
index 17fdf9b..cd2e308 100644
--- a/src/Relation/Binary/PropositionalEquality/Core.agda
+++ b/src/Relation/Binary/PropositionalEquality/Core.agda
@@ -20,7 +20,7 @@ sym : ∀ {a} {A : Set a} → Symmetric (_≡_ {A = A})
 sym refl = refl
 
 trans : ∀ {a} {A : Set a} → Transitive (_≡_ {A = A})
-trans refl refl = refl
+trans refl eq = eq
 
 subst : ∀ {a p} {A : Set a} → Substitutive (_≡_ {A = A}) p
 subst P refl p = p
diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index 2838317..ea3eb3e 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -65,7 +65,7 @@ private
 -- When P is a decidable predicate over a finite set the following
 -- lemma can be proved.
 
-¬∀⟶∃¬ : ∀ n {p} (P : Fin n → Set p) → (∀ i → Dec (P i)) →
+¬∀⟶∃¬ : ∀ n {p} (P : Fin n → Set p) → Decidable P →
         ¬ (∀ i → P i) → ∃ λ i → ¬ P i
 ¬∀⟶∃¬ n P dec ¬P = Prod.map id proj₁ $ ¬∀⟶∃¬-smallest n P dec ¬P
 
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index dc00b32..6670fef 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -132,3 +132,9 @@ P ⟨⊎⟩ Q = [ P , Q ]
 _⟨→⟩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
         Pred A ℓ₁ → Pred B ℓ₂ → Pred (A → B) _
 (P ⟨→⟩ Q) f = P ⊆ Q ∘ f
+
+------------------------------------------------------------------------
+-- Properties of unary relations
+
+Decidable : ∀ {a p} {A : Set a} (P : A → Set p) → Set _
+Decidable P = ∀ x → Dec (P x)