From 0dfcf44379fa6574836ff57bda1f2930ccfc24cd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Wed, 24 Jul 2024 12:17:17 -0300
Subject: [PATCH] wip: prime numbers

---
 src/1Lab/Classical.lagda.md                   |   2 +-
 src/1Lab/Equiv.lagda.md                       |   8 +-
 src/1Lab/HLevel.lagda.md                      |   2 +-
 src/1Lab/Membership.agda                      |   2 +-
 src/1Lab/Path.lagda.md                        |   5 +-
 src/1Lab/Path/IdentitySystem.lagda.md         |  11 +-
 src/1Lab/Resizing.lagda.md                    |   6 +-
 src/1Lab/Rewrite.agda                         |  12 -
 src/1Lab/Type.lagda.md                        |   2 +-
 src/1Lab/Underlying.agda                      |   5 +
 src/1Lab/Univalence.lagda.md                  |   2 +-
 src/Algebra/Magma.lagda.md                    |   2 +-
 src/Algebra/Ring/Solver.agda                  |   1 -
 src/Cat/Base.lagda.md                         |  13 +-
 src/Cat/CartesianClosed/Instances/PSh.agda    |   4 +-
 src/Cat/Displayed/Comprehension.lagda.md      |   2 +-
 src/Cat/Displayed/Total/Op.lagda.md           |  17 +-
 src/Cat/Instances/Comma.lagda.md              |   2 +-
 src/Cat/Instances/Shape/Involution.lagda.md   |   2 +-
 src/Cat/Instances/Shape/Parallel.lagda.md     |   6 +-
 src/Cat/Instances/Shape/Two.lagda.md          |   4 +-
 src/Cat/Instances/StrictCat/Cohesive.lagda.md |   2 +-
 src/Cat/Internal/Opposite.lagda.md            |   6 +-
 src/Cat/Monoidal/Instances/Day.lagda.md       |   6 +-
 src/Data/Bool.lagda.md                        |  94 +-----
 src/Data/Bool/Base.lagda.md                   | 129 ++++++++
 src/Data/Dec/Base.lagda.md                    |   8 +-
 src/Data/Fin/Base.lagda.md                    |  12 +-
 src/Data/Fin/Properties.lagda.md              |  47 ++-
 src/Data/Id/Base.lagda.md                     |  11 +-
 src/Data/Int/HIT.lagda.md                     |   8 +-
 src/Data/List/Base.lagda.md                   |   6 +-
 src/Data/List/Properties.lagda.md             |   1 -
 src/Data/List/Quantifiers.lagda.md            |  19 +-
 src/Data/Nat/Base.lagda.md                    |  40 +--
 src/Data/Nat/DivMod.lagda.md                  | 118 +++++--
 src/Data/Nat/Divisible.lagda.md               |  29 +-
 src/Data/Nat/Divisible/GCD.lagda.md           |  41 +++
 src/Data/Nat/Order.lagda.md                   | 129 ++++++--
 src/Data/Nat/Prime.lagda.md                   | 291 ++++++++++++++++++
 src/Data/Nat/Properties.lagda.md              |  21 +-
 src/Data/Sum/Properties.lagda.md              |   2 +-
 src/Homotopy/Space/Delooping.lagda.md         |   5 +-
 .../Propositional/Classical/SAT.lagda.md      |   6 +-
 src/Meta/Append.lagda.md                      |   2 +-
 src/Prim/Data/Nat.lagda.md                    |   4 +-
 src/Prim/Data/Sigma.lagda.md                  |   2 +-
 src/Prim/Kan.lagda.md                         |   4 +-
 48 files changed, 860 insertions(+), 293 deletions(-)
 delete mode 100644 src/1Lab/Rewrite.agda
 create mode 100644 src/Data/Bool/Base.lagda.md
 create mode 100644 src/Data/Nat/Prime.lagda.md

diff --git a/src/1Lab/Classical.lagda.md b/src/1Lab/Classical.lagda.md
index 743cdfd4f..42220d040 100644
--- a/src/1Lab/Classical.lagda.md
+++ b/src/1Lab/Classical.lagda.md
@@ -153,7 +153,7 @@ gives us a section $\Sigma P \to 2$.
 ```agda
 module _ (split : Surjections-split) (P : Ω) where
   section : ∥ ((x : Susp ∣ P ∣) → fibre 2→Σ x) ∥
-  section = split Bool-is-set (Susp-prop-is-set (hlevel 1)) 2→Σ 2→Σ-surjective
+  section = split (hlevel 2) (Susp-prop-is-set (hlevel 1)) 2→Σ 2→Σ-surjective
 ```
 
 But a section is always injective, and the booleans are [[discrete]], so we can
diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md
index 1a8ef473d..520346896 100644
--- a/src/1Lab/Equiv.lagda.md
+++ b/src/1Lab/Equiv.lagda.md
@@ -202,7 +202,7 @@ point with, rather than being a property of points.
 
 ```agda
 fibre : (A → B) → B → Type _
-fibre {A = A} f y = Σ[ x ∈ A ] (f x ≡ y)
+fibre {A = A} f y = Σ[ x ∈ A ] f x ≡ y
 ```
 :::
 
@@ -1094,13 +1094,13 @@ lift-inj p = ap Lift.lower p
 fibre-∘-≃
   : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
   → {f : B → C} {g : A → B}
-  → ∀ c → fibre (f ∘ g) c ≃ (Σ[ (b , _) ∈ fibre f c ] (fibre g b))
+  → ∀ c → fibre (f ∘ g) c ≃ (Σ[ (b , _) ∈ fibre f c ] fibre g b)
 fibre-∘-≃ {f = f} {g = g} c = Iso→Equiv (fwd , iso bwd invl invr)
     where
-      fwd : fibre (f ∘ g) c → Σ[ (b , _) ∈ fibre f c ] (fibre g b)
+      fwd : fibre (f ∘ g) c → Σ[ (b , _) ∈ fibre f c ] fibre g b
       fwd (a , p) = ((g a) , p) , (a , refl)
 
-      bwd : Σ[ (b , _) ∈ fibre f c ] (fibre g b) → fibre (f ∘ g) c
+      bwd : Σ[ (b , _) ∈ fibre f c ] fibre g b → fibre (f ∘ g) c
       bwd ((b , p) , (a , q)) = a , ap f q ∙ p
 
       invl : ∀ x → fwd (bwd x) ≡ x
diff --git a/src/1Lab/HLevel.lagda.md b/src/1Lab/HLevel.lagda.md
index 340286102..84b322d46 100644
--- a/src/1Lab/HLevel.lagda.md
+++ b/src/1Lab/HLevel.lagda.md
@@ -204,7 +204,7 @@ proof (used in the *definition* of path induction), we can demonstrate
 the application of path induction:
 
 ```agda
-_ : (a : A) → is-contr (Σ[ b ∈ A ] (b ≡ a))
+_ : (a : A) → is-contr (Σ[ b ∈ A ] b ≡ a)
 _ = λ t → record
   { centre = (t , refl)
   ; paths  = λ (s , p) → J' (λ s t p → (t , refl) ≡ (s , p)) (λ t → refl) p
diff --git a/src/1Lab/Membership.agda b/src/1Lab/Membership.agda
index 60f1df61a..7fedf95f5 100644
--- a/src/1Lab/Membership.agda
+++ b/src/1Lab/Membership.agda
@@ -45,7 +45,7 @@ infix 30 _∉_
 ∫ₚ
   : ∀ {ℓ ℓ' ℓ''} {X : Type ℓ} {ℙX : Type ℓ'} ⦃ m : Membership X ℙX ℓ'' ⦄
   → ℙX → Type _
-∫ₚ {X = X} P = Σ[ x ∈ X ] (x ∈ P)
+∫ₚ {X = X} P = Σ[ x ∈ X ] x ∈ P
 
 -- Notation typeclass for _⊆_. We could always define
 --
diff --git a/src/1Lab/Path.lagda.md b/src/1Lab/Path.lagda.md
index 474002dce..d5e6d6dfe 100644
--- a/src/1Lab/Path.lagda.md
+++ b/src/1Lab/Path.lagda.md
@@ -1044,7 +1044,7 @@ inhabitant!
 
 ```agda
 Singleton : ∀ {ℓ} {A : Type ℓ} → A → Type _
-Singleton x = Σ[ y ∈ _ ] (x ≡ y)
+Singleton x = Σ[ y ∈ _ ] x ≡ y
 ```
 
 We're given an inhabitant $y : A$ and a path $p : x \is y$. To identify
@@ -2378,5 +2378,8 @@ _$ₚ_ : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → Type ℓ₂} {f g : 
      → f ≡ g → ∀ x → f x ≡ g x
 (f $ₚ x) i = f i x
 {-# INLINE _$ₚ_ #-}
+
+_≠_ : ∀ {ℓ} {A : Type ℓ} → A → A → Type ℓ
+x ≠ y = ¬ x ≡ y
 ```
 -->
diff --git a/src/1Lab/Path/IdentitySystem.lagda.md b/src/1Lab/Path/IdentitySystem.lagda.md
index a2cc7a102..97f0e82f7 100644
--- a/src/1Lab/Path/IdentitySystem.lagda.md
+++ b/src/1Lab/Path/IdentitySystem.lagda.md
@@ -332,12 +332,7 @@ This is known as **Hedberg's theorem**.
 
 opaque
   Discrete→is-set : ∀ {ℓ} {A : Type ℓ} → Discrete A → is-set A
-  Discrete→is-set {A = A} dec =
-    identity-system→hlevel 1 (¬¬-stable-identity-system stable) λ x y f g →
-      funext λ h → absurd (g h)
-    where
-      stable : {x y : A} → ¬ ¬ x ≡ y → x ≡ y
-      stable {x = x} {y = y} ¬¬p with dec {x} {y}
-      ... | yes p = p
-      ... | no ¬p = absurd (¬¬p ¬p)
+  Discrete→is-set {A = A} dec = identity-system→hlevel 1
+    (¬¬-stable-identity-system (dec→dne ⦃ dec ⦄))
+    λ x y f g → funext λ h → absurd (g h)
 ```
diff --git a/src/1Lab/Resizing.lagda.md b/src/1Lab/Resizing.lagda.md
index 4555c4e39..56bb6f318 100644
--- a/src/1Lab/Resizing.lagda.md
+++ b/src/1Lab/Resizing.lagda.md
@@ -227,9 +227,9 @@ disjunctions, and implications.
 
 <!--
 ```agda
-infixr 6 _∧Ω_
-infixr 5 _∨Ω_
-infixr 4 _→Ω_
+infixr 10 _∧Ω_
+infixr 9 _∨Ω_
+infixr 8 _→Ω_
 ```
 -->
 
diff --git a/src/1Lab/Rewrite.agda b/src/1Lab/Rewrite.agda
deleted file mode 100644
index d2ad83d6f..000000000
--- a/src/1Lab/Rewrite.agda
+++ /dev/null
@@ -1,12 +0,0 @@
-open import 1Lab.Path
-open import 1Lab.Type
-
-module 1Lab.Rewrite where
-
-data _≡rw_ {ℓ} {A : Type ℓ} (x : A) : A → SSet ℓ where
-  idrw : x ≡rw x
-
-{-# BUILTIN REWRITE _≡rw_ #-}
-
-postulate
-  make-rewrite : ∀ {ℓ} {A : Type ℓ} {x y : A} → Path A x y → x ≡rw y
diff --git a/src/1Lab/Type.lagda.md b/src/1Lab/Type.lagda.md
index 559cae942..6f29383f9 100644
--- a/src/1Lab/Type.lagda.md
+++ b/src/1Lab/Type.lagda.md
@@ -49,7 +49,7 @@ absurd ()
 
 ¬_ : ∀ {ℓ} → Type ℓ → Type ℓ
 ¬ A = A → ⊥
-infix 3 ¬_
+infix 6 ¬_
 ```
 
 :::{.definition #product-type}
diff --git a/src/1Lab/Underlying.agda b/src/1Lab/Underlying.agda
index 9c90c96f0..068c8ed12 100644
--- a/src/1Lab/Underlying.agda
+++ b/src/1Lab/Underlying.agda
@@ -6,6 +6,8 @@ open import 1Lab.HLevel
 open import 1Lab.Path
 open import 1Lab.Type hiding (Σ-syntax)
 
+open import Data.Bool.Base
+
 module 1Lab.Underlying where
 
 -- Notation class for types which have a chosen projection into a
@@ -54,6 +56,9 @@ instance
   Underlying-Lift ⦃ ua ⦄ .ℓ-underlying = ua .ℓ-underlying
   Underlying-Lift .⌞_⌟ x = ⌞ x .Lift.lower ⌟
 
+  Underlying-Bool : Underlying Bool
+  Underlying-Bool = record { ⌞_⌟ = So }
+
 -- The converse of to-is-true, generalised slightly. If P and Q are
 -- identical inhabitants of some type of structured types, and Q's
 -- underlying type is contractible, then P is inhabited. P's underlying
diff --git a/src/1Lab/Univalence.lagda.md b/src/1Lab/Univalence.lagda.md
index 427d8b624..a5d29b59b 100644
--- a/src/1Lab/Univalence.lagda.md
+++ b/src/1Lab/Univalence.lagda.md
@@ -95,7 +95,7 @@ open import 1Lab.Equiv.FromPath
 ```agda
 Glue : (A : Type ℓ)
      → {φ : I}
-     → (Te : Partial φ (Σ[ T ∈ Type ℓ' ] (T ≃ A)))
+     → (Te : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ A))
      → Type ℓ'
 ```
 
diff --git a/src/Algebra/Magma.lagda.md b/src/Algebra/Magma.lagda.md
index 3a84170f9..c7a0e0cf3 100644
--- a/src/Algebra/Magma.lagda.md
+++ b/src/Algebra/Magma.lagda.md
@@ -138,7 +138,7 @@ set, this obviously defines a magma:
 ```agda
 private
   is-magma-imp : is-magma imp
-  is-magma-imp .has-is-set = Bool-is-set
+  is-magma-imp .has-is-set = hlevel 2
 ```
 
 We show it is not commutative or associative by giving counterexamples:
diff --git a/src/Algebra/Ring/Solver.agda b/src/Algebra/Ring/Solver.agda
index ebe85fd38..bf1107915 100644
--- a/src/Algebra/Ring/Solver.agda
+++ b/src/Algebra/Ring/Solver.agda
@@ -12,7 +12,6 @@ Horner normal forms are not sparse).
 open import 1Lab.Reflection.Variables
 open import 1Lab.Reflection.Solver
 open import 1Lab.Reflection
