From b6ef9b46f291660cc7071310a8d1750111546422 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <patrick+github@patrickstevens.co.uk>
Date: Sun, 29 Dec 2019 12:11:21 +0000
Subject: [PATCH] Reshuffle orders (#91)

---
 Everything/Safe.agda                          |   4 +-
 Fields/CauchyCompletion/Approximation.agda    |   1 -
 Fields/Fields.agda                            |   2 -
 Fields/Orders/Lemmas.agda                     |   1 -
 Fields/Orders/Partial/Definition.agda         |   1 -
 Fields/Orders/Total/Definition.agda           |   1 -
 Groups/FirstIsomorphismTheorem.agda           |   1 -
 Groups/Homomorphisms/Image.agda               |   1 -
 Groups/Homomorphisms/Kernel.agda              |   1 -
 Groups/Subgroups/Normal/Definition.agda       |   1 -
 Groups/Subgroups/Normal/Examples.agda         |   1 -
 Groups/Subgroups/Normal/Lemmas.agda           |   1 -
 KeyValue/KeyValue.agda                        |  24 +-
 KeyValue/LinearStore/Definition.agda          |  62 +--
 KeyValue/LinearStore/Implementation.agda      | 381 +++++++++---------
 Numbers/BinaryNaturals/Addition.agda          |   2 +-
 Numbers/BinaryNaturals/Definition.agda        |   2 +-
 Numbers/BinaryNaturals/Order.agda             |  52 +--
 Numbers/BinaryNaturals/Subtraction.agda       |   2 +-
 Numbers/BinaryNaturals/SubtractionGo.agda     |   1 -
 Numbers/Integers/Order.agda                   |   3 +-
 .../RingStructure/EuclideanDomain.agda        |   2 +-
 Numbers/Modulo/Addition.agda                  |   2 +-
 Numbers/Modulo/Definition.agda                |   1 -
 Numbers/Modulo/Group.agda                     |   2 +-
 Numbers/Naturals/EuclideanAlgorithm.agda      |   4 +-
 Numbers/Naturals/Naturals.agda                |   3 +-
 Numbers/Naturals/Order.agda                   |   3 +-
 Numbers/Naturals/Order/Lemmas.agda            |   1 -
 Numbers/Naturals/Order/WellFounded.agda       |   4 +-
 Numbers/Naturals/Semiring.agda                |   2 -
 Numbers/Naturals/Subtraction.agda             |   2 -
 Numbers/Naturals/WithK.agda                   |   2 -
 Numbers/Primes/IntegerFactorisation.agda      |   4 +-
 Numbers/Primes/PrimeNumbers.agda              |   4 +-
 Numbers/Rationals/Lemmas.agda                 |   8 +-
 Orders.agda                                   | 109 -----
 Orders/Partial/Definition.agda                |  16 +
 Orders/Total/Definition.agda                  |  36 ++
 Orders/Total/Lemmas.agda                      |  81 ++++
 Orders/WellFounded/Definition.agda            |  14 +
 Orders/WellFounded/Induction.agda             |  26 ++
 Rings/EuclideanDomains/Definition.agda        |   2 +-
 Rings/Examples/Proofs.agda                    |   4 +-
 Rings/Ideals/Prime/Definition.agda            |   1 -
 Rings/IntegralDomains/Definition.agda         |   1 -
 Rings/IntegralDomains/Examples.agda           |   1 -
 Rings/IntegralDomains/Lemmas.agda             |   1 -
 Rings/Primes/Lemmas.agda                      |   1 -
 Setoids/Orders.agda                           |   7 +-
 Sets/CantorBijection/CantorBijection.agda     |   2 -
 Sets/CantorBijection/Order.agda               |   6 +-
 Sets/CantorBijection/Proofs.agda              |   4 +-
 Sets/Cardinality.agda                         |   3 +-
 Sets/FinSet.agda                              |   1 -
 Vectors.agda                                  |   4 +-
 WellFoundedInduction.agda                     |  29 --
 57 files changed, 476 insertions(+), 462 deletions(-)
 delete mode 100644 Orders.agda
 create mode 100644 Orders/Partial/Definition.agda
 create mode 100644 Orders/Total/Definition.agda
 create mode 100644 Orders/Total/Lemmas.agda
 create mode 100644 Orders/WellFounded/Definition.agda
 create mode 100644 Orders/WellFounded/Induction.agda
 delete mode 100644 WellFoundedInduction.agda

diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index 4186068..2ec4126 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -96,8 +96,8 @@ open import KeyValue.KeyValue
 open import KeyValue.LinearStore.Definition
 
 open import Maybe
-open import Orders
-open import WellFoundedInduction
+open import Orders.Total.Lemmas
+open import Orders.WellFounded.Induction
 
 open import ClassicalLogic.ClassicalFive
 
diff --git a/Fields/CauchyCompletion/Approximation.agda b/Fields/CauchyCompletion/Approximation.agda
index 4d6f924..43ca92c 100644
--- a/Fields/CauchyCompletion/Approximation.agda
+++ b/Fields/CauchyCompletion/Approximation.agda
@@ -1,7 +1,6 @@
 {-# OPTIONS --safe --warning=error --without-K --guardedness #-}
 
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-open import Orders
 open import Setoids.Setoids
 open import Rings.Definition
 open import Rings.Lemmas
diff --git a/Fields/Fields.agda b/Fields/Fields.agda
index 980fd1d..b01b3b0 100644
--- a/Fields/Fields.agda
+++ b/Fields/Fields.agda
@@ -6,8 +6,6 @@ open import Groups.Definition
 open import Rings.Definition
 open import Rings.Lemmas
 open import Setoids.Setoids
-open import Setoids.Orders
-open import Orders
 open import Rings.IntegralDomains.Definition
 open import Functions
 open import Sets.EquivalenceRelations
diff --git a/Fields/Orders/Lemmas.agda b/Fields/Orders/Lemmas.agda
index 20ec5a5..80bfe0c 100644
--- a/Fields/Orders/Lemmas.agda
+++ b/Fields/Orders/Lemmas.agda
@@ -10,7 +10,6 @@ open import Rings.Orders.Total.Definition
 open import Rings.Lemmas
 open import Setoids.Setoids
 open import Setoids.Orders
-open import Orders
 open import Rings.IntegralDomains.Definition
 open import Functions
 open import Sets.EquivalenceRelations
diff --git a/Fields/Orders/Partial/Definition.agda b/Fields/Orders/Partial/Definition.agda
index 3ea5c37..e04a206 100644
--- a/Fields/Orders/Partial/Definition.agda
+++ b/Fields/Orders/Partial/Definition.agda
@@ -8,7 +8,6 @@ open import Rings.Orders.Partial.Definition
 open import Rings.Lemmas
 open import Setoids.Setoids
 open import Setoids.Orders
-open import Orders
 open import Functions
 open import Sets.EquivalenceRelations
 open import Fields.Fields
diff --git a/Fields/Orders/Total/Definition.agda b/Fields/Orders/Total/Definition.agda
index bf6fd38..acaaaac 100644
--- a/Fields/Orders/Total/Definition.agda
+++ b/Fields/Orders/Total/Definition.agda
@@ -9,7 +9,6 @@ open import Rings.Orders.Total.Definition
 open import Rings.Lemmas
 open import Setoids.Setoids
 open import Setoids.Orders
-open import Orders
 open import Functions
 open import Sets.EquivalenceRelations
 open import Fields.Fields
diff --git a/Groups/FirstIsomorphismTheorem.agda b/Groups/FirstIsomorphismTheorem.agda
index a0cbb30..1479a51 100644
--- a/Groups/FirstIsomorphismTheorem.agda
+++ b/Groups/FirstIsomorphismTheorem.agda
@@ -2,7 +2,6 @@
 
 open import Groups.Groups
 open import Groups.Definition
-open import Orders
 open import Numbers.Integers.Integers
 open import Setoids.Setoids
 open import LogicalFormulae
diff --git a/Groups/Homomorphisms/Image.agda b/Groups/Homomorphisms/Image.agda
index f0f1eec..a0627ac 100644
--- a/Groups/Homomorphisms/Image.agda
+++ b/Groups/Homomorphisms/Image.agda
@@ -2,7 +2,6 @@
 
 open import Groups.Groups
 open import Groups.Definition
-open import Orders
 open import Numbers.Integers.Integers
 open import Setoids.Setoids
 open import Setoids.Subset
diff --git a/Groups/Homomorphisms/Kernel.agda b/Groups/Homomorphisms/Kernel.agda
index e5d6ed1..52b914b 100644
--- a/Groups/Homomorphisms/Kernel.agda
+++ b/Groups/Homomorphisms/Kernel.agda
@@ -2,7 +2,6 @@
 
 open import Groups.Groups
 open import Groups.Definition
-open import Orders
 open import Numbers.Integers.Integers
 open import Setoids.Setoids
 open import LogicalFormulae
diff --git a/Groups/Subgroups/Normal/Definition.agda b/Groups/Subgroups/Normal/Definition.agda
index 28bacff..1fabb91 100644
--- a/Groups/Subgroups/Normal/Definition.agda
+++ b/Groups/Subgroups/Normal/Definition.agda
@@ -2,7 +2,6 @@
 
 open import Groups.Groups
 open import Groups.Definition
-open import Orders
 open import Numbers.Integers.Integers
 open import Setoids.Setoids
 open import LogicalFormulae
diff --git a/Groups/Subgroups/Normal/Examples.agda b/Groups/Subgroups/Normal/Examples.agda
index 1779bc4..9d86107 100644
--- a/Groups/Subgroups/Normal/Examples.agda
+++ b/Groups/Subgroups/Normal/Examples.agda
@@ -2,7 +2,6 @@
 
 open import Groups.Groups
 open import Groups.Definition
-open import Orders
 open import Numbers.Integers.Integers
 open import Setoids.Setoids
 open import LogicalFormulae
diff --git a/Groups/Subgroups/Normal/Lemmas.agda b/Groups/Subgroups/Normal/Lemmas.agda
index 76c4790..15fe3a4 100644
--- a/Groups/Subgroups/Normal/Lemmas.agda
+++ b/Groups/Subgroups/Normal/Lemmas.agda
@@ -2,7 +2,6 @@
 
 open import Groups.Groups
 open import Groups.Definition
-open import Orders
 open import Numbers.Integers.Integers
 open import Setoids.Setoids
 open import LogicalFormulae
diff --git a/KeyValue/KeyValue.agda b/KeyValue/KeyValue.agda
index 74dd67e..9fc59db 100644
--- a/KeyValue/KeyValue.agda
+++ b/KeyValue/KeyValue.agda
@@ -1,7 +1,6 @@
 {-# OPTIONS --warning=error --safe --without-K #-}
 
 open import LogicalFormulae
-open import Orders
 open import Maybe
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import Vectors
@@ -9,14 +8,15 @@ open import Vectors
 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 
-module KeyValue.KeyValue where
-  record KeyValue {a b c : _} (keys : Set a) (values : Set b) (maps : Set c) : Set (a ⊔ b ⊔ c) where
-    field
-      tryFind : maps → keys → Maybe values
-      add : (map : maps) → keys → values → maps
-      empty : maps
-      count : maps → ℕ
-      lookupAfterAdd : (map : maps) → (k : keys) → (v : values) → tryFind (add map k v) k ≡ yes v
-      lookupAfterAdd' : (map : maps) → (k1 : keys) → (v : values) → (k2 : keys) → (k1 ≡ k2) || (tryFind (add map k1 v) k2 ≡ tryFind map k2)
-      countAfterAdd' : (map : maps) → (k : keys) → (v : values) → (tryFind map k ≡ no) → count (add map k v) ≡ succ (count map)
-      countAfterAdd : (map : maps) → (k : keys) → (v1 v2 : values) → (tryFind map k ≡ yes v2) → count (add map k v1) ≡ count map
+module KeyValue.KeyValue {a b : _} (keys : Set a) (values : Set b) where
+
+record KeyValue {c : _} (maps : Set c) : Set (a ⊔ b ⊔ c) where
+  field
+    tryFind : maps → keys → Maybe values
+    add : (map : maps) → keys → values → maps
+    empty : maps
+    count : maps → ℕ
+    lookupAfterAdd : (map : maps) → (k : keys) → (v : values) → tryFind (add map k v) k ≡ yes v
+    lookupAfterAdd' : (map : maps) → (k1 : keys) → (v : values) → (k2 : keys) → (k1 ≡ k2) || (tryFind (add map k1 v) k2 ≡ tryFind map k2)
+    countAfterAdd' : (map : maps) → (k : keys) → (v : values) → (tryFind map k ≡ no) → count (add map k v) ≡ succ (count map)
+    countAfterAdd : (map : maps) → (k : keys) → (v1 v2 : values) → (tryFind map k ≡ yes v2) → count (add map k v1) ≡ count map
diff --git a/KeyValue/LinearStore/Definition.agda b/KeyValue/LinearStore/Definition.agda
index 17dccd3..6b6c43f 100644
--- a/KeyValue/LinearStore/Definition.agda
+++ b/KeyValue/LinearStore/Definition.agda
@@ -1,35 +1,37 @@
 {-# OPTIONS --warning=error --safe --without-K #-}
 
-open import KeyValue.LinearStore.Implementation
-open import KeyValue.KeyValue
-open import Orders
+open import Orders.Total.Definition
 open import LogicalFormulae
 open import Maybe
 
-module KeyValue.LinearStore.Definition where
-  LinearStore : {a b c : _} (keys : Set a) (values : Set b) (keyOrder : TotalOrder {_} {c} keys) → KeyValue keys values (Map keys values keyOrder)
-  KeyValue.tryFind (LinearStore keys values keyOrder) = lookup {keys = keys} {values} {keyOrder}
-  KeyValue.add (LinearStore keys values keyOrder) = addMap
-  KeyValue.empty (LinearStore keys values keyOrder) = empty
-  KeyValue.count (LinearStore keys values keyOrder) = count {keys = keys} {values} {keyOrder}
-  KeyValue.lookupAfterAdd (LinearStore keys values keyOrder) empty k v with TotalOrder.totality keyOrder k k
-  KeyValue.lookupAfterAdd (LinearStore keys values keyOrder) empty k v | inl (inl x) = exFalso (TotalOrder.irreflexive keyOrder x)
-  KeyValue.lookupAfterAdd (LinearStore keys values keyOrder) empty k v | inl (inr x) = exFalso (TotalOrder.irreflexive keyOrder x)
-  KeyValue.lookupAfterAdd (LinearStore keys values keyOrder) empty k v | inr x = refl
-  KeyValue.lookupAfterAdd (LinearStore keys values keyOrder) (nonempty x) k v = lookupReducedSucceedsAfterAdd k v x
-  KeyValue.lookupAfterAdd' (LinearStore keys values keyOrder) empty k1 v k2 with TotalOrder.totality keyOrder k1 k2
-  KeyValue.lookupAfterAdd' (LinearStore keys values keyOrder) empty k1 v k2 | inl (inl x) = inr refl
-  KeyValue.lookupAfterAdd' (LinearStore keys values keyOrder) empty k1 v k2 | inl (inr x) = inr refl
-  KeyValue.lookupAfterAdd' (LinearStore keys values keyOrder) empty k1 v k2 | inr x = inl x
-  KeyValue.lookupAfterAdd' (LinearStore keys values keyOrder) (nonempty x) k1 v k2 with TotalOrder.totality keyOrder k1 k2
-  KeyValue.lookupAfterAdd' (LinearStore keys values keyOrder) (nonempty map) k1 v k2 | inl (inl x) with inspect (lookupReduced map k2)
-  KeyValue.lookupAfterAdd' (LinearStore keys values keyOrder) (nonempty map) k1 v k2 | inl (inl x) | no with≡ pr rewrite pr = inr (lookupReducedFailsAfterUnrelatedAdd k1 v k2 (inl x) map pr)
-  KeyValue.lookupAfterAdd' (LinearStore keys values keyOrder) (nonempty map) k1 v k2 | inl (inl x) | (yes lookedUp) with≡ pr rewrite pr = inr (lookupReducedSucceedsAfterUnrelatedAdd k1 v k2 lookedUp (inl x) map pr)
-  KeyValue.lookupAfterAdd' (LinearStore keys values keyOrder) (nonempty map) k1 v k2 | inl (inr x) with inspect (lookupReduced map k2)
-  KeyValue.lookupAfterAdd' (LinearStore keys values keyOrder) (nonempty map) k1 v k2 | inl (inr x) | no with≡ pr rewrite pr = inr (lookupReducedFailsAfterUnrelatedAdd k1 v k2 (inr x) map pr)
-  KeyValue.lookupAfterAdd' (LinearStore keys values keyOrder) (nonempty map) k1 v k2 | inl (inr x) | yes lookedUp with≡ pr rewrite pr = inr (lookupReducedSucceedsAfterUnrelatedAdd k1 v k2 lookedUp (inr x) map pr)
-  KeyValue.lookupAfterAdd' (LinearStore keys values keyOrder) (nonempty map) k1 v k2 | inr x = inl x
-  KeyValue.countAfterAdd' (LinearStore keys values keyOrder) empty _ _ _ = refl
-  KeyValue.countAfterAdd' (LinearStore keys values keyOrder) (nonempty x) k v = countReducedBehavesWhenAddingNotPresent k v x
-  KeyValue.countAfterAdd (LinearStore keys values keyOrder) empty _ _ _ ()
-  KeyValue.countAfterAdd (LinearStore keys values keyOrder) (nonempty map) k v1 v2 = countReducedBehavesWhenAddingPresent k v1 v2 map
+module KeyValue.LinearStore.Definition {a b : _} (keySet : Set a) (valueSet : Set b) {c : _} (keyOrder : TotalOrder keySet {c}) where
+
+open import KeyValue.KeyValue keySet valueSet
+open import KeyValue.LinearStore.Implementation keySet valueSet keyOrder
+
+LinearStore : KeyValue Map
+KeyValue.tryFind LinearStore = lookup
+KeyValue.add LinearStore = addMap
+KeyValue.empty LinearStore = empty
+KeyValue.count LinearStore = count
+KeyValue.lookupAfterAdd LinearStore empty k v with TotalOrder.totality keyOrder k k
+KeyValue.lookupAfterAdd LinearStore empty k v | inl (inl x) = exFalso (TotalOrder.irreflexive keyOrder x)
+KeyValue.lookupAfterAdd LinearStore empty k v | inl (inr x) = exFalso (TotalOrder.irreflexive keyOrder x)
+KeyValue.lookupAfterAdd LinearStore empty k v | inr x = refl
+KeyValue.lookupAfterAdd LinearStore (nonempty x) k v = lookupReducedSucceedsAfterAdd k v x
+KeyValue.lookupAfterAdd' LinearStore empty k1 v k2 with TotalOrder.totality keyOrder k1 k2
+KeyValue.lookupAfterAdd' LinearStore empty k1 v k2 | inl (inl x) = inr refl
+KeyValue.lookupAfterAdd' LinearStore empty k1 v k2 | inl (inr x) = inr refl
+KeyValue.lookupAfterAdd' LinearStore empty k1 v k2 | inr x = inl x
+KeyValue.lookupAfterAdd' LinearStore (nonempty x) k1 v k2 with TotalOrder.totality keyOrder k1 k2
+KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inl (inl x) with inspect (lookupReduced map k2)
+KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inl (inl x) | no with≡ pr rewrite pr = inr (lookupReducedFailsAfterUnrelatedAdd k1 v k2 (inl x) map pr)
+KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inl (inl x) | (yes lookedUp) with≡ pr rewrite pr = inr (lookupReducedSucceedsAfterUnrelatedAdd k1 v k2 lookedUp (inl x) map pr)
+KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inl (inr x) with inspect (lookupReduced map k2)
+KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inl (inr x) | no with≡ pr rewrite pr = inr (lookupReducedFailsAfterUnrelatedAdd k1 v k2 (inr x) map pr)
+KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inl (inr x) | yes lookedUp with≡ pr rewrite pr = inr (lookupReducedSucceedsAfterUnrelatedAdd k1 v k2 lookedUp (inr x) map pr)
+KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inr x = inl x
+KeyValue.countAfterAdd' LinearStore empty _ _ _ = refl
+KeyValue.countAfterAdd' LinearStore (nonempty x) k v = countReducedBehavesWhenAddingNotPresent k v x
+KeyValue.countAfterAdd LinearStore empty _ _ _ ()
+KeyValue.countAfterAdd LinearStore (nonempty map) k v1 v2 = countReducedBehavesWhenAddingPresent k v1 v2 map
diff --git a/KeyValue/LinearStore/Implementation.agda b/KeyValue/LinearStore/Implementation.agda
index e917b34..41c6689 100644
--- a/KeyValue/LinearStore/Implementation.agda
+++ b/KeyValue/LinearStore/Implementation.agda
@@ -1,7 +1,8 @@
 {-# OPTIONS --warning=error --safe --without-K #-}
 
 open import LogicalFormulae
-open import Orders
+open import Orders.Total.Definition
+open import Orders.Total.Lemmas
 open import Maybe
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import Vectors
@@ -9,223 +10,223 @@ open import Vectors
 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 
-module KeyValue.LinearStore.Implementation where
+module KeyValue.LinearStore.Implementation {a b c} (keySet : Set a) (valueSet : Set b) (keyOrder : TotalOrder {_} keySet {c}) where
 
-record ReducedMap {a b c : _} (keys : Set a) (values : Set b) (keyOrder : TotalOrder {_} {c} keys) (min : keys) : Set (a ⊔ b ⊔ c)
-record ReducedMap {a} {b} {c} keys values keyOrder min where
+record ReducedMap (min : keySet) : Set (a ⊔ b ⊔ c)
+record ReducedMap min where
   inductive
   field
-    firstEntry : values
-    next : Maybe (Sg keys (λ nextKey → (ReducedMap keys values keyOrder nextKey) && (TotalOrder._<_ keyOrder min nextKey)))
+    firstEntry : valueSet
+    next : Maybe (Sg keySet (λ nextKey → (ReducedMap nextKey) && (TotalOrder._<_ keyOrder min nextKey)))
 
-addReducedMap : {a b c : _} → {keys : Set a} → {values : Set b} → {keyOrder : TotalOrder {_} {c} keys} → {min : keys} → (k : keys) → (v : values) → (m : ReducedMap {a} {b} keys values keyOrder min) → ReducedMap keys values keyOrder (TotalOrder.min keyOrder min k)
-addReducedMap {keyOrder = keyOrder} {min} k v m with TotalOrder.totality keyOrder min k
-addReducedMap {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) = record { firstEntry = firstEntry ; next = yes (k , (record { firstEntry = v ; next = no} ,, min<k))}
-addReducedMap {keyOrder = keyOrder} {min} k v record { firstEntry = minVal ; next = yes (nextKey , (m ,, pr)) } | inl (inl min<k) = record { firstEntry = minVal ; next = yes ((TotalOrder.min keyOrder nextKey k) , (addReducedMap {keyOrder = keyOrder} {_} k v m ,, minFromBoth {order = keyOrder} pr min<k))}
-addReducedMap {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } | inl (inr k<min) = record { firstEntry = v ; next = yes (min , (record { firstEntry = firstEntry ; next = next } ,, k<min)) }
-addReducedMap {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } | inr min=k rewrite min=k = record { firstEntry = v ; next = next }
+addReducedMap : {min : keySet} → (k : keySet) → (v : valueSet) → (m : ReducedMap min) → ReducedMap (TotalOrder.min keyOrder min k)
+addReducedMap {min} k v m with TotalOrder.totality keyOrder min k
+addReducedMap {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) = record { firstEntry = firstEntry ; next = yes (k , (record { firstEntry = v ; next = no} ,, min<k))}
+addReducedMap {min} k v record { firstEntry = minVal ; next = yes (nextKey , (m ,, pr)) } | inl (inl min<k) = record { firstEntry = minVal ; next = yes ((TotalOrder.min keyOrder nextKey k) , (addReducedMap {_} k v m ,, minFromBoth keyOrder pr min<k))}
+addReducedMap {min} k v record { firstEntry = firstEntry ; next = next } | inl (inr k<min) = record { firstEntry = v ; next = yes (min , (record { firstEntry = firstEntry ; next = next } ,, k<min)) }
+addReducedMap {min} k v record { firstEntry = firstEntry ; next = next } | inr min=k rewrite min=k = record { firstEntry = v ; next = next }
 
-lookupReduced : {a b c : _} → {keys : Set a} → {values : Set b} → {keyOrder : TotalOrder {_} {c} keys} → {min : keys} → (m : ReducedMap keys values keyOrder min) → (target : keys) → Maybe values
-lookupReduced {keyOrder = keyOrder} {min} m k with TotalOrder.totality keyOrder min k
-lookupReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = no } k | inl (inl min<k) = no
-lookupReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, _))) } k | inl (inl min<k) = lookupReduced {keyOrder = keyOrder} {newMin} m k
-lookupReduced {keyOrder = keyOrder} {min} m k | inl (inr k<min) = no
-lookupReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = next } k | inr min=k = yes firstEntry
+lookupReduced : {min : keySet} → (m : ReducedMap min) → (target : keySet) → Maybe valueSet
+lookupReduced {min} m k with TotalOrder.totality keyOrder min k
+lookupReduced {min} record { firstEntry = firstEntry ; next = no } k | inl (inl min<k) = no
+lookupReduced {min} record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, _))) } k | inl (inl min<k) = lookupReduced {newMin} m k
+lookupReduced {min} m k | inl (inr k<min) = no
+lookupReduced {min} record { firstEntry = firstEntry ; next = next } k | inr min=k = yes firstEntry
 