-open import 1Lab.Rewrite
 
 open import Algebra.Ring.Cat.Initial
 open import Algebra.Ring.Commutative
diff --git a/src/Cat/Base.lagda.md b/src/Cat/Base.lagda.md
index e21d71a83..34292d46e 100644
--- a/src/Cat/Base.lagda.md
+++ b/src/Cat/Base.lagda.md
@@ -8,7 +8,6 @@ open import 1Lab.Extensionality
 open import 1Lab.HLevel.Closure
 open import 1Lab.Reflection
 open import 1Lab.Underlying
-open import 1Lab.Rewrite
 open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path
@@ -198,10 +197,7 @@ C^op^op≡C {C = C} i = precat i where
 
 <!--
 ```agda
-private
-  precategory-double-dual : ∀ {o ℓ} {C : Precategory o ℓ} → C ^op ^op ≡rw C
-  precategory-double-dual = make-rewrite C^op^op≡C
-{-# REWRITE precategory-double-dual #-}
+{-# REWRITE C^op^op≡C #-}
 ```
 -->
 
@@ -312,12 +308,7 @@ F^op^op≡F {F = F} i .Functor.F₁ = F .Functor.F₁
 F^op^op≡F {F = F} i .Functor.F-id = F .Functor.F-id
 F^op^op≡F {F = F} i .Functor.F-∘ = F .Functor.F-∘
 
-private
-  functor-double-dual
-    : ∀ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'} {F : Functor C D}
-    → Functor.op (Functor.op F) ≡rw F
-  functor-double-dual = make-rewrite F^op^op≡F
-{-# REWRITE functor-double-dual #-}
+{-# REWRITE F^op^op≡F #-}
 ```
 -->
 
diff --git a/src/Cat/CartesianClosed/Instances/PSh.agda b/src/Cat/CartesianClosed/Instances/PSh.agda
index ce2fab861..ebf830d35 100644
--- a/src/Cat/CartesianClosed/Instances/PSh.agda
+++ b/src/Cat/CartesianClosed/Instances/PSh.agda
@@ -53,7 +53,7 @@ module _ {o ℓ κ} {C : Precategory o ℓ} where
     open is-pullback
 
     pb-path
-      : ∀ {i} {x y : Σ[ x ∈ X.₀ i ] Σ[ y ∈ Y.₀ i ] (f.η i x ≡ g.η i y)}
+      : ∀ {i} {x y : Σ[ x ∈ X.₀ i ] Σ[ y ∈ Y.₀ i ] f.η i x ≡ g.η i y}
       → x .fst ≡ y .fst
       → x .snd .fst ≡ y .snd .fst
       → x ≡ y
@@ -65,7 +65,7 @@ module _ {o ℓ κ} {C : Precategory o ℓ} where
         i j
 
     pb : Pullback (PSh κ C) f g
-    pb .apex .F₀ i = el! (Σ[ x ∈ X.₀ i ] Σ[ y ∈ Y.₀ i ] (f.η i x ≡ g.η i y))
+    pb .apex .F₀ i = el! (Σ[ x ∈ X.₀ i ] Σ[ y ∈ Y.₀ i ] f.η i x ≡ g.η i y)
     pb .apex .F₁ {x} {y} h (a , b , p) = X.₁ h a , Y.₁ h b , path where abstract
       path : f.η y (X.₁ h a) ≡ g.η y (Y.₁ h b)
       path = happly (f.is-natural _ _ _) _
diff --git a/src/Cat/Displayed/Comprehension.lagda.md b/src/Cat/Displayed/Comprehension.lagda.md
index 251a1c359..cc09e56ee 100644
--- a/src/Cat/Displayed/Comprehension.lagda.md
+++ b/src/Cat/Displayed/Comprehension.lagda.md
@@ -164,7 +164,7 @@ with projections.
   _⨾ˢ_ : ∀ {Γ Δ x y} (σ : Hom Γ Δ) → Hom[ σ ] x y → Hom (Γ ⨾ x) (Δ ⨾ y)
   σ ⨾ˢ f = F₁' f .to
 
-  infixl 5 _⨾ˢ_
+  infixl 8 _⨾ˢ_
 
   sub-proj : ∀ {Γ Δ x y} {σ : Hom Γ Δ} → (f : Hom[ σ ] x y) → πᶜ ∘ (σ ⨾ˢ f) ≡ σ ∘ πᶜ
   sub-proj f = sym $ F₁' f .commute
diff --git a/src/Cat/Displayed/Total/Op.lagda.md b/src/Cat/Displayed/Total/Op.lagda.md
index c8c69c3c2..4f49c9d7d 100644
--- a/src/Cat/Displayed/Total/Op.lagda.md
+++ b/src/Cat/Displayed/Total/Op.lagda.md
@@ -1,7 +1,5 @@
 <!--
 ```agda
-open import 1Lab.Rewrite
-
 open import Cat.Functor.Equivalence.Path
 open import Cat.Functor.Equivalence
 open import Cat.Displayed.Fibre
@@ -68,12 +66,7 @@ total-op-involution {ℰ = ℰ} = path where
 
 <!--
 ```agda
-private
-  displayed-double-dual
-    : ∀ {o ℓ o' ℓ'} {ℬ : Precategory o ℓ} {ℰ : Displayed ℬ o' ℓ'}
-    → ((ℰ ^total-op) ^total-op) ≡rw ℰ
-  displayed-double-dual {ℰ = ℰ} = make-rewrite (total-op-involution {ℰ = ℰ})
-  {-# REWRITE displayed-double-dual #-}
+{-# REWRITE total-op-involution #-}
 ```
 -->
 
@@ -180,12 +173,6 @@ fibre-functor-total-op-total-op {ℰ = ℰ} {y = y} {F = F} i .F-∘ f g =
     i
     where open Precategory (Fibre ℰ y)
 
-private
-  fibre-functor-double-dual
-    : ∀ {o ℓ o' ℓ'} {ℬ : Precategory o ℓ} {ℰ : Displayed ℬ o' ℓ'} {x y}
-    → {F : Functor (Fibre ℰ x) (Fibre ℰ y)}
-    → fibre-functor-total-op (fibre-functor-total-op F) ≡rw F
-  fibre-functor-double-dual = make-rewrite fibre-functor-total-op-total-op
-{-# REWRITE fibre-functor-double-dual #-}
+{-# REWRITE fibre-functor-total-op-total-op #-}
 ```
 -->
diff --git a/src/Cat/Instances/Comma.lagda.md b/src/Cat/Instances/Comma.lagda.md
index b44ab8dcc..28fbcc122 100644
--- a/src/Cat/Instances/Comma.lagda.md
+++ b/src/Cat/Instances/Comma.lagda.md
@@ -239,7 +239,7 @@ square.
 module _ {A : Precategory ao ah} {B : Precategory bo bh} where
   private module A = Precategory A
 
-  infix 5 _↙_ _↘_
+  infix 8 _↙_ _↘_
   _↙_ : A.Ob → Functor B A → Precategory _ _
   X ↙ T = !Const X ↓ T
 
diff --git a/src/Cat/Instances/Shape/Involution.lagda.md b/src/Cat/Instances/Shape/Involution.lagda.md
index 6bd914ee8..a9b5ee85e 100644
--- a/src/Cat/Instances/Shape/Involution.lagda.md
+++ b/src/Cat/Instances/Shape/Involution.lagda.md
@@ -24,7 +24,7 @@ composition operation.
 ∙⤮∙ : Precategory lzero lzero
 ∙⤮∙ .Precategory.Ob = ⊤
 ∙⤮∙ .Precategory.Hom _ _ = Bool
-∙⤮∙ .Precategory.Hom-set _ _ = Bool-is-set
+∙⤮∙ .Precategory.Hom-set _ _ = hlevel 2
 ∙⤮∙ .Precategory.id = false
 ∙⤮∙ .Precategory._∘_ = xor
 ∙⤮∙ .Precategory.idr f = xor-falser f
diff --git a/src/Cat/Instances/Shape/Parallel.lagda.md b/src/Cat/Instances/Shape/Parallel.lagda.md
index 8d962b429..23eb71651 100644
--- a/src/Cat/Instances/Shape/Parallel.lagda.md
+++ b/src/Cat/Instances/Shape/Parallel.lagda.md
@@ -39,9 +39,9 @@ parallel arrows between them. It is the shape of [[equaliser]] and
 
 <!--
 ```agda
-  precat .Hom-set false false a b p q i j = tt
-  precat .Hom-set false true  a b p q i j = Bool-is-set a b p q i j
-  precat .Hom-set true  true  a b p q i j = tt
+  precat .Hom-set false false = hlevel 2
+  precat .Hom-set false true  = hlevel 2
+  precat .Hom-set true  true  = hlevel 2
 
   precat .id {false} = tt
   precat .id {true} = tt
diff --git a/src/Cat/Instances/Shape/Two.lagda.md b/src/Cat/Instances/Shape/Two.lagda.md
index 3840cba7a..bb4e846e3 100644
--- a/src/Cat/Instances/Shape/Two.lagda.md
+++ b/src/Cat/Instances/Shape/Two.lagda.md
@@ -66,11 +66,11 @@ defined above.
 
     q : ∀ {x y} (f : x ≡ y) → _
     q {false} {false} p =
-      F .F₁ p           ≡⟨ ap (F .F₁) (Bool-is-set _ _ _ _) ⟩
+      F .F₁ p           ≡⟨ ap (F .F₁) prop! ⟩
       F .F₁ refl        ≡⟨ F .F-id ⟩
       id                ∎
     q {true} {true} p =
-      F .F₁ p           ≡⟨ ap (F .F₁) (Bool-is-set _ _ _ _) ⟩
+      F .F₁ p           ≡⟨ ap (F .F₁) prop! ⟩
       F .F₁ refl        ≡⟨ F .F-id ⟩
       id                ∎
     q {false} {true} p = absurd (true≠false (sym p))
diff --git a/src/Cat/Instances/StrictCat/Cohesive.lagda.md b/src/Cat/Instances/StrictCat/Cohesive.lagda.md
index 38a25e0e2..043c7ad50 100644
--- a/src/Cat/Instances/StrictCat/Cohesive.lagda.md
+++ b/src/Cat/Instances/StrictCat/Cohesive.lagda.md
@@ -337,7 +337,7 @@ category are product sets of connected components.
 
 ```agda
 Π₀-preserve-prods
-  : ∀ {C D : Precategory o h} → π₀ ʻ (C ×ᶜ D) ≡ π₀ ʻ C × π₀ ʻ D
+  : ∀ {C D : Precategory o h} → π₀ ʻ (C ×ᶜ D) ≡ (π₀ ʻ C × π₀ ʻ D)
 Π₀-preserve-prods {C = C} {D = D} = Iso→Path (f , isom) where
   open is-iso
 ```
diff --git a/src/Cat/Internal/Opposite.lagda.md b/src/Cat/Internal/Opposite.lagda.md
index 2d4bedfe1..2571ba8fb 100644
--- a/src/Cat/Internal/Opposite.lagda.md
+++ b/src/Cat/Internal/Opposite.lagda.md
@@ -1,7 +1,5 @@
 <!--
 ```agda
-open import 1Lab.Rewrite
-
 open import Cat.Prelude
 
 import Cat.Internal.Base
@@ -51,8 +49,8 @@ private
   op-ihom-involutive
     : ∀ {C₀ C₁ Γ} {src tgt : Hom C₁ C₀} {x y : Hom Γ C₀}
     → {f : Internal-hom src tgt x y}
-    → op-ihom (op-ihom f) ≡rw f
-  op-ihom-involutive = make-rewrite (Internal-hom-path refl)
+    → op-ihom (op-ihom f) ≡ f
+  op-ihom-involutive = Internal-hom-path refl
 {-# REWRITE op-ihom-involutive #-}
 ```
 -->
diff --git a/src/Cat/Monoidal/Instances/Day.lagda.md b/src/Cat/Monoidal/Instances/Day.lagda.md
index ab05a00f7..5976d5bbc 100644
--- a/src/Cat/Monoidal/Instances/Day.lagda.md
+++ b/src/Cat/Monoidal/Instances/Day.lagda.md
@@ -1,7 +1,5 @@
 <!--
 ```agda
-open import 1Lab.Rewrite
-
 open import Cat.Diagram.Coend.Sets
 open import Cat.Functor.Naturality
 open import Cat.Instances.Product
@@ -283,8 +281,8 @@ $f(\day{h,x,y})$, in a way compatible with the relation above.
 ```agda
     factor-day
       : ∀ {i a b} {W : Cowedge (Day-diagram i)} {h : Hom i (a ⊗ b)} {x : X ʻ a} {y : Y ʻ b}
-      → factor W (day h x y) ≡rw W .ψ (a , b) (h , x , y)
-    factor-day = idrw
+      → factor W (day h x y) ≡ W .ψ (a , b) (h , x , y)
+    factor-day = refl
 
   {-# REWRITE factor-day #-}
 
diff --git a/src/Data/Bool.lagda.md b/src/Data/Bool.lagda.md
index 16c1435f9..7e35a6ed8 100644
--- a/src/Data/Bool.lagda.md
+++ b/src/Data/Bool.lagda.md
@@ -19,48 +19,12 @@ open is-iso
 
 ```agda
 module Data.Bool where
-
-open import Prim.Data.Bool public
 ```
 
 # The booleans
 
-The type of booleans is interesting in homotopy type theory because it
-is the simplest type where its automorphisms in `Type`{.Agda} are
-non-trivial. In particular, there are two: negation, and the identity.
-
-But first, true isn't false.
-
 ```agda
-true≠false : ¬ true ≡ false
-true≠false p = subst P p tt where
-  P : Bool → Type
-  P false = ⊥
-  P true = ⊤
-```
-
-It's worth noting how to prove two things are **not** equal. We write a
-predicate that distinguishes them by mapping one to `⊤`{.Agda}, and one
-to `⊥`{.Agda}. Then we can substitute under P along the claimed equality
-to get an element of `⊥`{.Agda} - a contradiction.
-
-## Basic algebraic properties
-
-The booleans form a [Boolean algebra][1], as one might already expect,
-given its name. The operations required to define such a structure are
-straightforward to define using pattern matching:
-
-```agda
-not : Bool → Bool
-not true = false
-not false = true
-
-and or : Bool → Bool → Bool
-and false y = false
-and true y = y
-
-or false y = y
-or true y = true
+open import Data.Bool.Base public
 ```
 
 Pattern matching on only the first argument might seem like a somewhat inpractical choice
@@ -273,44 +237,6 @@ imp-not-or false y = refl
 imp-not-or true y = refl
 ```
 
-## Discreteness
-
-Using pattern matching, and the fact that `true isn't false`{.Agda
-ident=true≠false}, one can write an algorithm to tell whether or not two
-booleans are the same:
-
-```agda
-instance
-  Discrete-Bool : Discrete Bool
-  Discrete-Bool {false} {false} = yes refl
-  Discrete-Bool {false} {true}  = no (λ p → true≠false (sym p))
-  Discrete-Bool {true}  {false} = no true≠false
-  Discrete-Bool {true}  {true}  = yes refl
-```
-
-```agda
-opaque
-  Bool-is-set : is-set Bool
-  Bool-is-set = Discrete→is-set Discrete-Bool
-
-instance
-  H-Level-Bool : ∀ {n} → H-Level Bool (2 + n)
-  H-Level-Bool = basic-instance 2 Bool-is-set
-```
-
-Furthermore, if we know we're not looking at true, then we must be
-looking at false, and vice-versa:
-
-```agda
-x≠true→x≡false : (x : Bool) → ¬ x ≡ true → x ≡ false
-x≠true→x≡false false p = refl
-x≠true→x≡false true p = absurd (p refl)
-
-x≠false→x≡true : (x : Bool) → ¬ x ≡ false → x ≡ true
-x≠false→x≡true false p = absurd (p refl)
-x≠false→x≡true true p = refl
-```
-
 ## The "not" equivalence
 
 The construction of `not`{.Agda} as an equivalence factors through
@@ -475,21 +401,3 @@ The other case is analogous.
 The last case is when the path quacks like `ua (not, _)` - in that case,
 we use the `notLemma`{.Agda} to show it _must_ be `ua (not, _)`, and the
 univalence axiom finishes the job.
-
-<!--
-```agda
-if : ∀ {ℓ} {A : Type ℓ} → A → A → Bool → A
-if x y false = y
-if x y true = x
-
-infix 0 if_then_else_
-
-if_then_else_ : ∀ {ℓ} {A : Type ℓ} → Bool → A → A → A
-if false then t else f = f
-if true then t else f = t
-
-Bool-elim : ∀ {ℓ} (A : Bool → Type ℓ) → A true → A false → ∀ x → A x
-Bool-elim A at af true = at
-Bool-elim A at af false = af
-```
--->
diff --git a/src/Data/Bool/Base.lagda.md b/src/Data/Bool/Base.lagda.md
new file mode 100644
index 000000000..8af287c3c
--- /dev/null
+++ b/src/Data/Bool/Base.lagda.md
@@ -0,0 +1,129 @@
+<!--
+```agda
+open import 1Lab.Path.IdentitySystem
+open import 1Lab.HLevel.Closure
+open import 1Lab.Path
+open import 1Lab.Type
+
+open import Data.Dec.Base
+```
+-->
+
+```agda
+module Data.Bool.Base where
+```
+
+<!--
+```agda
+open import Prim.Data.Bool public
+```
+-->
+
+```agda
+true≠false : ¬ true ≡ false
+true≠false p = subst P p tt where
+  P : Bool → Type
+  P false = ⊥
+  P true = ⊤
+```
+
+<!--
+```agda
+false≠true : ¬ false ≡ true
+false≠true = true≠false ∘ sym
+```
+-->
+
+```agda
+not : Bool → Bool
+not true = false
+not false = true
+
+and or : Bool → Bool → Bool
+and false y = false
+and true y = y
+
+or false y = y
+or true y = true
+```
+
+```agda
+instance
+  Discrete-Bool : Discrete Bool
+  Discrete-Bool {false} {false} = yes refl
+  Discrete-Bool {false} {true}  = no false≠true
+  Discrete-Bool {true}  {false} = no true≠false
+  Discrete-Bool {true}  {true}  = yes refl
+```
+
+<!--
+```agda
+instance
+  H-Level-Bool : ∀ {n} → H-Level Bool (2 + n)
+  H-Level-Bool = basic-instance 2 (Discrete→is-set auto)
+```
+-->
+
+```agda
+x≠true→x≡false : (x : Bool) → x ≠ true → x ≡ false
+x≠true→x≡false false p = refl
+x≠true→x≡false true p = absurd (p refl)
+
+x≠false→x≡true : (x : Bool) → x ≠ false → x ≡ true
+x≠false→x≡true false p = absurd (p refl)
+x≠false→x≡true true p = refl
+```
+
+```agda
+is-true : Bool → Type
+is-true true  = ⊤
+is-true false = ⊥
+
+record So (b : Bool) : Type where
+  field
+    is-so : is-true b
+
+pattern oh = record { is-so = tt }
+```
+
+<!--
+```agda
+¬so-false : So false → ⊥
+¬so-false ()
+
+oh? : ∀ x → Dec (So x)
+oh? true = yes oh
+oh? false = no λ ()
+
+not-so : ∀ {x} → ¬ So x → So (not x)
+not-so {true} ¬p = absurd (¬p oh)
+not-so {false} p = oh
+
+instance
+  H-Level-So : ∀ {x n} → H-Level (So x) (suc n)
+  H-Level-So {false} = prop-instance λ ()
+  H-Level-So {true} = prop-instance λ where
+    oh oh → refl
+
+  Dec-So : ∀ {x} → Dec (So x)
+  Dec-So = oh? _
+```
+-->
+
+<!--
+```agda
+if : ∀ {ℓ} {A : Type ℓ} → A → A → Bool → A
+if x y false = y
+if x y true = x
+
+infix 0 if_then_else_
+
+if_then_else_ : ∀ {ℓ} {A : Type ℓ} → Bool → A → A → A
+if false then t else f = f
+if true then t else f = t
+
+Bool-elim : ∀ {ℓ} (A : Bool → Type ℓ) → A true → A false → ∀ x → A x
+Bool-elim A at af true = at
+Bool-elim A at af false = af
+```
+-->
diff --git a/src/Data/Dec/Base.lagda.md b/src/Data/Dec/Base.lagda.md
index 4ccd371bf..79b0b0b8a 100644
--- a/src/Data/Dec/Base.lagda.md
+++ b/src/Data/Dec/Base.lagda.md
@@ -47,9 +47,11 @@ Dec-rec = Dec-elim _
 ```agda
 recover : ∀ {ℓ} {A : Type ℓ} ⦃ d : Dec A ⦄ → .A → A
 recover ⦃ yes x ⦄ _ = x
-recover {A = A} ⦃ no ¬x ⦄ x = go (¬x x) where
-  go : .⊥ → A
-  go ()
+recover ⦃ no ¬x ⦄ x = absurd (¬x x)
+
+dec→dne : ∀ {ℓ} {A : Type ℓ} ⦃ d : Dec A ⦄ → ¬ ¬ A → A
+dec→dne ⦃ yes x ⦄ _   = x
+dec→dne ⦃ no ¬x ⦄ ¬¬x = absurd (¬¬x ¬x)
 ```
 -->
 
diff --git a/src/Data/Fin/Base.lagda.md b/src/Data/Fin/Base.lagda.md
index d1c24c44b..2efc4e27a 100644
--- a/src/Data/Fin/Base.lagda.md
+++ b/src/Data/Fin/Base.lagda.md
@@ -187,6 +187,10 @@ Fin-elim
 Fin-elim P pfzero pfsuc fzero = pfzero
 Fin-elim P pfzero pfsuc (fsuc x) = pfsuc x (Fin-elim P pfzero pfsuc x)
 
+fin-cons : ∀ {ℓ} {n} {P : Fin (suc n) → Type ℓ} → P 0 → (∀ x → P (fsuc x)) → ∀ x → P x
+fin-cons p0 ps fzero = p0
+fin-cons p0 ps (fsuc x) = ps x
+
 fin-absurd : Fin 0 → ⊥
 fin-absurd ()
 ```
@@ -203,11 +207,11 @@ sets.
 ```agda
 _≤_ : ∀ {n} → Fin n → Fin n → Type
 i ≤ j = to-nat i Nat.≤ to-nat j
-infix 3 _≤_
+infix 7 _≤_
 
 _<_ : ∀ {n} → Fin n → Fin n → Type
 i < j = to-nat i Nat.< to-nat j
-infix 3 _<_
+infix 7 _<_
 ```
 
 Next, we define a pair of functions `squish`{.Agda} and `skip`{.Agda},
@@ -240,7 +244,7 @@ $n$ values of $\bb{N}$.
 
 ```agda
 ℕ< : Nat → Type
-ℕ< x = Σ[ n ∈ Nat ] (n Nat.< x)
+ℕ< x = Σ[ n ∈ Nat ] n Nat.< x
 
 from-ℕ< : ∀ {n} → ℕ< n → Fin n
 from-ℕ< {n = suc n} (zero , q) = fzero
@@ -271,7 +275,7 @@ split-+ {m = zero} i = inr i
 split-+ {m = suc m} fzero = inl fzero
 split-+ {m = suc m} (fsuc i) = ⊎-map fsuc id (split-+ i)
 
-avoid : ∀ {n} (i j : Fin (suc n)) → (¬ i ≡ j) → Fin n
+avoid : ∀ {n} (i j : Fin (suc n)) → i ≠ j → Fin n
 avoid fzero fzero i≠j = absurd (i≠j refl)
 avoid {n = suc n} fzero (fsuc j) i≠j = j
 avoid {n = suc n} (fsuc i) fzero i≠j = fzero
diff --git a/src/Data/Fin/Properties.lagda.md b/src/Data/Fin/Properties.lagda.md
index 1c6da5354..e9e37fed9 100644
--- a/src/Data/Fin/Properties.lagda.md
+++ b/src/Data/Fin/Properties.lagda.md
@@ -3,6 +3,7 @@
 open import 1Lab.Prelude
 
 open import Data.Fin.Base
+open import Data.Nat.Base using (s≤s)
 open import Data.Dec
 open import Data.Sum
 
@@ -167,7 +168,7 @@ Fin≃ℕ< : ∀ {n} → Fin n ≃ ℕ< n
 Fin≃ℕ< {n} = to-ℕ< , is-iso→is-equiv (iso from-ℕ< (to-from-ℕ< {n}) from-to-ℕ<)
 
 avoid-injective
-  : ∀ {n} (i : Fin (suc n)) {j k : Fin (suc n)} {i≠j : ¬ i ≡ j} {i≠k : ¬ i ≡ k}
+  : ∀ {n} (i : Fin (suc n)) {j k : Fin (suc n)} {i≠j : i ≠ j} {i≠k : i ≠ k}
   → avoid i j i≠j ≡ avoid i k i≠k → j ≡ k
 avoid-injective fzero {fzero} {k} {i≠j} p = absurd (i≠j refl)
 avoid-injective fzero {fsuc j} {fzero} {i≠k = i≠k} p = absurd (i≠k refl)
@@ -191,8 +192,7 @@ Fin-suc-Π
 Fin-suc-Π = Iso→Equiv λ where
   .fst f → f fzero , (λ x → f (fsuc x))
 
-  .snd .is-iso.inv (z , f) fzero    → z
-  .snd .is-iso.inv (z , f) (fsuc x) → f x
+  .snd .is-iso.inv (z , s) → fin-cons z s
 
   .snd .is-iso.rinv x → refl
 
@@ -287,17 +287,48 @@ $\Pi$-types and $\Sigma$-types, respectively.
 
 ```agda
 instance
-  Fin-exhaustible
+  Dec-Fin-∀
     : ∀ {n ℓ} {A : Fin n → Type ℓ}
     → ⦃ ∀ {x} → Dec (A x) ⦄ → Dec (∀ x → A x)
-  Fin-exhaustible {n} ⦃ d ⦄ = Fin-Monoidal n λ _ → d
+  Dec-Fin-∀ {n} ⦃ d ⦄ = Fin-Monoidal n (λ _ → d)
 
-  Fin-omniscient
+  Dec-Fin-Σ
     : ∀ {n ℓ} {A : Fin n → Type ℓ}
     → ⦃ ∀ {x} → Dec (A x) ⦄ → Dec (Σ (Fin n) A)
-  Fin-omniscient {n} ⦃ d ⦄ = Fin-Alternative n λ _ → d
+  Dec-Fin-Σ {n} ⦃ d ⦄ = Fin-Alternative n λ _ → d
 ```
 
+```agda
+Fin-omniscience
+  : ∀ {n ℓ} (P : Fin n → Type ℓ) ⦃ _ : ∀ {x} → Dec (P x) ⦄
+  → (Σ[ j ∈ Fin n ] P j × ∀ k → P k → j ≤ k) ⊎ (∀ x → ¬ P x)
+Fin-omniscience {zero} P = inr λ ()
+Fin-omniscience {suc n} P with holds? (P 0)
+... | yes here = inl (0 , here , λ _ _ → 0≤x)
+... | no ¬here with Fin-omniscience (P ∘ fsuc)
+... | inl (ix , pix , least) = inl (fsuc ix , pix , fin-cons (λ here → absurd (¬here here)) λ i pi → Nat.s≤s (least i pi))
+... | inr nowhere = inr (fin-cons ¬here nowhere)
+```
+
+<!--
+```agda
+Fin-omniscience-neg
+  : ∀ {n ℓ} (P : Fin n → Type ℓ) ⦃ _ : ∀ {x} → Dec (P x) ⦄
+  → (∀ x → P x) ⊎ (Σ[ j ∈ Fin n ] ¬ P j × ∀ k → ¬ P k → j ≤ k)
+Fin-omniscience-neg P with Fin-omniscience (¬_ ∘ P)
+... | inr p = inl λ i → dec→dne (p i)
+... | inl (j , ¬pj , least) = inr (j , ¬pj , least)
+
+Fin-find
+  : ∀ {n ℓ} {P : Fin n → Type ℓ} ⦃ _ : ∀ {x} → Dec (P x) ⦄
+  → ¬ (∀ x → P x)
+  → Σ[ x ∈ Fin n ] ¬ P x × ∀ y → ¬ P y → x ≤ y
+Fin-find {P = P} ¬p with Fin-omniscience-neg P
+... | inl p = absurd (¬p p)
+... | inr p = p
+```
+-->
+
 ## Injections and surjections
 
 The standard finite sets are **Dedekind-finite**, which means that every
@@ -347,7 +378,7 @@ avoid-insert
   → (ρ : Fin n → A)
   → (i : Fin (suc n)) (a : A)
   → (j : Fin (suc n))
-  → (i≠j : ¬ i ≡ j)
+  → (i≠j : i ≠ j)
   → (ρ [ i ≔ a ]) j ≡ ρ (avoid i j i≠j)
 avoid-insert {n = n} ρ fzero a fzero i≠j = absurd (i≠j refl)
 avoid-insert {n = suc n} ρ fzero a (fsuc j) i≠j = refl
diff --git a/src/Data/Id/Base.lagda.md b/src/Data/Id/Base.lagda.md
index 0959b0190..d04d442a3 100644
--- a/src/Data/Id/Base.lagda.md
+++ b/src/Data/Id/Base.lagda.md
@@ -6,7 +6,6 @@ open import 1Lab.Path.IdentitySystem
 open import 1Lab.HLevel.Closure
 open import 1Lab.Type.Sigma
 open import 1Lab.Univalence
-open import 1Lab.Rewrite
 open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path
@@ -114,13 +113,13 @@ opaque
   _≡ᵢ?_ : ∀ {ℓ} {A : Type ℓ} ⦃ _ : Discrete A ⦄ (x y : A) → Dec (x ≡ᵢ y)
   x ≡ᵢ? y = discrete-id (x ≡? y)
 
-  ≡ᵢ?-default : ∀ {ℓ} {A : Type ℓ} {x y : A} {d : Discrete A} → (_≡ᵢ?_ ⦃ d ⦄ x y) ≡rw discrete-id d
-  ≡ᵢ?-default = make-rewrite refl
+  ≡ᵢ?-default : ∀ {ℓ} {A : Type ℓ} {x y : A} {d : Discrete A} → (_≡ᵢ?_ ⦃ d ⦄ x y) ≡ discrete-id d
+  ≡ᵢ?-default = refl
 
-  ≡ᵢ?-yes : ∀ {ℓ} {A : Type ℓ} {x : A} {d : Discrete A} → (_≡ᵢ?_ ⦃ d ⦄ x x) ≡rw yes reflᵢ
-  ≡ᵢ?-yes {d = d} = make-rewrite (case d return (λ d → discrete-id d ≡ yes reflᵢ) of λ where
+  ≡ᵢ?-yes : ∀ {ℓ} {A : Type ℓ} {x : A} {d : Discrete A} → (_≡ᵢ?_ ⦃ d ⦄ x x) ≡ yes reflᵢ
+  ≡ᵢ?-yes {d = d} = case d return (λ d → discrete-id d ≡ yes reflᵢ) of λ where
     (yes a) → ap yes (is-set→is-setᵢ (Discrete→is-set d) _ _ _ _)
-    (no ¬a) → absurd (¬a refl))
+    (no ¬a) → absurd (¬a refl)
 
 {-# REWRITE ≡ᵢ?-default ≡ᵢ?-yes #-}
 
diff --git a/src/Data/Int/HIT.lagda.md b/src/Data/Int/HIT.lagda.md
index 02df4c096..49b2efed7 100644
--- a/src/Data/Int/HIT.lagda.md
+++ b/src/Data/Int/HIT.lagda.md
@@ -1,7 +1,6 @@
 <!--
 ```agda
 open import 1Lab.Prelude
-open import 1Lab.Rewrite
 
 open import Data.Nat.Solver
 open import Data.Dec
@@ -781,10 +780,9 @@ instance
   Discrete-Int : Discrete Int
   Discrete-Int = go _ _ where
     go₀ : (a b x y : Nat) → Dec (diff a b ≡ diff x y)
-    go₀ a b x y with inspect (a + y == b + x)
-    ... | true , p  = yes (same-difference (is-equal→path {a + y} {b + x} p))
-    ... | false , p = no λ q → is-not-equal→not-path
-      {a + y} {b + x} p (ℤ-Path.encode a b (diff x y) q)
+    go₀ a b x y with a + y ≡? b + x
+    ... | yes p  = yes (same-difference p)
+    ... | no ¬p = no λ ab → ¬p (ℤ-Path.encode a b (diff x y) ab)
 
     go₁ : (a b : Nat) (y : Int) → Dec (diff a b ≡ y)
     go₁ a b (diff x y) = go₀ a b x y
diff --git a/src/Data/List/Base.lagda.md b/src/Data/List/Base.lagda.md
index c3eca4509..4dfbaedee 100644
--- a/src/Data/List/Base.lagda.md
+++ b/src/Data/List/Base.lagda.md
@@ -139,7 +139,7 @@ _++_ : ∀ {ℓ} {A : Type ℓ} → List A → List A → List A
 []       ++ ys = ys
 (x ∷ xs) ++ ys = x ∷ (xs ++ ys)
 
-infixr 5 _++_
+infixr 8 _++_
 
 instance
   Append-List : ∀ {ℓ} {A : Type ℓ} → Append (List A)
@@ -164,6 +164,10 @@ count : Nat → List Nat
 count zero = []
 count (suc n) = 0 ∷ map suc (count n)
 
+product : List Nat → Nat
+product [] = 1
+product (x ∷ xs) = x * product xs
+
 reverse : List A → List A
 reverse = go [] where
   go : List A → List A → List A
diff --git a/src/Data/List/Properties.lagda.md b/src/Data/List/Properties.lagda.md
index eaa7d0cc4..7354da83c 100644
--- a/src/Data/List/Properties.lagda.md
+++ b/src/Data/List/Properties.lagda.md
@@ -160,7 +160,6 @@ map-++
 map-++ f [] ys = refl
 map-++ f (x ∷ xs) ys = ap (f x ∷_) (map-++ f xs ys)
 
-
 take-length : ∀ {ℓ} {A : Type ℓ} (xs : List A) → take (length xs) xs ≡ xs
 take-length [] = refl
 take-length (x ∷ xs) = ap (x ∷_) (take-length xs)
diff --git a/src/Data/List/Quantifiers.lagda.md b/src/Data/List/Quantifiers.lagda.md
index 017d0cb69..43dd165d6 100644
--- a/src/Data/List/Quantifiers.lagda.md
+++ b/src/Data/List/Quantifiers.lagda.md
@@ -82,7 +82,7 @@ All-rec n e (p ∷ a) = e p (e p n)
 ∷-all-× : All P (x ∷ xs) → P x × All P xs
 ∷-all-× (px ∷ pxs) = px , pxs
 
-¬some-[] : ¬ (Some P [])
+¬some-[] : ¬ Some P []
 ¬some-[] ()
 
 ∷-some-⊎ : Some P (x ∷ xs) → P x ⊎ Some P xs
@@ -158,4 +158,21 @@ instance
 all-∈ : All P xs → x ∈ xs → P x
 all-∈ {P = P} (px ∷ pxs) (here p) = subst P (sym p) px
 all-∈ (px ∷ pxs) (there x∈xs) = all-∈ pxs x∈xs
+
+to-all : (∀ x → x ∈ xs → P x) → All P xs
+to-all {xs = []} p = []
+to-all {xs = x ∷ xs} p = p x (here refl) ∷ to-all (λ i w → p i (there w))
 ```
+
+<!--
+```agda
+instance
+  H-Level-All : ∀ {ℓ ℓ'} {A : Type ℓ} {P : A → Type ℓ'} {n} ⦃ _ : ∀ {x} → H-Level (P x) n ⦄ {xs} → H-Level (All P xs) n
+  H-Level-All {P = P} {xs = xs} = hlevel-instance
+    (retract→is-hlevel {A = ∀ x → x ∈ₗ xs → P x} _ to-all (λ a _ → all-∈ a) inv (hlevel _))
+    where
+      inv : ∀ {xs} → is-left-inverse (to-all {xs = xs} {P = P}) (λ a z → all-∈ a)
+      inv {xs} [] = refl
+      inv {x ∷ xs} (y ∷ ys) i = coe1→i (λ _ → P x) i y ∷ inv ys i
+```
+-->
diff --git a/src/Data/Nat/Base.lagda.md b/src/Data/Nat/Base.lagda.md
index 9da4870d7..410ae8cdc 100644
--- a/src/Data/Nat/Base.lagda.md
+++ b/src/Data/Nat/Base.lagda.md
@@ -6,8 +6,8 @@ open import 1Lab.HLevel
 open import 1Lab.Path
 open import 1Lab.Type
 
+open import Data.Bool.Base
 open import Data.Dec.Base
-open import Data.Bool
 ```
 -->
 
@@ -104,23 +104,28 @@ private module _ where private
 
 <!--
 ```agda
-is-equal→path : ∀ {x y} → (x == y) ≡ true → x ≡ y
-is-equal→path {zero}  {zero}  p = refl
-is-equal→path {zero}  {suc y} p = absurd (true≠false (sym p))
-is-equal→path {suc x} {zero}  p = absurd (true≠false (sym p))
-is-equal→path {suc x} {suc y} p = ap suc (is-equal→path p)
+abstract
+  from-prim-eq : ∀ {x y} → So (x == y) → x ≡ y
+  from-prim-eq {zero}  {zero}  p = refl
+  from-prim-eq {suc x} {suc y} p = ap suc (from-prim-eq p)
 
-is-not-equal→not-path : ∀ {x y} → (x == y) ≡ false → ¬ (x ≡ y)
-is-not-equal→not-path {zero}  {zero}  p q = absurd (true≠false p)
-is-not-equal→not-path {zero}  {suc y} p q = absurd (zero≠suc q)
-is-not-equal→not-path {suc x} {zero}  p q = absurd (zero≠suc (sym q))
-is-not-equal→not-path {suc x} {suc y} p q = is-not-equal→not-path p (suc-inj q)
+  from-prim-eq-refl : ∀ {x p} → from-prim-eq {x} {x} p ≡ refl
+  from-prim-eq-refl {zero} = refl
+  from-prim-eq-refl {suc x} = ap (ap suc) (from-prim-eq-refl {x})
+
+  {-# REWRITE from-prim-eq-refl #-}
+
+  to-prim-eq : ∀ {x y} → x ≡ y → So (x == y)
+  to-prim-eq {zero} {zero} p = oh
+  to-prim-eq {zero} {suc y} p = absurd (zero≠suc p)
+  to-prim-eq {suc x} {zero} p = absurd (suc≠zero p)
+  to-prim-eq {suc x} {suc y} p = to-prim-eq (suc-inj p)
 
 instance
   Discrete-Nat : Discrete Nat
-  Discrete-Nat {x} {y} with inspect (x == y)
-  ... | true  , p = yes (is-equal→path p)
-  ... | false , p = no  (is-not-equal→not-path p)
+  Discrete-Nat {x} {y} with oh? (x == y)
+  ... | yes p = yes (from-prim-eq p)
+  ... | no ¬p = no (¬p ∘ to-prim-eq)
 ```
 -->
 
@@ -181,7 +186,7 @@ _^_ : Nat → Nat → Nat
 x ^ zero = 1
 x ^ suc y = x * (x ^ y)
 
-infixr 8 _^_
+infixr 10 _^_
 ```
 
 ## Ordering
@@ -215,8 +220,7 @@ instance
   {-# INCOHERENT x≤x x≤sucy #-}
 
 Positive : Nat → Type
-Positive zero    = ⊥
-Positive (suc n) = ⊤
+Positive n = 1 ≤ n
 ```
 -->
 
@@ -226,7 +230,7 @@ re-using the definition of `_≤_`{.Agda}.
 ```agda
 _<_ : Nat → Nat → Type
 m < n = suc m ≤ n
-infix 3 _<_ _≤_
+infix 7 _<_ _≤_
 ```
 
 As an "ordering combinator", we can define the _maximum_ of two natural
diff --git a/src/Data/Nat/DivMod.lagda.md b/src/Data/Nat/DivMod.lagda.md
index 08e03d0fe..6009ce464 100644
--- a/src/Data/Nat/DivMod.lagda.md
+++ b/src/Data/Nat/DivMod.lagda.md
@@ -46,9 +46,18 @@ The easy case is to divide zero by anything, in which case the result is
 zero with remainder zero. The more interesting case comes when we have
 some successor, and we want to divide it.
 
+<!--
 ```agda
-divide-pos : ∀ a b → .⦃ _ : Positive b ⦄ → DivMod a b
-divide-pos zero (suc b) = divmod 0 0 refl (s≤s 0≤x)
+module _ where private
+-- This is a nice explanation of the division algorithm but it ends up
+-- being extremely slow when compared to the builtins. So we define the
+-- nice prosaic version first, then define the fast version hidden..
+```
+-->
+
+```agda
+  divide-pos : ∀ a b → .⦃ _ : Positive b ⦄ → DivMod a b
+  divide-pos zero (suc b) = divmod 0 0 refl (s≤s 0≤x)
 ```
 
 It suffices to assume --- since $a$ is smaller than $1+a$ --- that we
@@ -57,8 +66,8 @@ ordering on $\NN$ is trichotomous, we can proceed by cases on whether
 $(1 + r') < b$.
 
 ```agda
-divide-pos (suc a) b with divide-pos a b
-divide-pos (suc a) b | divmod q' r' p s with ≤-split (suc r') b
+  divide-pos (suc a) b with divide-pos a b
+  divide-pos (suc a) b | divmod q' r' p s with ≤-split (suc r') b
 ```
 
 First, suppose that $1 + r' < b$, i.e., $1 + r'$ _can_ serve as a
@@ -70,8 +79,8 @@ $$
 $$
 
 ```agda
-divide-pos (suc a) b | divmod q' r' p s | inl r'+1<b =
-  divmod q' (suc r') (ap suc p ∙ sym (+-sucr (q' * b) r')) r'+1<b
+  divide-pos (suc a) b | divmod q' r' p s | inl r'+1<b =
+    divmod q' (suc r') (ap suc p ∙ sym (+-sucr (q' * b) r')) r'+1<b
 ```
 
 The other case --- that in which $1 + r' = b$ --- is more interesting.
@@ -81,14 +90,14 @@ in this case, $q = 1 + q'$ and $r = 0$, which works out because ($0 < b$
 and) of some arithmetic. See for yourself:
 
 ```agda
-divide-pos (suc a) (suc b') | divmod q' r' p s | inr (inr r'+1=b) =
-  divmod (suc q') 0
-    ( suc a                           ≡⟨ ap suc p ⟩
-      suc (q' * (suc b') + r')        ≡˘⟨ ap (λ e → suc (q' * e + r')) r'+1=b ⟩
-      suc (q' * (suc r') + r')        ≡⟨ nat! ⟩
-      suc (r' + q' * (suc r') + zero) ≡⟨ ap (λ e → e + q' * e + 0) r'+1=b ⟩
-      (suc b') + q' * (suc b') + 0    ∎ )
-    (s≤s 0≤x)
+  divide-pos (suc a) (suc b') | divmod q' r' p s | inr (inr r'+1=b) =
+    divmod (suc q') 0
+      ( suc a                           ≡⟨ ap suc p ⟩
+        suc (q' * (suc b') + r')        ≡˘⟨ ap (λ e → suc (q' * e + r')) r'+1=b ⟩
+        suc (q' * (suc r') + r')        ≡⟨ nat! ⟩
+        suc (r' + q' * (suc r') + zero) ≡⟨ ap (λ e → e + q' * e + 0) r'+1=b ⟩
+        (suc b') + q' * (suc b') + 0    ∎ )
+      (s≤s 0≤x)
 ```
 
 Note that we actually have one more case to consider -- or rather,
@@ -96,9 +105,9 @@ discard -- that in which $b < 1 + r'$. It's impossible because, by the
 definition of division, we have $r' < b$, meaning $(1 + r') \le b$.
 
 ```agda
-divide-pos (suc a) (suc b') | divmod q' r' p s | inr (inl b<r'+1) =
-  absurd (<-not-equal b<r'+1
-    (≤-antisym (≤-sucr (≤-peel b<r'+1)) (recover s)))
+  divide-pos (suc a) (suc b') | divmod q' r' p s | inr (inl b<r'+1) =
+    absurd (<-not-equal b<r'+1
+      (≤-antisym (≤-sucr (≤-peel b<r'+1)) (recover s)))
 ```
 
 As a finishing touch, we define short operators to produce the result of
@@ -108,26 +117,75 @@ degree of freedom when defining $x/0$ and $x \% 0$. The canonical choice
 is to yield $0$ in both cases.
 
 ```agda
-_%_ : Nat → Nat → Nat
-a % zero = zero
-a % suc b = divide-pos a (suc b) .DivMod.rem
+  _%_ : Nat → Nat → Nat
+  a % zero = zero
+  a % suc b = divide-pos a (suc b) .DivMod.rem
 
-_/ₙ_ : Nat → Nat → Nat
-a /ₙ zero = zero
-a /ₙ suc b = divide-pos a (suc b) .DivMod.quot
+  _/ₙ_ : Nat → Nat → Nat
+  a /ₙ zero = zero
+  a /ₙ suc b = divide-pos a (suc b) .DivMod.quot
 
-is-divmod : ∀ x y → .⦃ _ : Positive y ⦄ → x ≡ (x /ₙ y) * y + x % y
-is-divmod x (suc y) with divide-pos x (suc y)
-... | divmod q r α β = recover α
+  is-divmod : ∀ x y → .⦃ _ : Positive y ⦄ → x ≡ (x /ₙ y) * y + x % y
+  is-divmod x (suc y) with divide-pos x (suc y)
+  ... | divmod q r α β = recover α
 
-x%y<y : ∀ x y → .⦃ _ : Positive y ⦄ → (x % y) < y
-x%y<y x (suc y) with divide-pos x (suc y)
-... | divmod q r α β = recover β
+  x%y<y : ∀ x y → .⦃ _ : Positive y ⦄ → (x % y) < y
+  x%y<y x (suc y) with divide-pos x (suc y)
+  ... | divmod q r α β = recover β
 ```
 
 With this, we can decide whether two numbers divide each other by
 checking whether the remainder is zero!
 
+<!--
+```agda
+mod-helper : (k m n j : Nat) → Nat
+mod-helper k m  zero    j      = k
+mod-helper k m (suc n)  zero   = mod-helper 0       m n m
+mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j
+
+div-helper : (k m n j : Nat) → Nat
+div-helper k m  zero    j      = k
+div-helper k m (suc n)  zero   = div-helper (suc k) m n m
+div-helper k m (suc n) (suc j) = div-helper k       m n j
+
+{-# BUILTIN NATDIVSUCAUX div-helper #-}
+{-# BUILTIN NATMODSUCAUX mod-helper #-}
+
+-- _ = {! mod-helper 0 0 4294967296 2  !}
+
+_/ₙ_ : (d1 d2 : Nat) .⦃ _ : Positive d2 ⦄ → Nat
+d1 /ₙ suc d2 = div-helper 0 d2 d1 d2
+
+_%_ : (d1 d2 : Nat) .⦃ _ : Positive d2 ⦄ → Nat
+d1 % suc d2 = mod-helper 0 d2 d1 d2
+
+abstract
+  private
+    div-mod-lemma : ∀ am ad d n → am + ad * suc (am + n) + d ≡ mod-helper am (am + n) d n + div-helper ad (am + n) d n * suc (am + n)
+    div-mod-lemma am ad zero n = +-zeror _
+    div-mod-lemma am ad (suc d) zero rewrite Id≃path.from (+-zeror am) = +-sucr _ d ∙ div-mod-lemma zero (suc ad) d am
+    div-mod-lemma am ad (suc d) (suc n) rewrite Id≃path.from (+-sucr am n) = +-sucr _ d ∙ div-mod-lemma (suc am) ad d n
+
+    mod-le : ∀ a d n → mod-helper a (a + n) d n ≤ a + n
+    mod-le a zero n = +-≤l a n
+    mod-le a (suc d) zero = mod-le zero d (a + 0)
+    mod-le a (suc d) (suc n) rewrite Id≃path.from (+-sucr a n) = mod-le (suc a) d n
+
+  is-divmod : ∀ x y → .⦃ _ : Positive y ⦄ → x ≡ (x /ₙ y) * y + x % y
+  is-divmod x (suc y) = div-mod-lemma 0 0 x y ∙ +-commutative (x % (suc y)) _
+
+  x%y<y : ∀ x y → .⦃ _ : Positive y ⦄ → (x % y) < y
+  x%y<y x (suc y) = s≤s (mod-le 0 x y)
+
+from-fast-mod : ∀ d1 d2 .⦃ _ : Positive d2 ⦄ → d1 % d2 ≡ 0 → d2 ∣ d1
+from-fast-mod d1 d2 p = fibre→∣ (d1 /ₙ d2 , sym (is-divmod d1 d2 ∙ ap (d1 /ₙ d2 * d2 +_) p ∙ +-zeror _))
+
+divide-pos : ∀ a b → .⦃ _ : Positive b ⦄ → DivMod a b
+divide-pos a b = divmod (a /ₙ b) (a % b) (is-divmod a b) (x%y<y a b)
+```
+-->
+
 ```agda
 instance
   Dec-∣ : ∀ {n m} → Dec (n ∣ m)
@@ -138,5 +196,5 @@ instance
     let
       n∣r : (q' - q) * n ≡ r
       n∣r = monus-distribr q' q n ∙ sym (monus-swapl _ _ _ (sym (p ∙ recover α)))
-    in <-≤-asym (recover β) (m∣sn→m≤sn (q' - q , n∣r))
+    in <-≤-asym (recover β) (m∣sn→m≤sn (q' - q , recover n∣r))
 ```
diff --git a/src/Data/Nat/Divisible.lagda.md b/src/Data/Nat/Divisible.lagda.md
index 1408a1a57..b6fefa833 100644
--- a/src/Data/Nat/Divisible.lagda.md
+++ b/src/Data/Nat/Divisible.lagda.md
@@ -34,7 +34,7 @@ _∣_ : Nat → Nat → Type
 zero  ∣ y = y ≡ zero
 suc x ∣ y = fibre (_* suc x) y
 
-infix 5 _∣_
+infix 7 _∣_
 ```
 
 In this way, we break the pathological case of $0 | 0$ by _decreeing_ it
@@ -117,6 +117,14 @@ m∣sn→m≤sn : ∀ {x y} → x ∣ suc y → x ≤ suc y
 m∣sn→m≤sn {x} {y} p with ∣→fibre p
 ... | zero  , p = absurd (zero≠suc p)
 ... | suc k , p = difference→≤ (k * x) p
+
+m∣n→m≤n : ∀ {m n} .⦃ _ : Positive n ⦄ → m ∣ n → m ≤ n
+m∣n→m≤n {n = suc _} = m∣sn→m≤sn
+
+proper-divisor-< : ∀ {m n} .⦃ _ : Positive n ⦄ → m ≠ n → m ∣ n → m < n
+proper-divisor-< m≠n m∣n with ≤-strengthen (m∣n→m≤n m∣n)
+... | inl here  = absurd (m≠n here)
+... | inr there = there
 ```
 
 This will let us establish the antisymmetry we were looking for:
@@ -139,6 +147,9 @@ expect a number to divide its multiples. Fortunately, this is the case:
 
 ∣-*r : ∀ {x y} → x ∣ y * x
 ∣-*r {y = y} = fibre→∣ (y , refl)
+
+|-*l-pres : ∀ {n a b} → n ∣ b → n ∣ a * b
+|-*l-pres {n} {a} {b} p1 with (q , α) ← ∣→fibre p1 = fibre→∣ (a * q , *-associative a q n ∙ ap (a *_) α)
 ```
 
 If two numbers are multiples of $k$, then so is their sum.
@@ -147,6 +158,22 @@ If two numbers are multiples of $k$, then so is their sum.
 ∣-+ : ∀ {k n m} → k ∣ n → k ∣ m → k ∣ (n + m)
 ∣-+ {zero} {n} {m} p q = ap (_+ m) p ∙ q
 ∣-+ {suc k} (x , p) (y , q) = x + y , *-distrib-+r x y (suc k) ∙ ap₂ _+_ p q
+
+∣-+-cancel : ∀ {n a b} → n ∣ a → n ∣ a + b → n ∣ b
+∣-+-cancel {n} {a} {b} p1 p2 with (q , α) ← ∣→fibre p1 | (r , β) ← ∣→fibre p2 = fibre→∣
+  (r - q , monus-distribr r q n ∙ ap₂ _-_ β α ∙ ap ((a + b) -_) (sym (+-zeror a)) ∙ monus-cancell a b 0)
+
+∣-+-cancel' : ∀ {n a b} → n ∣ b → n ∣ a + b → n ∣ a
+∣-+-cancel' {n} {a} {b} p1 p2 = ∣-+-cancel {n} {b} {a} p1 (subst (n ∣_) (+-commutative a b) p2)
+```
+
+The only number that divides 1 is 1 itself:
+
+```agda
+∣-1 : ∀ {n} → n ∣ 1 → n ≡ 1
+∣-1 {0} p = sym p
+∣-1 {1} p = refl
+∣-1 {suc (suc n)} (k , p) = *-is-oner k (2 + n) p
 ```
 
 ## Even and odd numbers
diff --git a/src/Data/Nat/Divisible/GCD.lagda.md b/src/Data/Nat/Divisible/GCD.lagda.md
index 8309217f9..5eb910793 100644
--- a/src/Data/Nat/Divisible/GCD.lagda.md
+++ b/src/Data/Nat/Divisible/GCD.lagda.md
@@ -8,6 +8,7 @@ open import Data.Nat.Properties
 open import Data.Nat.Divisible
 open import Data.Nat.DivMod
 open import Data.Nat.Order
+open import Data.Dec.Base
 open import Data.Nat.Base
 open import Data.Sum.Base
 ```
@@ -191,3 +192,43 @@ is-gcd-graphs-gcd {m = m} {n} {d} = prop-ext!
   (λ x → ap fst $ GCD-is-prop (gcd m n , Euclid.euclid m n .snd) (d , x))
   (λ p → subst (is-gcd m n) p (Euclid.euclid m n .snd))
 ```
+
+## Euclid's lemma
+
+```agda
+|-*-coprime-cancel
+  : ∀ n a b .⦃ _ : Positive n ⦄ .⦃ _ : Positive a ⦄
+  → n ∣ a * b → is-gcd n a 1 → n ∣ b
+|-*-coprime-cancel n a b div coprime = done where
+  E : Nat → Prop lzero
+  E x = el! (0 < x × n ∣ x * b)
+
+  has : Σ[ x ∈ Nat ] ((x ∈ E) × (∀ y → (0 < y) × (n ∣ y * b) → x ≤ y))
+  has = ℕ-well-ordered {P = E} (λ _ → auto) (inc (a , recover auto , div))
+
+  instance
+    _ : Positive (has .fst)
+    _ = has .snd .fst .fst
+
+  step : ∀ x → x ∈ E → has .fst ∣ x
+  step x (xe , d) with divmod q r α β ← divide-pos x (has .fst) =
+    let
+      d' : n ∣ (q * has .fst * b + r * b)
+      d' = subst (n ∣_) (ap (_* b) (recover α) ∙ *-distrib-+r (q * has .fst) r b) d
+
+      d'' : n ∣ r * b
+      d'' = ∣-+-cancel {n} {q * has .fst * b} {r * b} (subst (n ∣_) (sym (*-associative q (has .fst) b)) (|-*l-pres {a = q} (has .snd .fst .snd))) d'
+    in case r ≡? 0 of λ where
+      (yes p) → fibre→∣ (q , sym (recover α ∙ ap (q * has .fst +_) p ∙ +-zeror (q * has .fst)))
+      (no ¬p) → absurd (<-irrefl
+        (≤-antisym (≤-trans ≤-ascend (recover β)) (has .snd .snd r (nonzero→positive ¬p , d'')))
+        (recover β))
+
+  almost : has .fst ≡ 1
+  almost = ∣-1 $ coprime .greatest {has .fst}
+    (step n (recover auto , ∣-*l))
+    (step a (recover auto , div))
+
+  done : n ∣ b
+  done = subst (n ∣_) (ap (_* b) almost ∙ *-onel b) (has .snd .fst .snd)
+```
diff --git a/src/Data/Nat/Order.lagda.md b/src/Data/Nat/Order.lagda.md
index f47d58b8a..5d4186564 100644
--- a/src/Data/Nat/Order.lagda.md
+++ b/src/Data/Nat/Order.lagda.md
@@ -2,9 +2,12 @@
 ```agda
 open import 1Lab.Prelude
 
+open import Data.Bool.Base
 open import Data.Dec.Base
 open import Data.Nat.Base
 open import Data.Sum
+
+import Prim.Data.Nat as Prim
 ```
 -->
 
@@ -28,7 +31,19 @@ naturals automatically.
 ≤-refl : ∀ {x : Nat} → x ≤ x
 ≤-refl {zero}  = 0≤x
 ≤-refl {suc x} = s≤s ≤-refl
+```
+
+<!--
+```agda
+≤-refl' : ∀ {x y} → x ≡ y → x ≤ y
+≤-refl' {zero} {zero} p = 0≤x
+≤-refl' {zero} {suc y} p = absurd (zero≠suc p)
+≤-refl' {suc x} {zero} p = absurd (suc≠zero p)
+≤-refl' {suc x} {suc y} p = s≤s (≤-refl' (suc-inj p))
+```
+-->
 
+```agda
 ≤-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
 ≤-trans 0≤x     0≤x     = 0≤x
 ≤-trans 0≤x     (s≤s q) = 0≤x
@@ -60,22 +75,73 @@ equivalence between $x \le y$ and $(1 + x) \le (1 + y)$.
 
 <!--
 ```agda
+private
+  from-prim-< : ∀ x y → ⌞ x Prim.< y ⌟ → x < y
+  from-prim-< zero (suc y) o = s≤s 0≤x
+  from-prim-< (suc x) (suc y) o = s≤s (from-prim-< x y o)
+
+  to-prim-< : ∀ x y → x < y → ⌞ x Prim.< y ⌟
+  to-prim-< zero (suc y) o = oh
+  to-prim-< (suc x) (suc y) o = to-prim-< x y (≤-peel o)
+
 instance
   H-Level-≤ : ∀ {n x y} → H-Level (x ≤ y) (suc n)
   H-Level-≤ = prop-instance ≤-is-prop
 ```
 -->
 
+### Properties of the strict order
+
+```agda
+<-≤-asym : ∀ {x y} → x < y → ¬ (y ≤ x)
+<-≤-asym {.(suc _)} {.(suc _)} (s≤s p) (s≤s q) = <-≤-asym p q
+
+<-asym : ∀ {x y} → x < y → ¬ (y < x)
+<-asym {.(suc _)} {.(suc _)} (s≤s p) (s≤s q) = <-asym p q
+
+<-not-equal : ∀ {x y} → x < y → x ≠ y
+<-not-equal {zero} (s≤s p) q = absurd (zero≠suc q)
+<-not-equal {suc x} (s≤s p) q = <-not-equal p (suc-inj q)
+
+<-irrefl : ∀ {x y} → x ≡ y → ¬ (x < y)
+<-irrefl {suc x} {zero}  p      q  = absurd (suc≠zero p)
+<-irrefl {zero}  {suc y} p      _  = absurd (zero≠suc p)
+<-irrefl {suc x} {suc y} p (s≤s q) = <-irrefl (suc-inj p) q
+
+<-weaken : ∀ {x y} → x < y → x ≤ y
+<-weaken {x} {suc y} p = ≤-sucr (≤-peel p)
+
+≤-strengthen : ∀ {x y} → x ≤ y → (x ≡ y) ⊎ (x < y)
+≤-strengthen {zero} {zero} 0≤x = inl refl
+≤-strengthen {zero} {suc y} 0≤x = inr (s≤s 0≤x)
+≤-strengthen {suc x} {suc y} (s≤s p) with ≤-strengthen p
+... | inl eq = inl (ap suc eq)
+... | inr le = inr (s≤s le)
+
+<-from-≤ : ∀ {x y} → x ≠ y → x ≤ y → x < y
+<-from-≤ x≠y x≤y with ≤-strengthen x≤y
+... | inl x=y = absurd (x≠y x=y)
+... | inr x<y = x<y
+```
+
+### Linearity
+
 Furthermore, `_≤_`{.Agda} is decidable, and weakly total:
 
+<!--
 ```agda
-≤-dec : (x y : Nat) → Dec (x ≤ y)
-≤-dec zero zero = yes 0≤x
-≤-dec zero (suc y) = yes 0≤x
-≤-dec (suc x) zero = no λ { () }
-≤-dec (suc x) (suc y) with ≤-dec x y
-... | yes x≤y = yes (s≤s x≤y)
-... | no ¬x≤y = no (λ { (s≤s x≤y) → ¬x≤y x≤y })
+module _ where private
+```
+-->
+
+```agda
+  ≤-dec : (x y : Nat) → Dec (x ≤ y)
+  ≤-dec zero zero = yes 0≤x
+  ≤-dec zero (suc y) = yes 0≤x
+  ≤-dec (suc x) zero = no λ { () }
+  ≤-dec (suc x) (suc y) with ≤-dec x y
+  ... | yes x≤y = yes (s≤s x≤y)
+  ... | no ¬x≤y = no (λ { (s≤s x≤y) → ¬x≤y x≤y })
 
 ≤-is-weakly-total : ∀ x y → ¬ (x ≤ y) → y ≤ x
 ≤-is-weakly-total zero    zero    _    = 0≤x
@@ -87,6 +153,33 @@ Furthermore, `_≤_`{.Agda} is decidable, and weakly total:
 
 <!--
 ```agda
+<-from-not-≤ : ∀ x y → ¬ (x ≤ y) → y < x
+<-from-not-≤ zero    zero    x    = absurd (x 0≤x)
+<-from-not-≤ zero    (suc y) ¬0≤s = absurd (¬0≤s 0≤x)
+<-from-not-≤ (suc x) zero    _    = s≤s 0≤x
+<-from-not-≤ (suc x) (suc y) ¬s≤s = s≤s $
+  <-from-not-≤ x y λ z → ¬s≤s (s≤s z)
+
+≤-uncap : ∀ m n → m ≠ suc n → m ≤ suc n → m ≤ n
+≤-uncap m n p 0≤x = 0≤x
+≤-uncap (suc x) zero p (s≤s 0≤x) = absurd (p refl)
+≤-uncap (suc x) (suc n) p (s≤s q) = s≤s (≤-uncap x n (p ∘ ap suc) q)
+```
+-->
+
+<!--
+```agda
+≤-dec : (x y : Nat) → Dec (x ≤ y)
+≤-dec x y with x ≡? y
+... | yes x=y = yes (≤-refl' x=y)
+... | no ¬x=y with oh? (x Prim.< y)
+... | yes x<y = yes (<-weaken (from-prim-< x y x<y))
+... | no ¬x<y  = no not-both where
+  not-both : ¬ (x ≤ y)
+  not-both p with ≤-strengthen p
+  ... | inl x=y = ¬x=y x=y
+  ... | inr x<y = ¬x<y (to-prim-< x y x<y)
+
 instance
   Dec-≤ : ∀ {x y} → Dec (x ≤ y)
   Dec-≤ = ≤-dec _ _
@@ -120,28 +213,6 @@ their strict ordering:
   go (suc x) (suc y) p q    = ap suc (go x y (λ { a → p (s≤s a) }) λ { a → q (s≤s a) })
 ```
 
-### Properties of the strict order
-
-```agda
-<-≤-asym : ∀ {x y} → x < y → ¬ (y ≤ x)
-<-≤-asym {.(suc _)} {.(suc _)} (s≤s p) (s≤s q) = <-≤-asym p q
-
-<-asym : ∀ {x y} → x < y → ¬ (y < x)
-<-asym {.(suc _)} {.(suc _)} (s≤s p) (s≤s q) = <-asym p q
-
-<-not-equal : ∀ {x y} → x < y → ¬ x ≡ y
-<-not-equal {zero} (s≤s p) q = absurd (zero≠suc q)
-<-not-equal {suc x} (s≤s p) q = <-not-equal p (suc-inj q)
-
-<-irrefl : ∀ {x y} → x ≡ y → ¬ (x < y)
-<-irrefl {suc x} {zero}  p      q  = absurd (suc≠zero p)
-<-irrefl {zero}  {suc y} p      _  = absurd (zero≠suc p)
-<-irrefl {suc x} {suc y} p (s≤s q) = <-irrefl (suc-inj p) q
-
-weaken-< : ∀ {x y} → x < y → x ≤ y
-weaken-< {x} {suc y} p = ≤-sucr (≤-peel p)
-```
-
 ## Nat is a lattice
 
 An interesting tidbit about the ordering on $\NN$ is that it is, in some
diff --git a/src/Data/Nat/Prime.lagda.md b/src/Data/Nat/Prime.lagda.md
new file mode 100644
index 000000000..68f1d668a
--- /dev/null
+++ b/src/Data/Nat/Prime.lagda.md
@@ -0,0 +1,291 @@
+<!--
+```agda
+open import 1Lab.Prelude
+
+open import Data.Wellfounded.Properties
+open import Data.Nat.Divisible.GCD
+open import Data.List.Quantifiers
+open import Data.Wellfounded.Base
+open import Data.List.Membership
+open import Data.Fin.Properties
+open import Data.Nat.Properties
+open import Data.Nat.Divisible
+open import Data.Nat.DivMod
+open import Data.List.Base
+open import Data.Nat.Order
+open import Data.Fin.Base renaming (_≤_ to _≤ᶠ_) hiding (_<_)
+open import Data.Nat.Base
+open import Data.Dec
+open import Data.Sum
+```
+-->
+
+```agda
+module Data.Nat.Prime where
+```
+
+# Prime and composite numbers
+
+A number $n$ is **prime** when it is greater than two (which we split
+into being positive and being apart from 1), and, if $d$ is any other
+number that divides $n$, then either $d = 1$ or $d = n$. Since we've
+assumed $n \neq 1$, these cases are disjoint, so being a prime is a
+[[proposition]].
+
+```agda
+record is-prime (n : Nat) : Type where
+  field
+    ⦃ positive ⦄ : Positive n
+    prime≠1   : n ≠ 1
+    primality : ∀ d → d ∣ n → (d ≡ 1) ⊎ (d ≡ n)
+```
+
+We note that a prime number has no *proper divisors*, in that, if $d
+\neq 1$ and $d \neq n$, then $d$ does not divide $n$.
+
+```agda
+  ¬proper-divisor : ∀ {d} → d ≠ 1 → d ≠ n → ¬ d ∣ n
+  ¬proper-divisor ¬d=1 ¬d=n d∣n with primality _ d∣n
+  ... | inl d=1 = ¬d=1 d=1
+  ... | inr d=n = ¬d=n d=n
+```
+
+<!--
+```agda
+  prime>1 : 1 < n
+  prime>1 = <-from-≤ (prime≠1 ∘ sym) positive
+
+private unquoteDecl eqv = declare-record-iso eqv (quote is-prime)
+open is-prime
+
+abstract instance
+  H-Level-is-prime : ∀ {n k} → H-Level (is-prime n) (suc k)
+  H-Level-is-prime = prop-instance $ Iso→is-hlevel 1 eqv $ Σ-is-hlevel 1 (hlevel 1) λ p →
+    Σ-is-hlevel 1 (hlevel 1) λ q → Π-is-hlevel² 1 λ d dn →
+      disjoint-⊎-is-prop (hlevel 1) (hlevel 1) (λ (a , b) → q (sym b ∙ a))
+```
+-->
+
+Conversely, if $n > 2$ is a number that is not prime, it is called
+**composite**. Instead of defining `is-composite`{.Agda} to be the
+literal negation of `is-prime`{.Agda}, we instead define this notion
+positively: To say that a number is composite is to give a prime $p$ and
+a number $q \ge 2$ such that $qp = n$ and $p$ is the smallest divisor of
+$n$.
+
+```agda
+record is-composite (n : Nat) : Type where
+  field
+    {p q} : Nat
+
+    p-prime  : is-prime p
+    q-proper : 1 < q
+
+    factors : q * p ≡ n
+    least : ∀ p' → 1 < p' → p' ∣ n → p ≤ p'
+```
+
+Note that the assumption that $p$ is a prime is simply for convenience:
+the least proper divisor of *any* number is always a prime.
+
+```agda
+least-divisor→is-prime
+  : ∀ p n → 1 < p → p ∣ n → (∀ p' → 1 < p' → p' ∣ n → p ≤ p') → is-prime p
+least-divisor→is-prime p n gt div least .positive = ≤-trans ≤-ascend gt
+least-divisor→is-prime p n gt div least .prime≠1 q = <-irrefl (sym q) gt
+least-divisor→is-prime p@(suc p') n gt div least .primality 0 x = absurd (suc≠zero x)
+least-divisor→is-prime p@(suc p') n gt div least .primality 1 x = inl refl
+least-divisor→is-prime p@(suc p') n gt div least .primality m@(suc (suc k)) x =
+  inr (≤-antisym (m∣sn→m≤sn x) (least m (s≤s (s≤s 0≤x)) (∣-trans x div)))
+```
+
+<!--
+```agda
+open is-composite hiding (p ; q ; factors)
+
+private unquoteDecl eqv' = declare-record-iso eqv' (quote is-composite)
+
+abstract instance
+  H-Level-is-composite : ∀ {n k} → H-Level (is-composite n) (suc k)
+  H-Level-is-composite = prop-instance λ a@record{p = p ; q = q} b@record{p = p' ; q = q'} →
+    let
+      open is-composite using (factors)
+
+      ap=bp : p ≡ p'
+      ap=bp = ≤-antisym
+        (a .least p' (prime>1 (b .p-prime)) (fibre→∣ (q' , b .factors)))
+        (b .least p (prime>1 (a .p-prime)) (fibre→∣ (q , a .factors)))
+
+      aq=bq : q ≡ q'
+      aq=bq = *-injl p q q' (*-commutative p q ∙ a .factors ∙ sym (b .factors) ∙ ap (q' *_) (sym ap=bp) ∙ *-commutative q' p)
+    in Equiv.injective (Iso→Equiv eqv') (Σ-pathp ap=bp (Σ-prop-pathp! aq=bq))
+
+prime-divisor-lt : ∀ p q n .⦃ _ : Positive n ⦄ → is-prime p → q * p ≡ n → q < n
+prime-divisor-lt p q n pprime div with ≤-strengthen (m∣n→m≤n {q} {n} (fibre→∣ (p , *-commutative p q ∙ div)))
+... | inr less = less
+... | inl same = absurd (pprime .prime≠1 $
+  *-injr n p 1 (sym (+-zeror n ∙ sym div ∙ *-commutative q p ∙ ap (p *_) same)))
+
+prime-remainder-positive : ∀ p q n .⦃ _ : Positive n ⦄ → ¬ is-prime n → is-prime p → q * p ≡ n → 1 < q
+prime-remainder-positive p 0 n@(suc _) _ _ div = absurd (zero≠suc div)
+prime-remainder-positive p 1 n@(suc _) nn pp div = absurd (nn (subst is-prime (sym (+-zeror p) ∙ div) pp))
+prime-remainder-positive p (suc (suc _)) (suc _) _ _ _ = s≤s (s≤s 0≤x)
+
+distinct-primes→coprime : ∀ {a b} → is-prime a → is-prime b → ¬ a ≡ b → is-gcd a b 1
+distinct-primes→coprime {a@(suc a')} {b@(suc b')} apr bpr a≠b = record
+  { gcd-∣l = a , *-oner a
+  ; gcd-∣r = b , *-oner b
+  ; greatest = λ {g'} w2 w → case bpr .primality _ w of λ where
+    (inl p) → subst (_∣ 1) (sym p) ∣-refl
+    (inr q) → case apr .primality _ w2 of λ where
+      (inl p) → subst (_∣ 1) (sym p) ∣-refl
+      (inr r) → absurd (a≠b (sym r ∙ q))
+  }
+```
+-->
+
+## Primality testing
+
+```agda
+is-prime-or-composite : ∀ n → 1 < n → is-prime n ⊎ is-composite n
+is-prime-or-composite n@(suc (suc m)) (s≤s p)
+  with Fin-omniscience {n = n} (λ k → 1 < to-nat k × to-nat k ∣ n)
+... | inr prime = inl record { prime≠1 = suc≠zero ∘ suc-inj ; primality = no-divisors→prime } where
+  no-divisors→prime : ∀ d → d ∣ n → d ≡ 1 ⊎ d ≡ n
+  no-divisors→prime d div with d ≡? 1
+  ... | yes p = inl p
+  ... | no ¬d=1 with d ≡? n
+  ... | yes p = inr p
+  ... | no ¬d=n =
+    let
+      ord : d < n
+      ord = proper-divisor-< ¬d=n div
+
+      coh : d ≡ to-nat (from-ℕ< (d , ord))
+      coh = sym (ap fst (to-from-ℕ< (d , ord)))
+
+      no = case d return (λ x → ¬ x ≡ 1 → x ∣ n → 1 < x) of λ where
+        0 p1 div → absurd (<-irrefl (sym div) (s≤s 0≤x))
+        1 p1 div → absurd (p1 refl)
+        (suc (suc n)) p1 div → s≤s (s≤s 0≤x)
+    in absurd (prime (from-ℕ< (d , ord)) ((subst (1 <_) coh (no ¬d=1 div)) , subst (_∣ n) coh div))
+... | inl (ix , (proper , div) , least)
+  = inr record { p-prime = prime ; q-proper = proper' ; factors = path ; least = least' } where
+  open Σ (∣→fibre div) renaming (fst to quot ; snd to path)
+
+  abstract
+    least' : (p' : Nat) → 1 < p' → p' ∣ n → to-nat ix ≤ p'
+    least' p' x div with ≤-strengthen (m∣n→m≤n div)
+    ... | inl same = ≤-trans ≤-ascend (subst (to-nat ix <_) (sym same) (to-ℕ< ix .snd))
+    ... | inr less =
+      let
+        it : ℕ< n
+        it = p' , less
+
+        coh : p' ≡ to-nat (from-ℕ< it)
+        coh = sym (ap fst (to-from-ℕ< it))
+
+        orig = least (from-ℕ< it) (subst (1 <_) coh x , subst (_∣ n) coh div)
+      in ≤-trans orig (subst (to-nat (from-ℕ< it) ≤_) (sym coh) ≤-refl)
+
+  prime : is-prime (to-nat ix)
+  prime = least-divisor→is-prime (to-nat ix) n proper div least'
+
+  proper' : 1 < quot
+  proper' with quot | path
+  ... | 0 | q = absurd (<-irrefl q (s≤s 0≤x))
+  ... | 1 | q = absurd (<-irrefl (sym (+-zeror (to-nat ix)) ∙ q) (to-ℕ< ix .snd))
+  ... | suc (suc n) | p = s≤s (s≤s 0≤x)
+
+record Factorisation (n : Nat) : Type where
+  constructor factored
+  field
+    primes    : List Nat
+    factors   : product primes ≡ n
+    is-primes : All is-prime primes
+
+  prime-divides : ∀ {x} → x ∈ₗ primes → x ∣ n
+  prime-divides {x} h = subst (x ∣_) factors (work _ _ h) where
+    work : ∀ x xs → x ∈ₗ xs → x ∣ product xs
+    work x (y ∷ xs) (here p) = subst (λ e → x ∣ e * product xs) p (∣-*l {x} {product xs})
+    work x (y ∷ xs) (there p) =
+      let
+        it = work x xs p
+        (div , p) = ∣→fibre it
+      in fibre→∣ (y * div , *-associative y div x ∙ ap (y *_) p)
+
+  find-prime-factor : ∀ {x} → is-prime x → x ∣ n → x ∈ₗ primes
+  find-prime-factor {num} x d =
+    work _ primes x (λ _ → all-∈ is-primes) (subst (num ∣_) (sym factors) d)
+    where
+    work : ∀ x xs → is-prime x → (∀ x → x ∈ₗ xs → is-prime x) → x ∣ product xs → x ∈ₗ xs
+    work x [] xp ps xd = absurd (prime≠1 xp (∣-1 xd))
+    work x (y ∷ xs) xp ps xd with x ≡? y
+    ... | yes x=y = here x=y
+    ... | no ¬p = there $ work x xs xp (λ x w → ps x (there w))
+      (|-*-coprime-cancel x y (product xs)
+        ⦃ auto ⦄ ⦃ ps y (here refl) .positive ⦄
+        xd (distinct-primes→coprime xp (ps y (here refl)) ¬p))
+
+open is-composite using (factors)
+open Factorisation
+
+factorisation-unique' : ∀ {n} (a b : Factorisation n) → ∀ p → p ∈ₗ a .primes → p ∈ₗ b .primes
+factorisation-unique' a b p p∈a =
+  let
+    p∣n = prime-divides a p∈a
+  in find-prime-factor b (all-∈ (a .is-primes) p∈a) p∣n
+
+factorisation-worker
+  : ∀ n → (∀ k → k < n → .⦃ _ : Positive k ⦄ → Factorisation k)
+  → .⦃ _ : Positive n ⦄ → Factorisation n
+factorisation-worker 1 ind = factored [] refl []
+factorisation-worker n@(suc (suc m)) ind with is-prime-or-composite n (s≤s (s≤s 0≤x))
+... | inl prime     = factored (n ∷ []) (ap (2 +_) (*-oner m)) (prime ∷ [])
+... | inr composite@record{p = p; q = q} =
+  let
+    instance
+      _ : Positive q
+      _ = ≤-trans ≤-ascend (composite .q-proper)
+
+    factored ps path primes = ind q $
+      prime-divisor-lt p q n (composite .p-prime) (composite .factors)
+  in record
+    { primes    = p ∷ ps
+    ; factors   = ap (p *_) path ·· *-commutative p q ·· composite .factors
+    ; is-primes = composite .p-prime ∷ primes
+    }
+
+factorial : Nat → Nat
+factorial zero = 1
+factorial (suc n) = suc n * factorial n
+
+factorial-positive : ∀ n → Positive (factorial n)
+factorial-positive zero = s≤s 0≤x
+factorial-positive (suc n) = *-preserves-≤ 1 (suc n) 1 (factorial n) (s≤s 0≤x) (factorial-positive n)
+
+≤-factorial : ∀ n → n ≤ factorial n
+≤-factorial zero = 0≤x
+≤-factorial (suc n) = subst (_≤ factorial (suc n)) (*-oner (suc n)) (*-preserves-≤ (suc n) (suc n) 1 (factorial n) ≤-refl (factorial-positive n))
+
+∣-factorial : ∀ n {m} → m < n → suc m ∣ factorial n
+∣-factorial (suc n) {m} m≤n with suc m ≡? suc n
+... | yes m=n = subst (_∣ factorial (suc n)) (sym m=n) (∣-*l {suc n} {factorial n})
+... | no m≠n  = |-*l-pres {suc m} {suc n} {factorial n} $
+  ∣-factorial n {m} (≤-uncap (suc m) n m≠n m≤n)
+
+factorise : (n : Nat) .⦃ _ : Positive n ⦄ → Factorisation n
+factorise = Wf-induction _<_ <-wf _ factorisation-worker
+
+new-prime : (n : Nat) → Σ[ p ∈ Nat ] n < p × is-prime p
+new-prime n with is-prime-or-composite (suc (factorial n)) (s≤s (factorial-positive n))
+new-prime n | inl prime     = suc (factorial n) , s≤s (≤-factorial n) , prime
+new-prime n | inr c@record{p = p} with holds? (suc n ≤ p)
+new-prime n | inr c@record{p = p} | yes n<p = p , n<p , c .p-prime
+new-prime n | inr c@record{p = suc p; q = q} | no ¬n<p =
+  let
+    rem = ∣-factorial n (<-from-not-≤ _ _ (¬n<p ∘ s≤s))
+    rem' : suc p ≡ 1
+    rem' = ∣-1 (∣-+-cancel' {n = suc p} {a = 1} {b = factorial n} rem (fibre→∣ (q , c .factors)))
+  in absurd (c .p-prime .prime≠1 rem')
+```
diff --git a/src/Data/Nat/Properties.lagda.md b/src/Data/Nat/Properties.lagda.md
index 8d80f01b6..71a2563d0 100644
--- a/src/Data/Nat/Properties.lagda.md
+++ b/src/Data/Nat/Properties.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-open import 1Lab.Rewrite
 open import 1Lab.Path
 open import 1Lab.Type
 
@@ -119,6 +118,22 @@ numbers]. Since they're mostly simple inductive arguments written in
 
 *-suc-inj' : ∀ k x y → suc k * x ≡ suc k * y → x ≡ y
 *-suc-inj' k x y p = *-suc-inj k x y (*-commutative x (suc k) ·· p ·· *-commutative (suc k) y)
+
+*-injr : ∀ k x y .⦃ _ : Positive k ⦄ → x * k ≡ y * k → x ≡ y
+*-injr (suc k) x y p = *-suc-inj k x y p
+
+*-injl : ∀ k x y .⦃ _ : Positive k ⦄ → k * x ≡ k * y → x ≡ y
+*-injl (suc k) x y p = *-suc-inj' k x y p
+
+*-is-onel : ∀ x n → x * n ≡ 1 → x ≡ 1
+*-is-onel zero n p = p
+*-is-onel (suc zero) zero p = refl
+*-is-onel (suc (suc x)) zero p = absurd (zero≠suc (sym (*-zeror x) ∙ p))
+*-is-onel (suc x) (suc zero) p = ap suc (sym (*-oner x)) ∙ p
+*-is-onel (suc x) (suc (suc n)) p = absurd (zero≠suc (sym (suc-inj p)))
+
+*-is-oner : ∀ x n → x * n ≡ 1 → n ≡ 1
+*-is-oner x n p = *-is-onel n x (*-commutative n x ∙ p)
 ```
 
 ## Exponentiation
@@ -228,6 +243,10 @@ difference→≤ {x} {z} zero p            = subst (x ≤_) (sym (+-zeror x) ∙
 difference→≤ {zero}  {z}     (suc y) p = 0≤x
 difference→≤ {suc x} {zero}  (suc y) p = absurd (suc≠zero p)
 difference→≤ {suc x} {suc z} (suc y) p = s≤s (difference→≤ (suc y) (suc-inj p))
+
+nonzero→positive : ∀ {x} → x ≠ 0 → 0 < x
+nonzero→positive {zero} p = absurd (p refl)
+nonzero→positive {suc x} p = s≤s 0≤x
 ```
 
 ### Monus
diff --git a/src/Data/Sum/Properties.lagda.md b/src/Data/Sum/Properties.lagda.md
index 6ab7ea4df..bab379dec 100644
--- a/src/Data/Sum/Properties.lagda.md
+++ b/src/Data/Sum/Properties.lagda.md
@@ -176,7 +176,7 @@ the coproduct of _disjoint_ propositions is a proposition:
 
 ```agda
 disjoint-⊎-is-prop
-  : is-prop A → is-prop B → ¬ A × B
+  : is-prop A → is-prop B → ¬ (A × B)
   → is-prop (A ⊎ B)
 disjoint-⊎-is-prop Ap Bp notab (inl x) (inl y) = ap inl (Ap x y)
 disjoint-⊎-is-prop Ap Bp notab (inl x) (inr y) = absurd (notab (x , y))
diff --git a/src/Homotopy/Space/Delooping.lagda.md b/src/Homotopy/Space/Delooping.lagda.md
index aefac7f8c..6a7314322 100644
--- a/src/Homotopy/Space/Delooping.lagda.md
+++ b/src/Homotopy/Space/Delooping.lagda.md
@@ -2,7 +2,6 @@
 ```agda
 open import 1Lab.Reflection.Induction
 open import 1Lab.Prelude
-open import 1Lab.Rewrite
 
 open import Algebra.Group.Cat.Base
 open import Algebra.Group.Homotopy
@@ -477,8 +476,8 @@ We can then obtain a nice interface for working with `winding`{.Agda}.
   opaque
     unfolding winding-is-equiv
 
-    winding-is-equiv-base : winding-is-equiv base ≡rw Equiv.inverse (G≃ΩB G) .snd
-    winding-is-equiv-base = make-rewrite prop!
+    winding-is-equiv-base : winding-is-equiv base ≡ Equiv.inverse (G≃ΩB G) .snd
+    winding-is-equiv-base = prop!
 
   {-# REWRITE winding-is-equiv-base #-}
 
diff --git a/src/Logic/Propositional/Classical/SAT.lagda.md b/src/Logic/Propositional/Classical/SAT.lagda.md
index 6d0dcb74d..d80c73569 100644
--- a/src/Logic/Propositional/Classical/SAT.lagda.md
+++ b/src/Logic/Propositional/Classical/SAT.lagda.md
@@ -259,8 +259,8 @@ unit-propagate-sat x ϕs (ρ , ρ-sat) =
 unit-propagate-unsat
   : (x : Literal (suc Γ))
   → (ϕs : CNF (suc Γ))
-  → ¬ Σ[ ρ ∈ (Fin Γ → Bool) ]       (⟦ unit-propagate x ϕs ⟧ ρ ≡ true)
-  → ¬ Σ[ ρ ∈ (Fin (suc Γ) → Bool) ] ((⟦ ϕs ⟧ ρ ≡ true) × (⟦ x ⟧ ρ ≡ true))
+  → ¬ (Σ[ ρ ∈ (Fin Γ → Bool) ]       ⟦ unit-propagate x ϕs ⟧ ρ ≡ true)
+  → ¬ (Σ[ ρ ∈ (Fin (suc Γ) → Bool) ] ⟦ ϕs ⟧ ρ ≡ true × ⟦ x ⟧ ρ ≡ true)
 unit-propagate-unsat x ϕs ¬sat (ρ , ρ-sat , x-sat) = ¬sat $
     delete ρ (lit-var x)
   , sym (unit-propagate-complete x ϕs ρ x-sat) ∙ ρ-sat
@@ -274,7 +274,7 @@ representation of $\top$, while having an empty clause is the CNF
 representation of $\bot$.
 
 ```agda
-cnf-sat? : (ϕs : CNF Γ) → Dec (Σ[ ρ ∈ (Fin Γ → Bool) ] (⟦ ϕs ⟧ ρ ≡ true))
+cnf-sat? : (ϕs : CNF Γ) → Dec (Σ[ ρ ∈ (Fin Γ → Bool) ] ⟦ ϕs ⟧ ρ ≡ true)
 cnf-sat? {Γ = zero} []       = yes ((λ ()) , refl)
 cnf-sat? {Γ = zero} (ϕ ∷ ϕs) = no λ where
   (ρ , sat) → ¬empty-clause-sat ϕ ρ (and-reflect-true-l sat)
diff --git a/src/Meta/Append.lagda.md b/src/Meta/Append.lagda.md
index db89e2de7..3fbf6ea87 100644
--- a/src/Meta/Append.lagda.md
+++ b/src/Meta/Append.lagda.md
@@ -12,7 +12,7 @@ module Meta.Append where
 
 ```agda
 record Append {ℓ} (A : Type ℓ) : Type ℓ where
-  infixr 6 _<>_
+  infixr 8 _<>_
 
   field
     mempty : A
diff --git a/src/Prim/Data/Nat.lagda.md b/src/Prim/Data/Nat.lagda.md
index fb050e9c4..cbdf4496b 100644
--- a/src/Prim/Data/Nat.lagda.md
+++ b/src/Prim/Data/Nat.lagda.md
@@ -31,8 +31,8 @@ are computed more efficiently when bound as `BUILTIN`s.
 
 ```agda
 infix  4 _==_ _<_
-infixl 6 _+_ _-_
-infixl 7 _*_
+infixl 8 _+_ _-_
+infixl 9 _*_
 
 _+_ : Nat → Nat → Nat
 zero  + m = m
diff --git a/src/Prim/Data/Sigma.lagda.md b/src/Prim/Data/Sigma.lagda.md
index 2b9c3638c..f3ae44856 100644
--- a/src/Prim/Data/Sigma.lagda.md
+++ b/src/Prim/Data/Sigma.lagda.md
@@ -36,7 +36,7 @@ infixr 4 _,_
 Σ-syntax X F = Σ X F
 
 syntax Σ-syntax X (λ x → F) = Σ[ x ∈ X ] F
-infix 5 Σ-syntax
+infix 4 Σ-syntax
 ```
 -->
 
diff --git a/src/Prim/Kan.lagda.md b/src/Prim/Kan.lagda.md
index 8010be0cc..fcb20efa3 100644
--- a/src/Prim/Kan.lagda.md
+++ b/src/Prim/Kan.lagda.md
@@ -50,7 +50,7 @@ postulate
 
 {-# BUILTIN PATHP PathP #-}
 
-infix 4 _≡_
+infix 7 _≡_
 
 _≡_ : ∀ {ℓ} {A : Type ℓ} → A → A → Type ℓ
 _≡_ {A = A} = PathP (λ i → A)
@@ -60,6 +60,8 @@ _≡_ {A = A} = PathP (λ i → A)
 
 <!--
 ```agda
+{-# BUILTIN REWRITE _≡_ #-}
+
 caseⁱ_of_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (x : A) → ((y : A) → x ≡ y → B) → B
 caseⁱ x of f = f x (λ i → x)