-countReduced : {a b c : _} {keys : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keys} {min : keys} → (m : ReducedMap keys values keyOrder min) → ℕ
+countReduced : {min : keySet} → (m : ReducedMap min) → ℕ
 countReduced record { firstEntry = firstEntry ; next = no } = 1
 countReduced record { firstEntry = firstEntry ; next = (yes (key , (m ,, pr))) } = succ (countReduced m)
 
-lookupReducedSucceedsAfterAdd : {a b c : _} → {keys : Set a} → {values : Set b} → {keyOrder : TotalOrder {_} {c} keys} → {min : keys} → (k : keys) → (v : values) → (m : ReducedMap keys values keyOrder min) → (lookupReduced (addReducedMap k v m) k ≡ yes v)
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m with TotalOrder.totality keyOrder min k
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) with TotalOrder.totality keyOrder min k
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) with TotalOrder.totality keyOrder k k
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) | inl (inl k<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<k)
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) | inl (inr k<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<k)
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) | inr p = refl
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inr k<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) min<k k<min))
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inr min=k rewrite min=k = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<k)
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) with TotalOrder.totality keyOrder min k
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inl (inl _) = lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} k v m
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inl (inr k<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) min<k k<min))
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inr min=k rewrite min=k = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<k)
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m | inl (inr k<min) with TotalOrder.totality keyOrder k k
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m | inl (inr k<min) | inl (inl k<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<k)
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m | inl (inr k<min) | inl (inr k<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<k)
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m | inl (inr k<min) | inr p = refl
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m | inr min=k with TotalOrder.totality keyOrder k k
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m | inr min=k | inl (inl k<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<k)
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m | inr min=k | inl (inr k<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<k)
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m | inr min=k | inr p with TotalOrder.totality keyOrder min k
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m | inr min=k | inr p | inl (inl min<k) rewrite min=k = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<k)
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m | inr min=k | inr p | inl (inr k<min) rewrite min=k = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<min)
-lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {.k} k v record { firstEntry = firstEntry ; next = next } | inr refl | inr p | inr s = refl
+lookupReducedSucceedsAfterAdd : {min : keySet} → (k : keySet) → (v : valueSet) → (m : ReducedMap min) → (lookupReduced (addReducedMap k v m) k ≡ yes v)
+lookupReducedSucceedsAfterAdd {min} k v m with TotalOrder.totality keyOrder min k
+lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) with TotalOrder.totality keyOrder min k
+lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) with TotalOrder.totality keyOrder k k
+lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) | inl (inl k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
+lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) | inl (inr k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
+lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) | inr p = refl
+lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inr k<min) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder min<k k<min))
+lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inr min=k rewrite min=k = exFalso (TotalOrder.irreflexive keyOrder min<k)
+lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) with TotalOrder.totality keyOrder min k
+lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inl (inl _) = lookupReducedSucceedsAfterAdd k v m
+lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inl (inr k<min) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder min<k k<min))
+lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inr min=k rewrite min=k = exFalso (TotalOrder.irreflexive keyOrder min<k)
+lookupReducedSucceedsAfterAdd {min} k v m | inl (inr k<min) with TotalOrder.totality keyOrder k k
+lookupReducedSucceedsAfterAdd {min} k v m | inl (inr k<min) | inl (inl k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
+lookupReducedSucceedsAfterAdd {min} k v m | inl (inr k<min) | inl (inr k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
+lookupReducedSucceedsAfterAdd {min} k v m | inl (inr k<min) | inr p = refl
+lookupReducedSucceedsAfterAdd {min} k v m | inr min=k with TotalOrder.totality keyOrder k k
+lookupReducedSucceedsAfterAdd {min} k v m | inr min=k | inl (inl k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
+lookupReducedSucceedsAfterAdd {min} k v m | inr min=k | inl (inr k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
+lookupReducedSucceedsAfterAdd {min} k v m | inr min=k | inr p with TotalOrder.totality keyOrder min k
+lookupReducedSucceedsAfterAdd {min} k v m | inr min=k | inr p | inl (inl min<k) rewrite min=k = exFalso (TotalOrder.irreflexive keyOrder min<k)
+lookupReducedSucceedsAfterAdd {min} k v m | inr min=k | inr p | inl (inr k<min) rewrite min=k = exFalso (TotalOrder.irreflexive keyOrder k<min)
+lookupReducedSucceedsAfterAdd {.k} k v record { firstEntry = firstEntry ; next = next } | inr refl | inr p | inr s = refl
 
-lookupReducedSucceedsAfterUnrelatedAdd : {a b c : _} → {keys : Set a} → {values : Set b} → {keyOrder : TotalOrder {_} {c} keys} → {min : keys} → (unrelatedK : keys) → (unrelatedV : values) → (k : keys) → (v : values) → ((TotalOrder._<_ keyOrder unrelatedK k) || (TotalOrder._<_ keyOrder k unrelatedK)) → (m : ReducedMap keys values keyOrder min) → (lookupReduced m k ≡ yes v) → lookupReduced (addReducedMap unrelatedK unrelatedV m) k ≡ yes v
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m lookupReducedSucceeds with TotalOrder.totality keyOrder min k'
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m lookupReducedSucceeds | inl (inl min<k') with TotalOrder.totality keyOrder min k
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr record { firstEntry = firstEntry ; next = no } () | inl (inl min<k') | inl (inl min<k)
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedSucceeds | inl (inl min<k') | inl (inl min<k) = lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {a} k' v' k v pr fst lookupReducedSucceeds
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inl min<k') | inl (inr k<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<min (PartialOrder.<Transitive (TotalOrder.order keyOrder) min<k' x)))
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr k<k') m () | inl (inl min<k') | inl (inr k<min)
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {.min} k' v' min v (inl x) m lookupReducedSucceeds | inl (inl min<k') | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) x min<k'))
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {.min} k' v' min v (inr x) record { firstEntry = v2 ; next = no } p | inl (inl min<k') | inr refl = applyEquality yes (yesInjective p)
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {.min} k' v' min v (inr x) record { firstEntry = .v ; next = (yes (a , b)) } refl | inl (inl min<k') | inr refl = applyEquality yes refl
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) with TotalOrder.totality keyOrder k' k
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) | inl (inl k'<k) with TotalOrder.totality keyOrder min k
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) | inl (inl k'<k) | inl (inl min<k) = lookupReducedSucceeds
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m () | inl (inr k'<min) | inl (inl k'<k) | inl (inr k<min)
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) | inl (inl k'<k) | inr refl = lookupReducedSucceeds
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) x k<k'))
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr x) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') with TotalOrder.totality keyOrder min k
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr _) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') | inl (inl x) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) x (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<k' k'<min)))
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr _) m () | inl (inr k'<min) | inl (inr k<k') | inl (inr x)
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr _) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') | inr x rewrite x = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<k' k'<min))
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inr k'<min) | inr k'=k rewrite k'=k = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr x) m lookupReducedSucceeds | inl (inr k'<min) | inr k'=k rewrite k'=k = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m lookupReducedSucceeds | inr refl with TotalOrder.totality keyOrder min k
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {k'} k' v' k v (inl _) record { firstEntry = firstEntry ; next = no } () | inr refl | inl (inl min<k)
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {k'} k' v' k v (inl _) record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedSucceeds | inr refl | inl (inl min<k) = lookupReducedSucceeds
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {k'} k' v' k v (inr x) m lookupReducedSucceeds | inr refl | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) min<k x))
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {k'} k' v' k v (inl x) m () | inr refl | inl (inr k<min)
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {k'} k' v' k v (inr x) m () | inr refl | inl (inr k<min)
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {.min} .min v' min v (inl x) m lookupReducedSucceeds | inr refl | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
-lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {.min} .min v' min v (inr x) m lookupReducedSucceeds | inr refl | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
+lookupReducedSucceedsAfterUnrelatedAdd : {min : keySet} → (unrelatedK : keySet) → (unrelatedV : valueSet) → (k : keySet) → (v : valueSet) → ((TotalOrder._<_ keyOrder unrelatedK k) || (TotalOrder._<_ keyOrder k unrelatedK)) → (m : ReducedMap min) → (lookupReduced m k ≡ yes v) → lookupReduced (addReducedMap unrelatedK unrelatedV m) k ≡ yes v
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds with TotalOrder.totality keyOrder min k'
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds | inl (inl min<k') with TotalOrder.totality keyOrder min k
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr record { firstEntry = firstEntry ; next = no } () | inl (inl min<k') | inl (inl min<k)
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedSucceeds | inl (inl min<k') | inl (inl min<k) = lookupReducedSucceedsAfterUnrelatedAdd {a} k' v' k v pr fst lookupReducedSucceeds
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inl min<k') | inl (inr k<min) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k<min (TotalOrder.<Transitive keyOrder min<k' x)))
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inr k<k') m () | inl (inl min<k') | inl (inr k<min)
+lookupReducedSucceedsAfterUnrelatedAdd {.min} k' v' min v (inl x) m lookupReducedSucceeds | inl (inl min<k') | inr refl = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder x min<k'))
+lookupReducedSucceedsAfterUnrelatedAdd {.min} k' v' min v (inr x) record { firstEntry = v2 ; next = no } p | inl (inl min<k') | inr refl = applyEquality yes (yesInjective p)
+lookupReducedSucceedsAfterUnrelatedAdd {.min} k' v' min v (inr x) record { firstEntry = .v ; next = (yes (a , b)) } refl | inl (inl min<k') | inr refl = applyEquality yes refl
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) with TotalOrder.totality keyOrder k' k
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) | inl (inl k'<k) with TotalOrder.totality keyOrder min k
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) | inl (inl k'<k) | inl (inl min<k) = lookupReducedSucceeds
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m () | inl (inr k'<min) | inl (inl k'<k) | inl (inr k<min)
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) | inl (inl k'<k) | inr refl = lookupReducedSucceeds
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder x k<k'))
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inr x) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') with TotalOrder.totality keyOrder min k
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inr _) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') | inl (inl x) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder x (TotalOrder.<Transitive keyOrder k<k' k'<min)))
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inr _) m () | inl (inr k'<min) | inl (inr k<k') | inl (inr x)
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inr _) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') | inr x rewrite x = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k<k' k'<min))
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inr k'<min) | inr k'=k rewrite k'=k = exFalso (TotalOrder.irreflexive keyOrder x)
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inr x) m lookupReducedSucceeds | inl (inr k'<min) | inr k'=k rewrite k'=k = exFalso (TotalOrder.irreflexive keyOrder x)
+lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds | inr refl with TotalOrder.totality keyOrder min k
+lookupReducedSucceedsAfterUnrelatedAdd {k'} k' v' k v (inl _) record { firstEntry = firstEntry ; next = no } () | inr refl | inl (inl min<k)
+lookupReducedSucceedsAfterUnrelatedAdd {k'} k' v' k v (inl _) record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedSucceeds | inr refl | inl (inl min<k) = lookupReducedSucceeds
+lookupReducedSucceedsAfterUnrelatedAdd {k'} k' v' k v (inr x) m lookupReducedSucceeds | inr refl | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder min<k x))
+lookupReducedSucceedsAfterUnrelatedAdd {k'} k' v' k v (inl x) m () | inr refl | inl (inr k<min)
+lookupReducedSucceedsAfterUnrelatedAdd {k'} k' v' k v (inr x) m () | inr refl | inl (inr k<min)
+lookupReducedSucceedsAfterUnrelatedAdd {.min} .min v' min v (inl x) m lookupReducedSucceeds | inr refl | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
+lookupReducedSucceedsAfterUnrelatedAdd {.min} .min v' min v (inr x) m lookupReducedSucceeds | inr refl | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
 
-lookupReducedFailsAfterUnrelatedAdd : {a b c : _} → {keys : Set a} → {values : Set b} → {keyOrder : TotalOrder {_} {c} keys} → {min : keys} → (unrelatedK : keys) → (unrelatedV : values) → (k : keys) → ((TotalOrder._<_ keyOrder unrelatedK k) || (TotalOrder._<_ keyOrder k unrelatedK)) → (m : ReducedMap keys values keyOrder min) → (lookupReduced m k ≡ no) → lookupReduced (addReducedMap unrelatedK unrelatedV m) k ≡ no
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr m lookupReducedFails with TotalOrder.totality keyOrder min k'
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr m lookupReducedFails | inl (inl min<k') with TotalOrder.totality keyOrder min k
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) with TotalOrder.totality keyOrder k' k
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) | inl (inl x) = refl
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) | inl (inr x) = refl
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .k v' k (inl x) record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .k v' k (inr x) record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedFails | inl (inl min<k') | inl (inl min<k) = lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} k' v' k pr fst lookupReducedFails
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr m lookupReducedFails | inl (inl min<k') | inl (inr k<min) = refl
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {.min} k' v' min pr m () | inl (inl min<k') | inr refl
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr m lookupReducedFails | inl (inr k'<min) with TotalOrder.totality keyOrder min k
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) with TotalOrder.totality keyOrder k' k
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) with TotalOrder.totality keyOrder min k
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inl x₁) record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inl _) = refl
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inl x₁) record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inl _) = lookupReducedFails
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inr x₁) record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inl _) = refl
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inr x₁) record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inl _) = lookupReducedFails
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inr x) = refl
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<k)
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inr k<k') = refl
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .k v' k (inl x) record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .k v' k (inr x) record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) with TotalOrder.totality keyOrder k' k
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) with TotalOrder.totality keyOrder min k
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<min min<k))
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inl (inr k<min') = refl
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<min)
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inr x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k'<k x))
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inr k<k') = refl
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .k v' k (inl x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .k v' k (inr x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr m () | inl (inr k'<min) | inr min=k
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .min v' k pr m lookupReducedFails | inr refl with TotalOrder.totality keyOrder min k
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .min v' k pr record { firstEntry = firstEntry ; next = no } lookupReducedFails | inr refl | inl (inl min<k) = refl
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .min v' k pr record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedFails | inr refl | inl (inl min<k) = lookupReducedFails
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .min v' k pr m lookupReducedFails | inr refl | inl (inr k<min) = refl
-lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .min v' k pr m () | inr refl | inr min=k
+lookupReducedFailsAfterUnrelatedAdd : {min : keySet} → (unrelatedK : keySet) → (unrelatedV : valueSet) → (k : keySet) → ((TotalOrder._<_ keyOrder unrelatedK k) || (TotalOrder._<_ keyOrder k unrelatedK)) → (m : ReducedMap min) → (lookupReduced m k ≡ no) → lookupReduced (addReducedMap unrelatedK unrelatedV m) k ≡ no
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m lookupReducedFails with TotalOrder.totality keyOrder min k'
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m lookupReducedFails | inl (inl min<k') with TotalOrder.totality keyOrder min k
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) with TotalOrder.totality keyOrder k' k
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) | inl (inl x) = refl
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) | inl (inr x) = refl
+lookupReducedFailsAfterUnrelatedAdd {min} .k v' k (inl x) record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
+lookupReducedFailsAfterUnrelatedAdd {min} .k v' k (inr x) record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedFails | inl (inl min<k') | inl (inl min<k) = lookupReducedFailsAfterUnrelatedAdd k' v' k pr fst lookupReducedFails
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m lookupReducedFails | inl (inl min<k') | inl (inr k<min) = refl
+lookupReducedFailsAfterUnrelatedAdd {.min} k' v' min pr m () | inl (inl min<k') | inr refl
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m lookupReducedFails | inl (inr k'<min) with TotalOrder.totality keyOrder min k
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) with TotalOrder.totality keyOrder k' k
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) with TotalOrder.totality keyOrder min k
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inl x₁) record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inl _) = refl
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inl x₁) record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inl _) = lookupReducedFails
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inr x₁) record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inl _) = refl
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inr x₁) record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inl _) = lookupReducedFails
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inr x) = refl
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder min<k)
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inr k<k') = refl
+lookupReducedFailsAfterUnrelatedAdd {min} .k v' k (inl x) record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
+lookupReducedFailsAfterUnrelatedAdd {min} .k v' k (inr x) record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) with TotalOrder.totality keyOrder k' k
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) with TotalOrder.totality keyOrder min k
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k<min min<k))
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inl (inr k<min') = refl
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder k<min)
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inr x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k'<k x))
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inr k<k') = refl
+lookupReducedFailsAfterUnrelatedAdd {min} .k v' k (inl x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
+lookupReducedFailsAfterUnrelatedAdd {min} .k v' k (inr x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
+lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m () | inl (inr k'<min) | inr min=k
+lookupReducedFailsAfterUnrelatedAdd {min} .min v' k pr m lookupReducedFails | inr refl with TotalOrder.totality keyOrder min k
+lookupReducedFailsAfterUnrelatedAdd {min} .min v' k pr record { firstEntry = firstEntry ; next = no } lookupReducedFails | inr refl | inl (inl min<k) = refl
+lookupReducedFailsAfterUnrelatedAdd {min} .min v' k pr record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedFails | inr refl | inl (inl min<k) = lookupReducedFails
+lookupReducedFailsAfterUnrelatedAdd {min} .min v' k pr m lookupReducedFails | inr refl | inl (inr k<min) = refl
+lookupReducedFailsAfterUnrelatedAdd {min} .min v' k pr m () | inr refl | inr min=k
 
-countReducedBehavesWhenAddingNotPresent : {a b c : _} {keys : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keys} {min : keys} → (k : keys) → (v : values) → (m : ReducedMap keys values keyOrder min) → (lookupReduced {keyOrder = keyOrder} m k ≡ no) → countReduced (addReducedMap k v m) ≡ succ (countReduced m)
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v m lookupReducedFails with TotalOrder.totality keyOrder k min
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) with TotalOrder.totality keyOrder min k
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) min<k k<min))
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inl (inr _) = refl
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<min)
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) with TotalOrder.totality keyOrder min k
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inr min<k) | inl (inl _) = refl
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedFails | inl (inr min<k) | inl (inl _) = applyEquality succ (countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} k v (_&&_.fst b) lookupReducedFails)
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) | inl (inr k<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) min<k k<min))
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<k)
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v m lookupReducedFails | inr refl with TotalOrder.totality keyOrder min min
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {k} k v m lookupReducedFails | inr refl | inl (inl min<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<min)
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {k} k v m lookupReducedFails | inr refl | inl (inr min<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<min)
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {k} k v record { firstEntry = firstEntry ; next = no } () | inr refl | inr p
-countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {k} k v record { firstEntry = firstEntry ; next = (yes x) } () | inr refl | inr p
+countReducedBehavesWhenAddingNotPresent : {min : keySet} → (k : keySet) → (v : valueSet) → (m : ReducedMap min) → (lookupReduced m k ≡ no) → countReduced (addReducedMap k v m) ≡ succ (countReduced m)
+countReducedBehavesWhenAddingNotPresent {min} k v m lookupReducedFails with TotalOrder.totality keyOrder k min
+countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) with TotalOrder.totality keyOrder min k
+countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder min<k k<min))
+countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inl (inr _) = refl
+countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inr refl = exFalso (TotalOrder.irreflexive keyOrder k<min)
+countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) with TotalOrder.totality keyOrder min k
+countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inr min<k) | inl (inl _) = refl
+countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedFails | inl (inr min<k) | inl (inl _) = applyEquality succ (countReducedBehavesWhenAddingNotPresent k v (_&&_.fst b) lookupReducedFails)
+countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) | inl (inr k<min) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder min<k k<min))
+countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder min<k)
+countReducedBehavesWhenAddingNotPresent {min} k v m lookupReducedFails | inr refl with TotalOrder.totality keyOrder min min
+countReducedBehavesWhenAddingNotPresent {k} k v m lookupReducedFails | inr refl | inl (inl min<min) = exFalso (TotalOrder.irreflexive keyOrder min<min)
+countReducedBehavesWhenAddingNotPresent {k} k v m lookupReducedFails | inr refl | inl (inr min<min) = exFalso (TotalOrder.irreflexive keyOrder min<min)
+countReducedBehavesWhenAddingNotPresent {k} k v record { firstEntry = firstEntry ; next = no } () | inr refl | inr p
+countReducedBehavesWhenAddingNotPresent {k} k v record { firstEntry = firstEntry ; next = (yes x) } () | inr refl | inr p
 
-countReducedBehavesWhenAddingPresent : {a b c : _} {keys : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keys} {min : keys} → (k : keys) → (v v' : values) → (m : ReducedMap keys values keyOrder min) → (lookupReduced {keyOrder = keyOrder} m k ≡ yes v') → countReduced (addReducedMap k v m) ≡ countReduced m
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds with TotalOrder.totality keyOrder k min
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inl (inl k<min) with TotalOrder.totality keyOrder min k
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inl (inl k<min) | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<min min<k))
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m () | inl (inl k<min) | inl (inr _)
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inl (inl k<min) | inr q = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (identityOfIndiscernablesLeft (TotalOrder._<_ keyOrder) k<min (equalityCommutative q)))
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inl (inr min<k) with TotalOrder.totality keyOrder min k
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' record { firstEntry = firstEntry ; next = no } () | inl (inr min<k) | inl (inl _)
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedSucceeds | inl (inr min<k) | inl (inl _) = applyEquality succ (countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} k v v' fst lookupReducedSucceeds)
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m () | inl (inr min<k) | inl (inr k<min)
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inl (inr min<k) | inr q = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (identityOfIndiscernablesLeft (λ a b → TotalOrder._<_ keyOrder a b) min<k q))
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inr q with TotalOrder.totality keyOrder min min
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inr q | inl (inl x) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inr q | inl (inr x) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
-countReducedBehavesWhenAddingPresent {keys = keys} {keyOrder = keyOrder} {min} k v v' record { firstEntry = firstEntry ; next = no } lookupReducedSucceeds | inr _ | inr p with TotalOrder.totality keyOrder min k
-countReducedBehavesWhenAddingPresent {keys = keys} {keyOrder = keyOrder} {min} k v v' record { firstEntry = firstEntry ; next = no } () | inr _ | inr p | inl (inl x)
-countReducedBehavesWhenAddingPresent {keys = keys} {keyOrder = keyOrder} {min} k v v' record { firstEntry = firstEntry ; next = no } () | inr _ | inr p | inl (inr x`)
-countReducedBehavesWhenAddingPresent {keys = keys} {keyOrder = keyOrder} {.k} k v v' record { firstEntry = firstEntry ; next = no } lookupReducedSucceeds | inr q | inr p | inr refl = refl
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedSucceeds | inr q | inr p with TotalOrder.totality keyOrder k k
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedSucceeds | inr q | inr p | inl (inl x) = exFalso (TotalOrder.irreflexive keyOrder x)
-countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedSucceeds | inr q | inr p | inl (inr x) = exFalso (TotalOrder.irreflexive keyOrder x)
-countReducedBehavesWhenAddingPresent {keys = keys} {values = values} {keyOrder = keyOrder} {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , (m ,, pr))) } q | inr q1 | inr p | inr x with TotalOrder.totality keyOrder min k
-countReducedBehavesWhenAddingPresent {keys = keys} {values} {keyOrder} {.k} k v v' record { firstEntry = firstEntry ; next = (yes (a , (m ,, pr))) } q | inr refl | inr p | inr x | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder min<k)
-countReducedBehavesWhenAddingPresent {keys = keys} {values} {keyOrder} {.k} k v v' record { firstEntry = firstEntry ; next = (yes (a , (m ,, pr))) } q | inr q1 | inr p | inr x | inr refl = refl
+countReducedBehavesWhenAddingPresent : {min : keySet} → (k : keySet) → (v v' : valueSet) → (m : ReducedMap min) → (lookupReduced m k ≡ yes v') → countReduced (addReducedMap k v m) ≡ countReduced m
+countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds with TotalOrder.totality keyOrder k min
+countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inl (inl k<min) with TotalOrder.totality keyOrder min k
+countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inl (inl k<min) | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k<min min<k))
+countReducedBehavesWhenAddingPresent {min} k v v' m () | inl (inl k<min) | inl (inr _)
+countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inl (inl k<min) | inr q = exFalso (TotalOrder.irreflexive keyOrder (identityOfIndiscernablesLeft (TotalOrder._<_ keyOrder) k<min (equalityCommutative q)))
+countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inl (inr min<k) with TotalOrder.totality keyOrder min k
+countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = no } () | inl (inr min<k) | inl (inl _)
+countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedSucceeds | inl (inr min<k) | inl (inl _) = applyEquality succ (countReducedBehavesWhenAddingPresent k v v' fst lookupReducedSucceeds)
+countReducedBehavesWhenAddingPresent {min} k v v' m () | inl (inr min<k) | inl (inr k<min)
+countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inl (inr min<k) | inr q = exFalso (TotalOrder.irreflexive keyOrder (identityOfIndiscernablesLeft (λ a b → TotalOrder._<_ keyOrder a b) min<k q))
+countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inr q with TotalOrder.totality keyOrder min min
+countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inr q | inl (inl x) = exFalso (TotalOrder.irreflexive keyOrder x)
+countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inr q | inl (inr x) = exFalso (TotalOrder.irreflexive keyOrder x)
+countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = no } lookupReducedSucceeds | inr _ | inr p with TotalOrder.totality keyOrder min k
+countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = no } () | inr _ | inr p | inl (inl x)
+countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = no } () | inr _ | inr p | inl (inr x`)
+countReducedBehavesWhenAddingPresent {.k} k v v' record { firstEntry = firstEntry ; next = no } lookupReducedSucceeds | inr q | inr p | inr refl = refl
+countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedSucceeds | inr q | inr p with TotalOrder.totality keyOrder k k
+countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedSucceeds | inr q | inr p | inl (inl x) = exFalso (TotalOrder.irreflexive keyOrder x)
+countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedSucceeds | inr q | inr p | inl (inr x) = exFalso (TotalOrder.irreflexive keyOrder x)
+countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , (m ,, pr))) } q | inr q1 | inr p | inr x with TotalOrder.totality keyOrder min k
+countReducedBehavesWhenAddingPresent {.k} k v v' record { firstEntry = firstEntry ; next = (yes (a , (m ,, pr))) } q | inr refl | inr p | inr x | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder min<k)
+countReducedBehavesWhenAddingPresent {.k} k v v' record { firstEntry = firstEntry ; next = (yes (a , (m ,, pr))) } q | inr q1 | inr p | inr x | inr refl = refl
 
-data Map {a b c : _} (keys : Set a) (values : Set b) (keyOrder : TotalOrder {_} {c} keys) : Set (a ⊔ b ⊔ c) where
-  empty : Map keys values keyOrder
-  nonempty : {min : keys} → ReducedMap keys values keyOrder min → Map keys values keyOrder
+data Map : Set (a ⊔ b ⊔ c) where
+  empty : Map
+  nonempty : {min : keySet} → ReducedMap min → Map
 
-addMap : {a b c : _} → {keys : Set a} → {values : Set b} → {keyOrder : TotalOrder {_} {c} keys} → (m : Map keys values keyOrder) → (k : keys) → (v : values) → Map keys values keyOrder
+addMap : (m : Map) → (k : keySet) → (v : valueSet) → Map
 addMap empty k v = nonempty {min = k} record { firstEntry = v ; next = no }
-addMap {keys = keys} {values} {keyOrder} (nonempty x) k v = nonempty (addReducedMap {keys = keys} {values} {keyOrder} k v x)
+addMap (nonempty x) k v = nonempty (addReducedMap k v x)
 
-lookup : {a b c : _} → {keys : Set a} → {values : Set b} → {keyOrder : TotalOrder {_} {c} keys} → (m : Map keys values keyOrder) → (target : keys) → Maybe values
-lookup {keyOrder = keyOrder} empty t = no
-lookup {keyOrder = keyOrder} (nonempty x) t = lookupReduced x t
+lookup : (m : Map) → (target : keySet) → Maybe valueSet
+lookup empty t = no
+lookup (nonempty x) t = lookupReduced x t
 
-count : {a b c : _} {keys : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keys} → (m : Map keys values keyOrder) → ℕ
-count {keyOrder = keyOrder} empty = 0
-count {keyOrder = keyOrder} (nonempty x) = countReduced x
+count : (m : Map) → ℕ
+count empty = 0
+count (nonempty x) = countReduced x
 
-keysReduced : {a b c : _} {keyDom : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keyDom} {min : keyDom} → (m : ReducedMap keyDom values keyOrder min) → Vec keyDom (countReduced m)
+keysReduced : {min : keySet} → (m : ReducedMap min) → Vec keySet (countReduced m)
 keysReduced {min = min} record { firstEntry = firstEntry ; next = no } = min ,- []
 keysReduced {min = min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } = min ,- (keysReduced fst)
 
-keys : {a b c : _} {keyDom : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keyDom} → (m : Map keyDom values keyOrder) → Vec keyDom (count m)
+keys : (m : Map) → Vec keySet (count m)
 keys empty = []
 keys (nonempty m) = keysReduced m
 
-lookupReducedWhenLess : {a b c : _} {keyDom : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keyDom} {min : keyDom} → (m : ReducedMap keyDom values keyOrder min) → (k : keyDom) → (TotalOrder._<_ keyOrder k min) → (lookupReduced m k ≡ no)
-lookupReducedWhenLess {keyOrder = keyOrder} {min} m k k<min with TotalOrder.totality keyOrder min k
-lookupReducedWhenLess {keyOrder = keyOrder} {min} m k k<min | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<min min<k))
-lookupReducedWhenLess {keyOrder = keyOrder} {min} m k k<min | inl (inr _) = refl
-lookupReducedWhenLess {keyOrder = keyOrder} {min} m k k<min | inr min=k rewrite min=k = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<min)
+lookupReducedWhenLess : {min : keySet} → (m : ReducedMap min) → (k : keySet) → (TotalOrder._<_ keyOrder k min) → (lookupReduced m k ≡ no)
+lookupReducedWhenLess {min} m k k<min with TotalOrder.totality keyOrder min k
+lookupReducedWhenLess {min} m k k<min | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k<min min<k))
+lookupReducedWhenLess {min} m k k<min | inl (inr _) = refl
+lookupReducedWhenLess {min} m k k<min | inr min=k rewrite min=k = exFalso (TotalOrder.irreflexive keyOrder k<min)
 
-lookupCertainReduced : {a b c : _} {keyDom : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keyDom} {min : keyDom} → (m : ReducedMap keyDom values keyOrder min) → (k : keyDom) → (vecContains (keysReduced m) k) → Sg values (λ v → lookupReduced m k ≡ yes v)
-lookupCertainReduced {keyDom = keyDom} {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = no } k pr = firstEntry , q
+lookupCertainReduced : {min : keySet} → (m : ReducedMap min) → (k : keySet) → (vecContains (keysReduced m) k) → Sg valueSet (λ v → lookupReduced m k ≡ yes v)
+lookupCertainReduced {min} record { firstEntry = firstEntry ; next = no } k pr = firstEntry , q
   where
     t : min ≡ k
     t = vecSolelyContains k pr
-    q : lookupReduced {keys = keyDom} {keyOrder = keyOrder} {min} (record { firstEntry = firstEntry ; next = no }) k ≡ yes firstEntry
+    q : lookupReduced {min} (record { firstEntry = firstEntry ; next = no }) k ≡ yes firstEntry
     q with TotalOrder.totality keyOrder k k
-    q | inl (inl k<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<k)
-    q | inl (inr k<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<k)
+    q | inl (inl k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
+    q | inl (inr k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
     q | inr p with TotalOrder.totality keyOrder min k
-    q | inr p | inl (inl min<k) rewrite t = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<k)
-    q | inr p | inl (inr k<min) rewrite t = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<min)
+    q | inr p | inl (inl min<k) rewrite t = exFalso (TotalOrder.irreflexive keyOrder min<k)
+    q | inr p | inl (inr k<min) rewrite t = exFalso (TotalOrder.irreflexive keyOrder k<min)
     q | inr p | inr x = refl
-lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k pr with TotalOrder.totality keyOrder min k
-lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = zero ; index<m = _ ; isHere = isHere } | inl (inl min<k) rewrite isHere = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<k)
-lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inl min<k) = lookupCertainReduced {keyOrder = keyOrder} fst k record { index = index ; index<m = canRemoveSuccFrom<N index<m ; isHere = isHere }
-lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = zero ; index<m = _ ; isHere = isHere } | inl (inr k<min) rewrite isHere = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<min)
-lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) with TotalOrder.totality keyOrder a k
-lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inl (inl a<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<min (PartialOrder.<Transitive (TotalOrder.order keyOrder) snd a<k)))
-lookupCertainReduced {values = values} {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inl (inr k<a) = exFalso h
+lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k pr with TotalOrder.totality keyOrder min k
+lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = zero ; index<m = _ ; isHere = isHere } | inl (inl min<k) rewrite isHere = exFalso (TotalOrder.irreflexive keyOrder min<k)
+lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inl min<k) = lookupCertainReduced fst k record { index = index ; index<m = canRemoveSuccFrom<N index<m ; isHere = isHere }
+lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = zero ; index<m = _ ; isHere = isHere } | inl (inr k<min) rewrite isHere = exFalso (TotalOrder.irreflexive keyOrder k<min)
+lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) with TotalOrder.totality keyOrder a k
+lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inl (inl a<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k<min (TotalOrder.<Transitive keyOrder snd a<k)))
+lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inl (inr k<a) = exFalso h
   where
-    f : Sg values (λ v → lookupReduced fst k ≡ yes v)
-    f = lookupCertainReduced {keyOrder = keyOrder} fst k record { index = index ; index<m = canRemoveSuccFrom<N index<m ; isHere = isHere }
+    f : Sg valueSet (λ v → lookupReduced fst k ≡ yes v)
+    f = lookupCertainReduced fst k record { index = index ; index<m = canRemoveSuccFrom<N index<m ; isHere = isHere }
     g : lookupReduced fst k ≡ no
     g = lookupReducedWhenLess fst k k<a
     noIsNotYes : {a : _} → {A : Set a} → {b : A} → (no ≡ yes b) → False
@@ -233,9 +234,9 @@ lookupCertainReduced {values = values} {keyOrder = keyOrder} {min} record { firs
     h : False
     h with f
     h | a , b rewrite g = noIsNotYes b
-lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) snd k<min))
-lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k pr | inr min=k = firstEntry , refl
+lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inr refl = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder snd k<min))
+lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k pr | inr min=k = firstEntry , refl
 
-lookupCertain : {a b c : _} {keyDom : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keyDom} → (m : Map keyDom values keyOrder) → (k : keyDom) → (vecContains (keys m) k) → Sg values (λ v → lookup m k ≡ yes v)
-lookupCertain {keyOrder = keyOrder} empty k record { index = index ; index<m = (le x ()) ; isHere = isHere }
-lookupCertain {keyOrder = keyOrder} (nonempty {min} m) k pr = lookupCertainReduced {keyOrder = keyOrder} {min} m k pr
+lookupCertain : (m : Map) → (k : keySet) → (vecContains (keys m) k) → Sg valueSet (λ v → lookup m k ≡ yes v)
+lookupCertain empty k record { index = index ; index<m = (le x ()) ; isHere = isHere }
+lookupCertain (nonempty {min} m) k pr = lookupCertainReduced {min} m k pr
diff --git a/Numbers/BinaryNaturals/Addition.agda b/Numbers/BinaryNaturals/Addition.agda
index e341706..2ebc597 100644
--- a/Numbers/BinaryNaturals/Addition.agda
+++ b/Numbers/BinaryNaturals/Addition.agda
@@ -9,7 +9,7 @@ open import Numbers.Naturals.Order
 open import Groups.Definition
 open import Numbers.BinaryNaturals.Definition
 open import Semirings.Definition
-open import Orders
+open import Orders.Total.Definition
 
 module Numbers.BinaryNaturals.Addition where
 
diff --git a/Numbers/BinaryNaturals/Definition.agda b/Numbers/BinaryNaturals/Definition.agda
index 8bcf49e..875096b 100644
--- a/Numbers/BinaryNaturals/Definition.agda
+++ b/Numbers/BinaryNaturals/Definition.agda
@@ -8,7 +8,7 @@ open import Numbers.Naturals.Order
 open import Numbers.Naturals.Definition
 open import Groups.Definition
 open import Semirings.Definition
-open import Orders
+open import Orders.Total.Definition
 
 module Numbers.BinaryNaturals.Definition where
 
diff --git a/Numbers/BinaryNaturals/Order.agda b/Numbers/BinaryNaturals/Order.agda
index 76d5c7c..e3e0072 100644
--- a/Numbers/BinaryNaturals/Order.agda
+++ b/Numbers/BinaryNaturals/Order.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --warning=error --safe --without-K #-}
 
-open import WellFoundedInduction
+open import Orders.WellFounded.Induction
 open import LogicalFormulae
 open import Functions
 open import Lists.Lists
@@ -9,7 +9,7 @@ open import Numbers.Naturals.Order.Lemmas
 open import Numbers.Naturals.Semiring
 open import Groups.Definition
 open import Numbers.BinaryNaturals.Definition
-open import Orders
+open import Orders.Total.Definition
 open import Semirings.Definition
 
 module Numbers.BinaryNaturals.Order where
@@ -288,25 +288,25 @@ module Numbers.BinaryNaturals.Order where
   chopDouble a b i with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
   chopDouble a b zero | inl (inl a<b) with TotalOrder.totality ℕTotalOrder (2 *N binNatToN a) (2 *N binNatToN b)
   chopDouble a b zero | inl (inl a<b) | inl (inl x) = refl
-  chopDouble a b zero | inl (inl a<b) | inl (inr b<a) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) b<a (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl))))
-  chopDouble a b zero | inl (inl a<b) | inr a=b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) a=b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) a<b)
+  chopDouble a b zero | inl (inl a<b) | inl (inr b<a) = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder b<a (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl))))
+  chopDouble a b zero | inl (inl a<b) | inr a=b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) a=b = exFalso (TotalOrder.irreflexive ℕTotalOrder a<b)
   chopDouble a b one | inl (inl a<b) with TotalOrder.totality ℕTotalOrder (2 *N binNatToN a) (2 *N binNatToN b)
   chopDouble a b one | inl (inl a<b) | inl (inl 2a<2b) = refl
-  chopDouble a b one | inl (inl a<b) | inl (inr 2b<2a) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) a<b (cancelInequalityLeft {2} 2b<2a)))
-  chopDouble a b one | inl (inl a<b) | inr 2a=2b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) 2a=2b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) a<b)
+  chopDouble a b one | inl (inl a<b) | inl (inr 2b<2a) = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive (ℕTotalOrder) a<b (cancelInequalityLeft {2} 2b<2a)))
+  chopDouble a b one | inl (inl a<b) | inr 2a=2b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) 2a=2b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) a<b)
   chopDouble a b zero | inl (inr b<a) with TotalOrder.totality ℕTotalOrder (2 *N binNatToN a) (2 *N binNatToN b)
-  chopDouble a b zero | inl (inr b<a) | inl (inl 2a<2b) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) b<a (cancelInequalityLeft {2} {binNatToN a} {binNatToN b} 2a<2b)))
+  chopDouble a b zero | inl (inr b<a) | inl (inl 2a<2b) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) b<a (cancelInequalityLeft {2} {binNatToN a} {binNatToN b} 2a<2b)))
   chopDouble a b zero | inl (inr b<a) | inl (inr 2b<2a) = refl
-  chopDouble a b zero | inl (inr b<a) | inr 2a=2b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) 2a=2b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) b<a)
+  chopDouble a b zero | inl (inr b<a) | inr 2a=2b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) 2a=2b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) b<a)
   chopDouble a b one | inl (inr b<a) with TotalOrder.totality ℕTotalOrder (2 *N binNatToN a) (2 *N binNatToN b)
-  chopDouble a b one | inl (inr b<a) | inl (inl 2a<2b) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) b<a (cancelInequalityLeft {2} 2a<2b)))
+  chopDouble a b one | inl (inr b<a) | inl (inl 2a<2b) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) b<a (cancelInequalityLeft {2} 2a<2b)))
   chopDouble a b one | inl (inr b<a) | inl (inr x) = refl
-  chopDouble a b one | inl (inr b<a) | inr 2a=2b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) 2a=2b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) b<a)
+  chopDouble a b one | inl (inr b<a) | inr 2a=2b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) 2a=2b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) b<a)
   chopDouble a b i | inr x with TotalOrder.totality ℕTotalOrder (binNatToN (i :: a)) (binNatToN (i :: b))
-  chopDouble a b zero | inr a=b | inl (inl a<b) rewrite a=b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) a<b)
-  chopDouble a b one | inr a=b | inl (inl a<b) rewrite a=b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) a<b)
-  chopDouble a b zero | inr a=b | inl (inr b<a) rewrite a=b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) b<a)
-  chopDouble a b one | inr a=b | inl (inr b<a) rewrite a=b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) b<a)
+  chopDouble a b zero | inr a=b | inl (inl a<b) rewrite a=b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) a<b)
+  chopDouble a b one | inr a=b | inl (inl a<b) rewrite a=b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) a<b)
+  chopDouble a b zero | inr a=b | inl (inr b<a) rewrite a=b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) b<a)
+  chopDouble a b one | inr a=b | inl (inr b<a) rewrite a=b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) b<a)
   chopDouble a b i | inr a=b | inr x = refl
 
   succNotLess : {n : ℕ} → succ n <N n → False
@@ -315,12 +315,12 @@ module Numbers.BinaryNaturals.Order where
   <BIsInherited : (a b : BinNat) → a <BInherited b ≡ a <B b
   <BIsInherited [] b with TotalOrder.totality ℕTotalOrder 0 (binNatToN b)
   <BIsInherited [] b | inl (inl x) with inspect (binNatToN b)
-  <BIsInherited [] b | inl (inl x) | 0 with≡ pr rewrite binNatToNZero b pr | pr = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) x)
+  <BIsInherited [] b | inl (inl x) | 0 with≡ pr rewrite binNatToNZero b pr | pr = exFalso (TotalOrder.irreflexive (ℕTotalOrder) x)
   <BIsInherited [] b | inl (inl x) | (succ bl) with≡ pr rewrite pr = equalityCommutative (zeroLess b λ p → zeroNotSucc bl b p pr)
   <BIsInherited [] b | inr 0=b rewrite canonicalSecond [] b Equal | binNatToNZero b (equalityCommutative 0=b) = refl
   <BIsInherited (a :: as) [] with TotalOrder.totality ℕTotalOrder (binNatToN (a :: as)) 0
   <BIsInherited (a :: as) [] | inl (inr x) with inspect (binNatToN (a :: as))
-  <BIsInherited (a :: as) [] | inl (inr x) | zero with≡ pr rewrite binNatToNZero (a :: as) pr | pr = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) x)
+  <BIsInherited (a :: as) [] | inl (inr x) | zero with≡ pr rewrite binNatToNZero (a :: as) pr | pr = exFalso (TotalOrder.irreflexive (ℕTotalOrder) x)
   <BIsInherited (a :: as) [] | inl (inr x) | succ y with≡ pr rewrite pr = equalityCommutative (zeroLess' (a :: as) λ i → zeroNotSucc y (a :: as) i pr)
   <BIsInherited (a :: as) [] | inr x rewrite canonicalFirst (a :: as) [] Equal | binNatToNZero (a :: as) x = refl
   <BIsInherited (zero :: a) (zero :: b) = transitivity (chopDouble a b zero) (<BIsInherited a b)
@@ -331,21 +331,21 @@ module Numbers.BinaryNaturals.Order where
        t : a <BInherited b ≡ FirstLess
        t with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
        t | inl (inl x) = refl
-       t | inl (inr x) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) x a<b))
-       t | inr x rewrite x = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) a<b)
+       t | inl (inr x) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) x a<b))
+       t | inr x rewrite x = exFalso (TotalOrder.irreflexive (ℕTotalOrder) a<b)
        indHyp : FirstLess ≡ go<B Equal a b
        indHyp = transitivity (equalityCommutative t) (<BIsInherited a b)
   <BIsInherited (zero :: a) (one :: b) | inl (inl 2a<2b+1) | inl (inr b<a) = exFalso (noIntegersBetweenXAndSuccX {2 *N binNatToN a} (2 *N binNatToN b) (lessRespectsMultiplicationLeft (binNatToN b) (binNatToN a) 2 b<a (le 1 refl)) 2a<2b+1)
   <BIsInherited (zero :: a) (one :: b) | inl (inl 2a<2b+1) | inr a=b rewrite a=b | canonicalFirst a b FirstLess | canonicalSecond (canonical a) b FirstLess | transitivity (equalityCommutative (binToBin a)) (transitivity (applyEquality NToBinNat a=b) (binToBin b)) = equalityCommutative (lemma1 (canonical b))
   <BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
-  <BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) | inl (inl a<b) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) 2b+1<2a (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl)) (le zero refl))))
+  <BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) | inl (inl a<b) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) 2b+1<2a (TotalOrder.<Transitive (ℕTotalOrder) (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl)) (le zero refl))))
   <BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) | inl (inr b<a) = equalityCommutative (equalToFirstGreater FirstLess a b (equalityCommutative indHyp))
     where
       t : a <BInherited b ≡ FirstGreater
       t with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
-      t | inl (inl x) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) x b<a))
+      t | inl (inl x) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) x b<a))
       t | inl (inr x) = refl
-      t | inr x rewrite x = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) b<a)
+      t | inr x rewrite x = exFalso (TotalOrder.irreflexive (ℕTotalOrder) b<a)
       indHyp : FirstGreater ≡ go<B Equal a b
       indHyp = transitivity (equalityCommutative t) (<BIsInherited a b)
   <BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) | inr a=b rewrite a=b = exFalso (succNotLess 2b+1<2a)
@@ -356,12 +356,12 @@ module Numbers.BinaryNaturals.Order where
     where
       t : a <BInherited b ≡ FirstLess
       t with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
-      t | inl (inr x) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) x a<b))
+      t | inl (inr x) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) x a<b))
       t | inl (inl x) = refl
-      t | inr x rewrite x = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) a<b)
+      t | inr x rewrite x = exFalso (TotalOrder.irreflexive (ℕTotalOrder) a<b)
       indHyp : FirstLess ≡ go<B Equal a b
       indHyp = transitivity (equalityCommutative t) (<BIsInherited a b)
-  <BIsInherited (one :: a) (zero :: b) | inl (inl 2a+1<2b) | inl (inr b<a) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) 2a+1<2b (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (lessRespectsMultiplicationLeft (binNatToN b) (binNatToN a) 2 b<a (le 1 refl)) (le zero refl))))
+  <BIsInherited (one :: a) (zero :: b) | inl (inl 2a+1<2b) | inl (inr b<a) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) 2a+1<2b (TotalOrder.<Transitive (ℕTotalOrder) (lessRespectsMultiplicationLeft (binNatToN b) (binNatToN a) 2 b<a (le 1 refl)) (le zero refl))))
   <BIsInherited (one :: a) (zero :: b) | inl (inl 2a+1<2b) | inr a=b rewrite a=b = exFalso (succNotLess 2a+1<2b)
   <BIsInherited (one :: a) (zero :: b) | inl (inr 2b<2a+1) with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
   <BIsInherited (one :: a) (zero :: b) | inl (inr 2b<2a+1) | inl (inl a<b) = exFalso (noIntegersBetweenXAndSuccX {2 *N binNatToN b} (2 *N binNatToN a) (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl)) 2b<2a+1)
@@ -369,9 +369,9 @@ module Numbers.BinaryNaturals.Order where
     where
       t : a <BInherited b ≡ FirstGreater
       t with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
-      t | inl (inl x) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) x b<a))
+      t | inl (inl x) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) x b<a))
       t | inl (inr x) = refl
-      t | inr x rewrite x = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) b<a)
+      t | inr x rewrite x = exFalso (TotalOrder.irreflexive (ℕTotalOrder) b<a)
       indHyp : FirstGreater ≡ go<B Equal a b
       indHyp = transitivity (equalityCommutative t) (<BIsInherited a b)
   <BIsInherited (one :: a) (zero :: b) | inl (inr 2b<2a+1) | inr a=b rewrite a=b | canonicalFirst a b FirstGreater | canonicalSecond (canonical a) b FirstGreater | transitivity (equalityCommutative (binToBin a)) (transitivity (applyEquality NToBinNat a=b) (binToBin b)) = equalityCommutative (lemma1 (canonical b))
diff --git a/Numbers/BinaryNaturals/Subtraction.agda b/Numbers/BinaryNaturals/Subtraction.agda
index cf7eece..33cff5b 100644
--- a/Numbers/BinaryNaturals/Subtraction.agda
+++ b/Numbers/BinaryNaturals/Subtraction.agda
@@ -10,7 +10,7 @@ open import Numbers.BinaryNaturals.Addition
 open import Numbers.BinaryNaturals.SubtractionGo
 open import Numbers.BinaryNaturals.SubtractionGoPreservesCanonicalRight
 open import Numbers.BinaryNaturals.SubtractionGoPreservesCanonicalLeft
-open import Orders
+open import Orders.Total.Definition
 open import Semirings.Definition
 open import Maybe
 
diff --git a/Numbers/BinaryNaturals/SubtractionGo.agda b/Numbers/BinaryNaturals/SubtractionGo.agda
index c6095db..e6ee245 100644
--- a/Numbers/BinaryNaturals/SubtractionGo.agda
+++ b/Numbers/BinaryNaturals/SubtractionGo.agda
@@ -4,7 +4,6 @@ open import LogicalFormulae
 open import Lists.Lists
 open import Numbers.Naturals.Naturals
 open import Numbers.BinaryNaturals.Definition
-open import Orders
 open import Semirings.Definition
 open import Maybe
 
diff --git a/Numbers/Integers/Order.agda b/Numbers/Integers/Order.agda
index 536ee60..25fe328 100644
--- a/Numbers/Integers/Order.agda
+++ b/Numbers/Integers/Order.agda
@@ -13,7 +13,8 @@ open import Rings.Orders.Partial.Definition
 open import Rings.Orders.Total.Definition
 open import Setoids.Setoids
 open import Setoids.Orders
-open import Orders
+open import Orders.Total.Definition
+open import Orders.Partial.Definition
 
 module Numbers.Integers.Order where
 
diff --git a/Numbers/Integers/RingStructure/EuclideanDomain.agda b/Numbers/Integers/RingStructure/EuclideanDomain.agda
index 544c74b..ba61db0 100644
--- a/Numbers/Integers/RingStructure/EuclideanDomain.agda
+++ b/Numbers/Integers/RingStructure/EuclideanDomain.agda
@@ -13,7 +13,7 @@ open import Groups.Definition
 open import Rings.Definition
 open import Setoids.Setoids
 open import Rings.EuclideanDomains.Definition
-open import Orders
+open import Orders.Total.Definition
 open import Numbers.Naturals.EuclideanAlgorithm
 
 module Numbers.Integers.RingStructure.EuclideanDomain where
diff --git a/Numbers/Modulo/Addition.agda b/Numbers/Modulo/Addition.agda
index 579377f..b7a676e 100644
--- a/Numbers/Modulo/Addition.agda
+++ b/Numbers/Modulo/Addition.agda
@@ -17,7 +17,7 @@ open import Sets.FinSetWithK
 open import Functions
 open import Numbers.Naturals.WithK
 open import Semirings.Definition
-open import Orders
+open import Orders.Total.Definition
 open import Numbers.Modulo.Definition
 
 module Numbers.Modulo.Addition where
diff --git a/Numbers/Modulo/Definition.agda b/Numbers/Modulo/Definition.agda
index cc4a237..4123f34 100644
--- a/Numbers/Modulo/Definition.agda
+++ b/Numbers/Modulo/Definition.agda
@@ -16,7 +16,6 @@ open import Sets.FinSetWithK
 open import Functions
 open import Numbers.Naturals.WithK
 open import Semirings.Definition
-open import Orders
 
 module Numbers.Modulo.Definition where
   record ℤn (n : ℕ) (pr : 0 <N n) : Set where
diff --git a/Numbers/Modulo/Group.agda b/Numbers/Modulo/Group.agda
index 334d8f3..d808e44 100644
--- a/Numbers/Modulo/Group.agda
+++ b/Numbers/Modulo/Group.agda
@@ -18,9 +18,9 @@ open import Sets.FinSetWithK
 open import Functions
 open import Numbers.Naturals.WithK
 open import Semirings.Definition
-open import Orders
 open import Numbers.Modulo.Definition
 open import Numbers.Modulo.Addition
+open import Orders.Total.Definition
 
 module Numbers.Modulo.Group where
 
diff --git a/Numbers/Naturals/EuclideanAlgorithm.agda b/Numbers/Naturals/EuclideanAlgorithm.agda
index aa3dfdb..b86a943 100644
--- a/Numbers/Naturals/EuclideanAlgorithm.agda
+++ b/Numbers/Naturals/EuclideanAlgorithm.agda
@@ -6,9 +6,9 @@ open import Numbers.Naturals.Naturals
 open import Numbers.Naturals.Order
 open import Numbers.Naturals.Order.Lemmas
 open import Numbers.Naturals.Order.WellFounded
-open import WellFoundedInduction
+open import Orders.WellFounded.Induction
 open import KeyValue.KeyValue
-open import Orders
+open import Orders.Total.Definition
 open import Vectors
 open import Maybe
 open import Semirings.Definition
diff --git a/Numbers/Naturals/Naturals.agda b/Numbers/Naturals/Naturals.agda
index c9ad07f..6334f13 100644
--- a/Numbers/Naturals/Naturals.agda
+++ b/Numbers/Naturals/Naturals.agda
@@ -2,7 +2,6 @@
 
 open import LogicalFormulae
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-open import WellFoundedInduction
 open import Functions
 open import Numbers.Naturals.Definition
 open import Numbers.Naturals.Semiring
@@ -13,7 +12,7 @@ open import Numbers.Naturals.Exponentiation
 open import Numbers.Naturals.Subtraction
 open import Semirings.Definition
 open import Monoids.Definition
-open import Orders
+open import Orders.Total.Definition
 
 module Numbers.Naturals.Naturals where
 
diff --git a/Numbers/Naturals/Order.agda b/Numbers/Naturals/Order.agda
index 3ee9210..f686aab 100644
--- a/Numbers/Naturals/Order.agda
+++ b/Numbers/Naturals/Order.agda
@@ -4,7 +4,8 @@ open import LogicalFormulae
 open import Semirings.Definition
 open import Numbers.Naturals.Definition
 open import Numbers.Naturals.Semiring
-open import Orders
+open import Orders.Total.Definition
+open import Orders.Partial.Definition
 
 module Numbers.Naturals.Order where
 open Semiring ℕSemiring
diff --git a/Numbers/Naturals/Order/Lemmas.agda b/Numbers/Naturals/Order/Lemmas.agda
index bf0d332..d90bbae 100644
--- a/Numbers/Naturals/Order/Lemmas.agda
+++ b/Numbers/Naturals/Order/Lemmas.agda
@@ -4,7 +4,6 @@ open import LogicalFormulae
 open import Semirings.Definition
 open import Numbers.Naturals.Order
 open import Numbers.Naturals.Semiring
-open import Orders
 
 module Numbers.Naturals.Order.Lemmas where
 open Semiring ℕSemiring
diff --git a/Numbers/Naturals/Order/WellFounded.agda b/Numbers/Naturals/Order/WellFounded.agda
index 65114bd..fb45f05 100644
--- a/Numbers/Naturals/Order/WellFounded.agda
+++ b/Numbers/Naturals/Order/WellFounded.agda
@@ -2,12 +2,12 @@
 
 open import LogicalFormulae
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-open import WellFoundedInduction
+open import Orders.WellFounded.Definition
 open import Functions
 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 open import Semirings.Definition
-open import Orders
+open import Orders.Total.Definition
 
 module Numbers.Naturals.Order.WellFounded where
 open Semiring ℕSemiring
diff --git a/Numbers/Naturals/Semiring.agda b/Numbers/Naturals/Semiring.agda
index ae41656..cfe9cd3 100644
--- a/Numbers/Naturals/Semiring.agda
+++ b/Numbers/Naturals/Semiring.agda
@@ -2,9 +2,7 @@
 
 open import LogicalFormulae
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-open import WellFoundedInduction
 open import Functions
-open import Orders
 open import Numbers.Naturals.Definition
 open import Numbers.Naturals.Addition
 open import Numbers.Naturals.Multiplication
diff --git a/Numbers/Naturals/Subtraction.agda b/Numbers/Naturals/Subtraction.agda
index 151d76c..9f1d2dc 100644
--- a/Numbers/Naturals/Subtraction.agda
+++ b/Numbers/Naturals/Subtraction.agda
@@ -2,9 +2,7 @@
 
 open import LogicalFormulae
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-open import WellFoundedInduction
 open import Functions
-open import Orders
 open import Numbers.Naturals.Definition
 open import Numbers.Naturals.Addition
 open import Numbers.Naturals.Order
diff --git a/Numbers/Naturals/WithK.agda b/Numbers/Naturals/WithK.agda
index 7823e06..8ebaa08 100644
--- a/Numbers/Naturals/WithK.agda
+++ b/Numbers/Naturals/WithK.agda
@@ -2,9 +2,7 @@
 
 open import LogicalFormulae
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-open import WellFoundedInduction
 open import Functions
-open import Orders
 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 
diff --git a/Numbers/Primes/IntegerFactorisation.agda b/Numbers/Primes/IntegerFactorisation.agda
index 7f6bfcd..2eb6f63 100644
--- a/Numbers/Primes/IntegerFactorisation.agda
+++ b/Numbers/Primes/IntegerFactorisation.agda
@@ -6,9 +6,9 @@ open import Numbers.Naturals.Order
 open import Numbers.Naturals.Order.Lemmas
 open import Numbers.Naturals.Order.WellFounded
 open import Numbers.Primes.PrimeNumbers
-open import WellFoundedInduction
 open import Semirings.Definition
-open import Orders
+open import Orders.Total.Definition
+open import Orders.WellFounded.Induction
 open import Numbers.Naturals.EuclideanAlgorithm
 
 module Numbers.Primes.IntegerFactorisation where
diff --git a/Numbers/Primes/PrimeNumbers.agda b/Numbers/Primes/PrimeNumbers.agda
index bf8f7bd..c64e235 100644
--- a/Numbers/Primes/PrimeNumbers.agda
+++ b/Numbers/Primes/PrimeNumbers.agda
@@ -7,9 +7,9 @@ open import Numbers.Naturals.Order
 open import Numbers.Naturals.Order.Lemmas
 open import Numbers.Naturals.Order.WellFounded
 open import Numbers.Naturals.WithK
-open import WellFoundedInduction
 open import KeyValue.KeyValue
-open import Orders
+open import Orders.Total.Definition
+open import Orders.Partial.Definition
 open import Vectors
 open import Maybe
 open import WithK
diff --git a/Numbers/Rationals/Lemmas.agda b/Numbers/Rationals/Lemmas.agda
index 29eb7b3..fa2521c 100644
--- a/Numbers/Rationals/Lemmas.agda
+++ b/Numbers/Rationals/Lemmas.agda
@@ -1,6 +1,5 @@
 {-# OPTIONS --safe --warning=error #-}
 
-open import WellFoundedInduction
 open import LogicalFormulae
 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
@@ -22,7 +21,8 @@ open import Functions
 open import Sets.EquivalenceRelations
 open import Numbers.Rationals.Definition
 open import Semirings.Definition
-open import Orders
+open import Orders.Total.Definition
+open import Orders.WellFounded.Induction
 
 module Numbers.Rationals.Lemmas where
 
@@ -86,7 +86,7 @@ evil' = rec <NWellfounded (λ z → (x x₁ : ℕ) (pr' : 0 <N x) (x₂ : z ≡
 
         halveDecreased : underlying aEven <N a
         halveDecreased with aEven
-        halveDecreased | zero , even rewrite equalityCommutative even = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) 0<a)
+        halveDecreased | zero , even rewrite equalityCommutative even = exFalso (TotalOrder.irreflexive ℕTotalOrder 0<a)
         halveDecreased | succ a/2 , even = le a/2 (transitivity (applyEquality succ (transitivity (Semiring.commutative ℕSemiring a/2 _) (applyEquality succ (transitivity (doubleIsAddTwo a/2) (multiplicationNIsCommutative 2 a/2))))) even)
 
         reduced : b +N underlying aEven <N k
@@ -97,7 +97,7 @@ evil' = rec <NWellfounded (λ z → (x x₁ : ℕ) (pr' : 0 <N x) (x₂ : z ≡
         0<b with TotalOrder.totality ℕTotalOrder 0 b
         0<b | inl (inl 0<b) = 0<b
         0<b | inl (inr ())
-        0<b | inr 0=b rewrite equalityCommutative 0=b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) {0} (identityOfIndiscernablesRight _<N_ 0<a (sqrt0 a pr)))
+        0<b | inr 0=b rewrite equalityCommutative 0=b = exFalso (TotalOrder.irreflexive ℕTotalOrder {0} (identityOfIndiscernablesRight _<N_ 0<a (sqrt0 a pr)))
 
         contr : False
         contr = indHyp (b +N underlying aEven) reduced b (underlying aEven) 0<b refl next3
diff --git a/Orders.agda b/Orders.agda
deleted file mode 100644
index 141bbb5..0000000
--- a/Orders.agda
+++ /dev/null
@@ -1,109 +0,0 @@
-{-# OPTIONS --safe --warning=error --without-K #-}
-
-open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-
-open import LogicalFormulae
-open import Functions
-
-module Orders where
-
-record PartialOrder {a b : _} (carrier : Set a) : Set (a ⊔ lsuc b) where
-  field
-    _<_ : Rel {a} {b} carrier
-    irreflexive : {x : carrier} → (x < x) → False
-    <Transitive : {a b c : carrier} → (a < b) → (b < c) → (a < c)
-  <WellDefined : {r s t u : carrier} → (r ≡ t) → (s ≡ u) → r < s → t < u
-  <WellDefined refl refl r<s = r<s
-
-record TotalOrder {a b : _} (carrier : Set a) : Set (a ⊔ lsuc b) where
-  field
-    order : PartialOrder {a} {b} carrier
-  _<_ : Rel carrier
-  _<_ = PartialOrder._<_ order
-  _≤_ : Rel carrier
-  _≤_ a b = (a < b) || (a ≡ b)
-  field
-    totality : (a b : carrier) → ((a < b) || (b < a)) || (a ≡ b)
-  min : carrier → carrier → carrier
-  min a b with totality a b
-  min a b | inl (inl a<b) = a
-  min a b | inl (inr b<a) = b
-  min a b | inr a=b = a
-  max : carrier → carrier → carrier
-  max a b with totality a b
-  max a b | inl (inl a<b) = b
-  max a b | inl (inr b<a) = a
-  max a b | inr a=b = b
-
-  irreflexive = PartialOrder.irreflexive order
-  <Transitive = PartialOrder.<Transitive order
-  <WellDefined = PartialOrder.<WellDefined order
-
-equivMin : {a b : _} {A : Set a} → (order : TotalOrder {a} {b} A) → {x y : A} → (TotalOrder._<_ order x y) → TotalOrder.min order x y ≡ x
-equivMin order {x} {y} x<y with TotalOrder.totality order x y
-equivMin order {x} {y} x<y | inl (inl x₁) = refl
-equivMin order {x} {y} x<y | inl (inr y<x) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.<Transitive (TotalOrder.order order) x<y y<x))
-equivMin order {x} {y} x<y | inr x=y rewrite x=y = refl
-
-equivMin' : {a b : _} {A : Set a} → (order : TotalOrder {a} {b} A) → {x y : A} → (TotalOrder.min order x y ≡ x) → (TotalOrder._<_ order x y) || (x ≡ y)
-equivMin' order {x} {y} minEq with TotalOrder.totality order x y
-equivMin' order {x} {y} minEq | inl (inl x<y) = inl x<y
-equivMin' order {x} {y} minEq | inl (inr y<x) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (identityOfIndiscernablesLeft (TotalOrder._<_ order) y<x minEq))
-equivMin' order {x} {y} minEq | inr x=y = inr x=y
-
-minCommutes : {a b : _} {A : Set a} → (order : TotalOrder {a} {b} A) → (x y : A) → (TotalOrder.min order x y) ≡ (TotalOrder.min order y x)
-minCommutes order x y with TotalOrder.totality order x y
-minCommutes order x y | inl (inl x<y) with TotalOrder.totality order y x
-minCommutes order x y | inl (inl x<y) | inl (inl y<x) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.<Transitive (TotalOrder.order order) y<x x<y))
-minCommutes order x y | inl (inl x<y) | inl (inr x<y') = refl
-minCommutes order x y | inl (inl x<y) | inr y=x = equalityCommutative y=x
-minCommutes order x y | inl (inr y<x) with TotalOrder.totality order y x
-minCommutes order x y | inl (inr y<x) | inl (inl y<x') = refl
-minCommutes order x y | inl (inr y<x) | inl (inr x<y) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.<Transitive (TotalOrder.order order) y<x x<y))
-minCommutes order x y | inl (inr y<x) | inr y=x = refl
-minCommutes order x y | inr x=y with TotalOrder.totality order y x
-minCommutes order x y | inr x=y | inl (inl x₁) = x=y
-minCommutes order x y | inr x=y | inl (inr x₁) = refl
-minCommutes order x y | inr x=y | inr x₁ = x=y
-
-minIdempotent : {a b : _} {A : Set a} → (order : TotalOrder {a} {b} A) → (x : A) → TotalOrder.min order x x ≡ x
-minIdempotent order x with TotalOrder.totality order x x
-minIdempotent order x | inl (inl x₁) = refl
-minIdempotent order x | inl (inr x₁) = refl
-minIdempotent order x | inr x₁ = refl
-
-swapMin : {a b : _} {A : Set a} {order : TotalOrder {a} {b} A} {x y z : A} → (TotalOrder.min order x (TotalOrder.min order y z)) ≡ TotalOrder.min order y (TotalOrder.min order x z)
-swapMin {order = order} {x} {y} {z} with TotalOrder.totality order y z
-swapMin {order = order} {x} {y} {z} | inl (inl y<z) with TotalOrder.totality order x z
-swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inl (inl x<z) = minCommutes order x y
-swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inl (inr z<x) with TotalOrder.totality order x y
-swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inl (inr z<x) | inl (inl x<y) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.<Transitive (TotalOrder.order order) y<z (PartialOrder.<Transitive (TotalOrder.order order) z<x x<y)))
-swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inl (inr z<x) | inl (inr y<x) = equalityCommutative (equivMin order y<z)
-swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inl (inr z<x) | inr x=y rewrite x=y = equalityCommutative (equivMin order y<z)
-swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inr x=z = minCommutes order x y
-swapMin {order = order} {x} {y} {z} | inl (inr z<y) with TotalOrder.totality order x z
-swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inl (inl x<z) rewrite minCommutes order y x = equalityCommutative (equivMin order (PartialOrder.<Transitive (TotalOrder.order order) x<z z<y))
-swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inl (inr z<x) with TotalOrder.totality order y z
-swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inl (inr z<x) | inl (inl y<z) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.<Transitive (TotalOrder.order order) z<y y<z))
-swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inl (inr z<x) | inl (inr z<y') = refl
-swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inl (inr z<x) | inr y=z = equalityCommutative y=z
-swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inr x=z rewrite x=z | minCommutes order y z = equalityCommutative (equivMin order z<y)
-swapMin {order = order} {x} {y} {z} | inr y=z with TotalOrder.totality order x z
-swapMin {order = order} {x} {y} {z} | inr y=z | inl (inl x<z) = minCommutes order x y
-swapMin {order = order} {x} {y} {z} | inr y=z | inl (inr z<x) rewrite y=z | minIdempotent order z | minCommutes order x z = equivMin order z<x
-swapMin {order = order} {x} {y} {z} | inr y=z | inr x=z = minCommutes order x y
-
-minMin : {a b : _} {A : Set a} → (order : TotalOrder {a} {b} A) → {x y : A} → (TotalOrder.min order x (TotalOrder.min order x y)) ≡ TotalOrder.min order x y
-minMin order {x} {y} with TotalOrder.totality order x y
-minMin order {x} {y} | inl (inl x<y) = minIdempotent order x
-minMin order {x} {y} | inl (inr y<x) with TotalOrder.totality order x y
-minMin order {x} {y} | inl (inr y<x) | inl (inl x<y) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.<Transitive (TotalOrder.order order) y<x x<y))
-minMin order {x} {y} | inl (inr y<x) | inl (inr y<x') = refl
-minMin order {x} {y} | inl (inr y<x) | inr x=y = x=y
-minMin order {x} {y} | inr x=y = minIdempotent order x
-
-minFromBoth : {a b : _} {A : Set a} → {order : TotalOrder {a} {b} A} → {min x y : A} → (TotalOrder._<_ order min x) → (TotalOrder._<_ order min y) → (TotalOrder._<_ order min (TotalOrder.min order x y))
-minFromBoth {a} {order = order} {x = x} {y} prX prY with TotalOrder.totality order x y
-minFromBoth {a} prX prY | inl (inl x<y) = prX
-minFromBoth {a} prX prY | inl (inr y<x) = prY
-minFromBoth {a} prX prY | inr x=y = prX
diff --git a/Orders/Partial/Definition.agda b/Orders/Partial/Definition.agda
new file mode 100644
index 0000000..9951a88
--- /dev/null
+++ b/Orders/Partial/Definition.agda
@@ -0,0 +1,16 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+open import LogicalFormulae
+open import Functions
+
+module Orders.Partial.Definition {a : _} (carrier : Set a) where
+
+record PartialOrder {b : _} : Set (a ⊔ lsuc b) where
+  field
+    _<_ : Rel {a} {b} carrier
+    irreflexive : {x : carrier} → (x < x) → False
+    <Transitive : {a b c : carrier} → (a < b) → (b < c) → (a < c)
+  <WellDefined : {r s t u : carrier} → (r ≡ t) → (s ≡ u) → r < s → t < u
+  <WellDefined refl refl r<s = r<s
diff --git a/Orders/Total/Definition.agda b/Orders/Total/Definition.agda
new file mode 100644
index 0000000..ad7a4b7
--- /dev/null
+++ b/Orders/Total/Definition.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+open import LogicalFormulae
+open import Functions
+
+module Orders.Total.Definition {a : _} (carrier : Set a) where
+
+open import Orders.Partial.Definition carrier
+
+record TotalOrder {b : _} : Set (a ⊔ lsuc b) where
+  field
+    order : PartialOrder {b}
+  _<_ : Rel carrier
+  _<_ = PartialOrder._<_ order
+  _≤_ : Rel carrier
+  _≤_ a b = (a < b) || (a ≡ b)
+  field
+    totality : (a b : carrier) → ((a < b) || (b < a)) || (a ≡ b)
+
+  min : carrier → carrier → carrier
+  min a b with totality a b
+  min a b | inl (inl a<b) = a
+  min a b | inl (inr b<a) = b
+  min a b | inr a=b = a
+  max : carrier → carrier → carrier
+  max a b with totality a b
+  max a b | inl (inl a<b) = b
+  max a b | inl (inr b<a) = a
+  max a b | inr a=b = b
+
+  irreflexive = PartialOrder.irreflexive order
+  <Transitive = PartialOrder.<Transitive order
+  <WellDefined = PartialOrder.<WellDefined order
+
diff --git a/Orders/Total/Lemmas.agda b/Orders/Total/Lemmas.agda
new file mode 100644
index 0000000..d520f26
--- /dev/null
+++ b/Orders/Total/Lemmas.agda
@@ -0,0 +1,81 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+open import LogicalFormulae
+open import Functions
+
+open import Orders.Total.Definition
+
+module Orders.Total.Lemmas {a b : _} {A : Set a} (order : TotalOrder A {b}) where
+
+open TotalOrder order
+
+equivMin : {x y : A} → (x < y) → min x y ≡ x
+equivMin {x} {y} x<y with totality x y
+equivMin {x} {y} x<y | inl (inl x₁) = refl
+equivMin {x} {y} x<y | inl (inr y<x) = exFalso (irreflexive (<Transitive x<y y<x))
+equivMin {x} {y} x<y | inr x=y rewrite x=y = refl
+
+equivMin' : {x y : A} → (min x y ≡ x) → (x < y) || (x ≡ y)
+equivMin' {x} {y} minEq with totality x y
+equivMin' {x} {y} minEq | inl (inl x<y) = inl x<y
+equivMin' {x} {y} minEq | inl (inr y<x) = exFalso (irreflexive (identityOfIndiscernablesLeft _<_ y<x minEq))
+equivMin' {x} {y} minEq | inr x=y = inr x=y
+
+minCommutes : (x y : A) → (min x y) ≡ (min y x)
+minCommutes x y with totality x y
+minCommutes x y | inl (inl x<y) with totality y x
+minCommutes x y | inl (inl x<y) | inl (inl y<x) = exFalso (irreflexive (<Transitive y<x x<y))
+minCommutes x y | inl (inl x<y) | inl (inr x<y') = refl
+minCommutes x y | inl (inl x<y) | inr y=x = equalityCommutative y=x
+minCommutes x y | inl (inr y<x) with totality y x
+minCommutes x y | inl (inr y<x) | inl (inl y<x') = refl
+minCommutes x y | inl (inr y<x) | inl (inr x<y) = exFalso (irreflexive (<Transitive y<x x<y))
+minCommutes x y | inl (inr y<x) | inr y=x = refl
+minCommutes x y | inr x=y with totality y x
+minCommutes x y | inr x=y | inl (inl x₁) = x=y
+minCommutes x y | inr x=y | inl (inr x₁) = refl
+minCommutes x y | inr x=y | inr x₁ = x=y
+
+minIdempotent : (x : A) → min x x ≡ x
+minIdempotent x with totality x x
+minIdempotent x | inl (inl x₁) = refl
+minIdempotent x | inl (inr x₁) = refl
+minIdempotent x | inr x₁ = refl
+
+swapMin : {x y z : A} → (min x (min y z)) ≡ min y (min x z)
+swapMin {x} {y} {z} with totality y z
+swapMin {x} {y} {z} | inl (inl y<z) with totality x z
+swapMin {x} {y} {z} | inl (inl y<z) | inl (inl x<z) = minCommutes x y
+swapMin {x} {y} {z} | inl (inl y<z) | inl (inr z<x) with totality x y
+swapMin {x} {y} {z} | inl (inl y<z) | inl (inr z<x) | inl (inl x<y) = exFalso (irreflexive (<Transitive y<z (<Transitive z<x x<y)))
+swapMin {x} {y} {z} | inl (inl y<z) | inl (inr z<x) | inl (inr y<x) = equalityCommutative (equivMin y<z)
+swapMin {x} {y} {z} | inl (inl y<z) | inl (inr z<x) | inr x=y rewrite x=y = equalityCommutative (equivMin y<z)
+swapMin {x} {y} {z} | inl (inl y<z) | inr x=z = minCommutes x y
+swapMin {x} {y} {z} | inl (inr z<y) with totality x z
+swapMin {x} {y} {z} | inl (inr z<y) | inl (inl x<z) rewrite minCommutes y x = equalityCommutative (equivMin (<Transitive x<z z<y))
+swapMin {x} {y} {z} | inl (inr z<y) | inl (inr z<x) with totality y z
+swapMin {x} {y} {z} | inl (inr z<y) | inl (inr z<x) | inl (inl y<z) = exFalso (irreflexive (<Transitive z<y y<z))
+swapMin {x} {y} {z} | inl (inr z<y) | inl (inr z<x) | inl (inr z<y') = refl
+swapMin {x} {y} {z} | inl (inr z<y) | inl (inr z<x) | inr y=z = equalityCommutative y=z
+swapMin {x} {y} {z} | inl (inr z<y) | inr x=z rewrite x=z | minCommutes y z = equalityCommutative (equivMin z<y)
+swapMin {x} {y} {z} | inr y=z with totality x z
+swapMin {x} {y} {z} | inr y=z | inl (inl x<z) = minCommutes x y
+swapMin {x} {y} {z} | inr y=z | inl (inr z<x) rewrite y=z | minIdempotent z | minCommutes x z = equivMin z<x
+swapMin {x} {y} {z} | inr y=z | inr x=z = minCommutes x y
+
+minMin : {x y : A} → (min x (min x y)) ≡ min x y
+minMin {x} {y} with totality x y
+minMin {x} {y} | inl (inl x<y) = minIdempotent x
+minMin {x} {y} | inl (inr y<x) with totality x y
+minMin {x} {y} | inl (inr y<x) | inl (inl x<y) = exFalso (irreflexive (<Transitive y<x x<y))
+minMin {x} {y} | inl (inr y<x) | inl (inr y<x') = refl
+minMin {x} {y} | inl (inr y<x) | inr x=y = x=y
+minMin {x} {y} | inr x=y = minIdempotent x
+
+minFromBoth : {l x y : A} → (l < x) → (l < y) → (l < (min x y))
+minFromBoth {a} {x = x} {y} prX prY with totality x y
+minFromBoth {a} prX prY | inl (inl x<y) = prX
+minFromBoth {a} prX prY | inl (inr y<x) = prY
+minFromBoth {a} prX prY | inr x=y = prX
diff --git a/Orders/WellFounded/Definition.agda b/Orders/WellFounded/Definition.agda
new file mode 100644
index 0000000..b223a5a
--- /dev/null
+++ b/Orders/WellFounded/Definition.agda
@@ -0,0 +1,14 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Functions
+
+module Orders.WellFounded.Definition {a b : _} {A : Set a} (_<_ : Rel {a} {b} A) where
+
+data Accessible (x : A) : Set (lsuc a ⊔ b) where
+  access : (∀ y → y < x → Accessible y) → Accessible x
+
+WellFounded : Set (lsuc a ⊔ b)
+WellFounded = ∀ x → Accessible x
+
diff --git a/Orders/WellFounded/Induction.agda b/Orders/WellFounded/Induction.agda
new file mode 100644
index 0000000..888f525
--- /dev/null
+++ b/Orders/WellFounded/Induction.agda
@@ -0,0 +1,26 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Functions
+open import Orders.WellFounded.Definition
+
+module Orders.WellFounded.Induction {a b : _} {A : Set a} {_<_ : Rel {a} {b} A} (wf : WellFounded _<_) where
+
+private
+  foldAcc :
+    {c : _}
+    (P : A → Set c) →
+    (∀ x → (∀ y → y < x → P y) → P x) →
+    ∀ z → Accessible _<_ z →
+    P z
+  foldAcc P inductionProof = go
+    where
+      go : (z : A) → (Accessible _<_ z) → P z
+      go z (access prf) = inductionProof z (λ y yLessZ → go y (prf y yLessZ))
+
+rec :
+  {c : _}
+  (P : A → Set c) →
+  (∀ x → (∀ y → y < x → P y) → P x) → (∀ z → P z)
+rec P inductionProof z = foldAcc P inductionProof _ (wf z)
diff --git a/Rings/EuclideanDomains/Definition.agda b/Rings/EuclideanDomains/Definition.agda
index c7c0d20..8a0b01a 100644
--- a/Rings/EuclideanDomains/Definition.agda
+++ b/Rings/EuclideanDomains/Definition.agda
@@ -14,7 +14,7 @@ open import Rings.Definition
 open import Rings.Homomorphisms.Definition
 open import Groups.Homomorphisms.Lemmas
 open import Rings.IntegralDomains.Definition
-open import Orders
+open import Orders.Total.Definition
 
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
diff --git a/Rings/Examples/Proofs.agda b/Rings/Examples/Proofs.agda
index 8944c43..0aec7aa 100644
--- a/Rings/Examples/Proofs.agda
+++ b/Rings/Examples/Proofs.agda
@@ -4,7 +4,6 @@ open import LogicalFormulae
 open import Functions
 open import Groups.Groups
 open import Groups.Definition
-open import Orders
 open import Rings.Definition
 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Naturals
@@ -14,6 +13,7 @@ open import Numbers.Primes.PrimeNumbers
 open import Numbers.Modulo.Definition
 open import Numbers.Modulo.Group
 open import Numbers.Naturals.EuclideanAlgorithm
+open import Orders.Total.Definition
 
 module Rings.Examples.Proofs where
   nToZn' : (n : ℕ) (pr : 0 <N n) (x : ℕ) → ℤn n pr
@@ -28,7 +28,7 @@ module Rings.Examples.Proofs where
   mod' (succ n) pr (negSucc x) = Group.inverse (ℤnGroup (succ n) pr) (nToZn' (succ n) pr (succ x))
 
   subtractionEquiv : (a : ℕ) → {b c : ℕ} → (c<b : c <N b) → a +N c ≡ b → a ≡ subtractionNResult.result (-N (inl c<b))
-  subtractionEquiv 0 {b} {c} c<b pr rewrite pr = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) c<b)
+  subtractionEquiv 0 {b} {c} c<b pr rewrite pr = exFalso (TotalOrder.irreflexive ℕTotalOrder c<b)
   subtractionEquiv (succ a) {b} {c} c<b pr = equivalentSubtraction 0 b (succ a) c (succIsPositive a) c<b (equalityCommutative pr)
 
   modNExampleSurjective' : (n : ℕ) → (pr : 0 <N n) → Surjection (mod' n pr)
diff --git a/Rings/Ideals/Prime/Definition.agda b/Rings/Ideals/Prime/Definition.agda
index 66e4903..c5a1069 100644
--- a/Rings/Ideals/Prime/Definition.agda
+++ b/Rings/Ideals/Prime/Definition.agda
@@ -5,7 +5,6 @@ open import Groups.Groups
 open import Groups.Lemmas
 open import Groups.Definition
 open import Numbers.Naturals.Naturals
-open import Orders
 open import Setoids.Setoids
 open import Functions
 open import Rings.Definition
diff --git a/Rings/IntegralDomains/Definition.agda b/Rings/IntegralDomains/Definition.agda
index bd02c76..d2d7d6a 100644
--- a/Rings/IntegralDomains/Definition.agda
+++ b/Rings/IntegralDomains/Definition.agda
@@ -5,7 +5,6 @@ open import Groups.Groups
 open import Groups.Lemmas
 open import Groups.Definition
 open import Numbers.Naturals.Naturals
-open import Orders
 open import Setoids.Setoids
 open import Functions
 open import Rings.Definition
diff --git a/Rings/IntegralDomains/Examples.agda b/Rings/IntegralDomains/Examples.agda
index e56f22e..0023184 100644
--- a/Rings/IntegralDomains/Examples.agda
+++ b/Rings/IntegralDomains/Examples.agda
@@ -5,7 +5,6 @@ open import Groups.Groups
 open import Groups.Lemmas
 open import Groups.Definition
 open import Numbers.Naturals.Naturals
-open import Orders
 open import Setoids.Setoids
 open import Functions
 open import Rings.Definition
diff --git a/Rings/IntegralDomains/Lemmas.agda b/Rings/IntegralDomains/Lemmas.agda
index 968cd36..4652942 100644
--- a/Rings/IntegralDomains/Lemmas.agda
+++ b/Rings/IntegralDomains/Lemmas.agda
@@ -5,7 +5,6 @@ open import Groups.Groups
 open import Groups.Lemmas
 open import Groups.Definition
 open import Numbers.Naturals.Naturals
-open import Orders
 open import Setoids.Setoids
 open import Functions
 open import Rings.Definition
diff --git a/Rings/Primes/Lemmas.agda b/Rings/Primes/Lemmas.agda
index 78e3966..9202b44 100644
--- a/Rings/Primes/Lemmas.agda
+++ b/Rings/Primes/Lemmas.agda
@@ -5,7 +5,6 @@ open import Groups.Groups
 open import Groups.Lemmas
 open import Groups.Definition
 open import Numbers.Naturals.Naturals
-open import Orders
 open import Setoids.Setoids
 open import Functions
 open import Rings.Definition
diff --git a/Setoids/Orders.agda b/Setoids/Orders.agda
index 33cc720..f51c3cd 100644
--- a/Setoids/Orders.agda
+++ b/Setoids/Orders.agda
@@ -1,7 +1,8 @@
 {-# OPTIONS --safe --warning=error --without-K #-}
 
 open import LogicalFormulae
-open import Orders
+open import Orders.Total.Definition
+open import Orders.Partial.Definition
 open import Setoids.Setoids
 open import Functions
 
@@ -33,10 +34,10 @@ record SetoidTotalOrder {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_<_ : Re
   max a b | inl (inr b<a) = a
   max a b | inr a=b = b
 
-partialOrderToSetoidPartialOrder : {a b : _} {A : Set a} (P : PartialOrder {a} {b} A) → SetoidPartialOrder (reflSetoid A) (PartialOrder._<_ P)
+partialOrderToSetoidPartialOrder : {a b : _} {A : Set a} (P : PartialOrder {a} A {b}) → SetoidPartialOrder (reflSetoid A) (PartialOrder._<_ P)
 SetoidPartialOrder.<WellDefined (partialOrderToSetoidPartialOrder P) a=b c=d a<c rewrite a=b | c=d = a<c
 SetoidPartialOrder.irreflexive (partialOrderToSetoidPartialOrder P) = PartialOrder.irreflexive P
 SetoidPartialOrder.<Transitive (partialOrderToSetoidPartialOrder P) = PartialOrder.<Transitive P
 
-totalOrderToSetoidTotalOrder : {a b : _} {A : Set a} (T : TotalOrder {a} {b} A) → SetoidTotalOrder (partialOrderToSetoidPartialOrder (TotalOrder.order T))
+totalOrderToSetoidTotalOrder : {a b : _} {A : Set a} (T : TotalOrder {a} A {b}) → SetoidTotalOrder (partialOrderToSetoidPartialOrder (TotalOrder.order T))
 SetoidTotalOrder.totality (totalOrderToSetoidTotalOrder T) = TotalOrder.totality T
diff --git a/Sets/CantorBijection/CantorBijection.agda b/Sets/CantorBijection/CantorBijection.agda
index 7c6bf70..7fe8108 100644
--- a/Sets/CantorBijection/CantorBijection.agda
+++ b/Sets/CantorBijection/CantorBijection.agda
@@ -7,8 +7,6 @@ open import Functions
 open import Numbers.Naturals.Naturals
 open import Sets.FinSet
 open import Semirings.Definition
-open import Orders
-open import WellFoundedInduction
 open import Sets.CantorBijection.Proofs
 
 module Sets.CantorBijection.CantorBijection where
diff --git a/Sets/CantorBijection/Order.agda b/Sets/CantorBijection/Order.agda
index b77043d..2b4340a 100644
--- a/Sets/CantorBijection/Order.agda
+++ b/Sets/CantorBijection/Order.agda
@@ -9,8 +9,10 @@ open import Numbers.Naturals.Order
 open import Numbers.Naturals.Order.WellFounded
 open import Sets.FinSet
 open import Semirings.Definition
-open import Orders
-open import WellFoundedInduction
+open import Orders.Total.Definition
+open import Orders.Partial.Definition
+open import Orders.WellFounded.Definition
+open import Orders.WellFounded.Induction
 
 module Sets.CantorBijection.Order where
 
diff --git a/Sets/CantorBijection/Proofs.agda b/Sets/CantorBijection/Proofs.agda
index 6427dff..4f4b619 100644
--- a/Sets/CantorBijection/Proofs.agda
+++ b/Sets/CantorBijection/Proofs.agda
@@ -8,9 +8,9 @@ open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 open import Sets.FinSet
 open import Semirings.Definition
-open import Orders
-open import WellFoundedInduction
 open import Sets.CantorBijection.Order
+open import Orders.Total.Definition
+open import Orders.WellFounded.Induction
 
 module Sets.CantorBijection.Proofs where
 
diff --git a/Sets/Cardinality.agda b/Sets/Cardinality.agda
index 634fb5a..323b6b5 100644
--- a/Sets/Cardinality.agda
+++ b/Sets/Cardinality.agda
@@ -9,9 +9,8 @@ open import Numbers.Naturals.Order
 open import Numbers.Naturals.Order.Lemmas
 open import Sets.FinSet
 open import Semirings.Definition
-open import Orders
-open import WellFoundedInduction
 open import Sets.CantorBijection.CantorBijection
+open import Orders.Total.Definition
 
 module Sets.Cardinality where
 
diff --git a/Sets/FinSet.agda b/Sets/FinSet.agda
index 4354bba..2cdf25f 100644
--- a/Sets/FinSet.agda
+++ b/Sets/FinSet.agda
@@ -6,7 +6,6 @@ open import LogicalFormulae
 open import Numbers.Naturals.Naturals
 open import Numbers.Naturals.Definition
 open import Numbers.Naturals.Order
-open import Orders
 
 module Sets.FinSet where
   data FinSet : (n : ℕ) → Set where
diff --git a/Vectors.agda b/Vectors.agda
index beaf28e..ff643fd 100644
--- a/Vectors.agda
+++ b/Vectors.agda
@@ -5,9 +5,11 @@ open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 open import Functions
 open import Semirings.Definition
-open import Orders
+open import Orders.Total.Definition
 open import Lists.Lists
 
+module Vectors where
+
 data Vec {a : _} (X : Set a) : ℕ -> Set a where
   [] : Vec X zero
   _,-_ : {n : ℕ} -> X -> Vec X n -> Vec X (succ n)
diff --git a/WellFoundedInduction.agda b/WellFoundedInduction.agda
deleted file mode 100644
index 86681d3..0000000
--- a/WellFoundedInduction.agda
+++ /dev/null
@@ -1,29 +0,0 @@
-{-# OPTIONS --safe --warning=error --without-K #-}
-
-open import LogicalFormulae
-open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-open import Functions
-
-module WellFoundedInduction where
-
-data Accessible {a} {b} {A} (_<_ : Rel {a} {b} A) (x : A) : Set (lsuc a ⊔ b) where
-  access : (∀ y → y < x → Accessible _<_ y) → Accessible _<_ x
-
-WellFounded : {a b : _} → ∀ {A} → Rel {a} {b} A → Set (lsuc a ⊔ b)
-WellFounded {a} _<_ = ∀ x → Accessible _<_ x
-
-foldAcc : {a b c : _} → {A : Set a} → {_<_ : Rel {a} {c} A} →
-  (P : A → Set b) →
-  (∀ x → (∀ y → y < x → P y) → P x) →
-  ∀ z → Accessible _<_ z →
-  P z
-foldAcc {a} {b} {c} {A} {_<_} P inductionProof = go
-  where
-    go : (z : A) → (Accessible _<_ z) → P z
-    go z (access prf) = inductionProof z (λ y yLessZ → go y (prf y yLessZ))
-
-rec : {a b c : _} → {A : Set a} → {_<_ : Rel {a} {c} A} →
-  WellFounded _<_ →
-  (P : A → Set b) →
-  (∀ x → (∀ y → y < x → P y) → P x) → (∀ z → P z)
-rec wf P inductionProof z = foldAcc P inductionProof _ (wf z)