From aec08fe658eafa569f9cec1c05a72cc5bdfc6c50 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 21 Nov 2023 08:30:25 -0600
Subject: [PATCH] style: remove all trailing whitespace

---
 src/Mugen/Algebra/Displacement.agda           | 10 ++--
 src/Mugen/Algebra/Displacement/Coimage.agda   |  8 +--
 .../Algebra/Displacement/FiniteSupport.agda   |  4 +-
 .../Algebra/Displacement/InfiniteProduct.agda | 10 ++--
 .../Algebra/Displacement/NearlyConstant.agda  | 56 +++++++++----------
 .../Algebra/Displacement/NonPositive.agda     |  2 +-
 src/Mugen/Algebra/Displacement/Product.agda   |  2 +-
 src/Mugen/Algebra/OrderedMonoid.agda          |  4 +-
 src/Mugen/Cat/HierarchyTheory/Properties.agda |  2 +-
 src/Mugen/Data/Coimage.agda                   |  4 +-
 src/Mugen/Data/Int.agda                       |  6 +-
 src/Mugen/Data/List.agda                      |  6 +-
 src/Mugen/Order/Coproduct.agda                |  2 +-
 .../Order/LeftInvariantRightCentered.agda     |  6 +-
 src/Mugen/Order/README.md                     |  2 +-
 src/Mugen/Prelude.agda                        |  8 +--
 16 files changed, 66 insertions(+), 66 deletions(-)

diff --git a/src/Mugen/Algebra/Displacement.agda b/src/Mugen/Algebra/Displacement.agda
index 9be6398..ba017d2 100644
--- a/src/Mugen/Algebra/Displacement.agda
+++ b/src/Mugen/Algebra/Displacement.agda
@@ -95,7 +95,7 @@ module _
     Iso→is-hlevel 1 eqv $
     Σ-is-hlevel 1 (Y.has-is-set _ _) λ _ →
     Π-is-hlevel² 1 λ _ _ → Y.has-is-set _ _
-    where unquoteDecl eqv = declare-record-iso eqv (quote is-displacement-algebra-hom) 
+    where unquoteDecl eqv = declare-record-iso eqv (quote is-displacement-algebra-hom)
 
   record Displacement-algebra-hom : Type (o ⊔ o' ⊔ r ⊔ r') where
     no-eta-equality
@@ -152,7 +152,7 @@ displacement-hom-∘ f g .strict-hom =
   strictly-monotone-∘ (f .strict-hom) (g .strict-hom)
 displacement-hom-∘ f g .has-is-displacement-hom .is-displacement-algebra-hom.pres-ε =
   ap (λ x → f # x) (g .pres-ε)
-  ∙ f .pres-ε 
+  ∙ f .pres-ε
 displacement-hom-∘ f g .has-is-displacement-hom .is-displacement-algebra-hom.pres-⊗ x y =
   ap (λ x → f # x) (g .pres-⊗ x y)
   ∙ f .pres-⊗ (g # x) (g # y)
@@ -302,7 +302,7 @@ module _
       identity  : ∀ (a : ⌞ A ⌟) → α a B.ε ≡ a
       compat    : ∀ (a : ⌞ A ⌟) (x y : ⌞ B ⌟) → α (α a x) y ≡ α a (x B.⊗ y)
       invariant : ∀ (a : ⌞ A ⌟) (x y : ⌞ B ⌟) → x B.< y → α a x A.< α a y
-  
+
   is-right-displacement-action-is-prop
     : (α : ⌞ A ⌟ → ⌞ B ⌟ → ⌞ A ⌟)
     → is-prop (is-right-displacement-action α)
@@ -311,7 +311,7 @@ module _
     Σ-is-hlevel 1 (Π-is-hlevel 1 λ _ → A.has-is-set _ _) λ _ →
     Σ-is-hlevel 1 (Π-is-hlevel³ 1 λ _ _ _ → A.has-is-set _ _) λ _ →
     Π-is-hlevel³ 1 λ _ _ _ → Π-is-hlevel 1 λ _ → A.<-thin
-    where unquoteDecl eqv = declare-record-iso eqv (quote is-right-displacement-action) 
+    where unquoteDecl eqv = declare-record-iso eqv (quote is-right-displacement-action)
 
 record Right-displacement-action
   {o r o′ r′}
@@ -326,7 +326,7 @@ record Right-displacement-action
 
 module _ where
   open Right-displacement-action
-  
+
   Right-displacement-action-path
     : ∀ {o r o′ r′}
     → {A : Strict-order o r} {B : Displacement-algebra o′ r′}
diff --git a/src/Mugen/Algebra/Displacement/Coimage.agda b/src/Mugen/Algebra/Displacement/Coimage.agda
index 59f1228..afa42ee 100644
--- a/src/Mugen/Algebra/Displacement/Coimage.agda
+++ b/src/Mugen/Algebra/Displacement/Coimage.agda
@@ -54,10 +54,10 @@ module Coim-of-displacement-hom
   -- Algebra
 
   _⊗coim_ : X/f → X/f → X/f
-  _⊗coim_ = Coim-map₂ (λ x y → x X.⊗ y) λ w x y z p q → 
-    (pres-⊗ w y ∙ ap₂ Y._⊗_ p q ∙ sym (pres-⊗ x z)) 
+  _⊗coim_ = Coim-map₂ (λ x y → x X.⊗ y) λ w x y z p q →
+    (pres-⊗ w y ∙ ap₂ Y._⊗_ p q ∙ sym (pres-⊗ x z))
 
-  εcoim : X/f 
+  εcoim : X/f
   εcoim = inc X.ε
 
   ⊗coim-idl : ∀ x → εcoim ⊗coim x ≡ x
@@ -167,7 +167,7 @@ module _ {o r} {X Y : Displacement-algebra o r} {f : Displacement-algebra-hom X
           (Y-joins.universal (coim≤→Y≤ x≤z) (coim≤→Y≤ y≤z))
 
       joins : has-joins (Coim-of-displacement-hom f)
-      joins .has-joins.join = coim-join 
+      joins .has-joins.join = coim-join
       joins .has-joins.joinl {x} {y} =
         Coim-elim-prop₂ {C = λ x y → x coim≤ (coim-join x y)}
           (λ x y → X/f.≤-thin) coim-joinl x y
diff --git a/src/Mugen/Algebra/Displacement/FiniteSupport.agda b/src/Mugen/Algebra/Displacement/FiniteSupport.agda
index 2bc9f90..ac44cc6 100644
--- a/src/Mugen/Algebra/Displacement/FiniteSupport.agda
+++ b/src/Mugen/Algebra/Displacement/FiniteSupport.agda
@@ -68,7 +68,7 @@ module FinSupport {o r} (𝒟 : Displacement-algebra o r) (cmp : ∀ x y → Tri
   merge-fin : FinSupportList → FinSupportList → FinSupportList
   merge-fin xs ys .FinSupportList.support = merge (xs .support) (ys .support)
   merge-fin xs ys .FinSupportList.is-ε = ap₂ _⊗_ (xs .is-ε) (ys .is-ε) ∙ 𝒟.idl
-  
+
   empty-fin : FinSupportList
   empty-fin .support = empty
   empty-fin .is-ε = refl
@@ -126,7 +126,7 @@ module _
   where
   open FinSupport 𝒟 cmp
   open FinSupportList
-  
+
   FinSupport⊆NearlyConstant : is-displacement-subalgebra (FiniteSupport 𝒟 cmp) (NearlyConstant 𝒟 cmp)
   FinSupport⊆NearlyConstant = to-displacement-subalgebra mk where
     mk : make-displacement-subalgebra _ _
diff --git a/src/Mugen/Algebra/Displacement/InfiniteProduct.agda b/src/Mugen/Algebra/Displacement/InfiniteProduct.agda
index 8238064..e16d968 100644
--- a/src/Mugen/Algebra/Displacement/InfiniteProduct.agda
+++ b/src/Mugen/Algebra/Displacement/InfiniteProduct.agda
@@ -31,13 +31,13 @@ module Inf {o r} (𝒟 : Displacement-algebra o r) where
   ε∞ _ = ε
 
   ⊗∞-associative : ∀ (f g h : Nat → ⌞ 𝒟 ⌟) → (f ⊗∞ (g ⊗∞ h)) ≡ ((f ⊗∞ g) ⊗∞ h)
-  ⊗∞-associative f g h = funext λ x → 𝒟.associative 
+  ⊗∞-associative f g h = funext λ x → 𝒟.associative
 
   ⊗∞-idl : ∀ (f : Nat → ⌞ 𝒟 ⌟) → (ε∞ ⊗∞ f) ≡ f
-  ⊗∞-idl f = funext λ x → 𝒟.idl 
+  ⊗∞-idl f = funext λ x → 𝒟.idl
 
   ⊗∞-idr : ∀ (f : Nat → ⌞ 𝒟 ⌟) → (f ⊗∞ ε∞) ≡ f
-  ⊗∞-idr f = funext λ x → 𝒟.idr 
+  ⊗∞-idr f = funext λ x → 𝒟.idr
 
   --------------------------------------------------------------------------------
   -- Algebra
@@ -64,7 +64,7 @@ module Inf {o r} (𝒟 : Displacement-algebra o r) where
     field
       ≤-everywhere : ∀ n →  f n 𝒟.≤ g n
       <-somewhere  : ∃[ n ∈ Nat ] (f n 𝒟.< g n)
- 
+
   open _inf<_ public
 
   inf≤-everywhere : ∀ {f g} → non-strict _inf<_ f g → ∀ n → f n 𝒟.≤ g n
@@ -78,7 +78,7 @@ module Inf {o r} (𝒟 : Displacement-algebra o r) where
   inf<-trans f g h f<g g<h .≤-everywhere n = 𝒟.≤-trans (≤-everywhere f<g n) (≤-everywhere g<h n)
   inf<-trans f g h f<g g<h .<-somewhere = ∥-∥-map (λ { (n , fn<gn) → n , 𝒟.≤-transr fn<gn (≤-everywhere g<h n) }) (<-somewhere f<g)
 
-  inf<-is-prop : ∀ f g  → is-prop (f inf< g) 
+  inf<-is-prop : ∀ f g  → is-prop (f inf< g)
   inf<-is-prop f g f<g f<g′ i .≤-everywhere n = 𝒟.≤-thin (≤-everywhere f<g n) (≤-everywhere f<g′ n) i
   inf<-is-prop f g f<g f<g′ i .<-somewhere = squash (<-somewhere f<g) (<-somewhere f<g′) i
 
diff --git a/src/Mugen/Algebra/Displacement/NearlyConstant.agda b/src/Mugen/Algebra/Displacement/NearlyConstant.agda
index 3020ef4..589e437 100644
--- a/src/Mugen/Algebra/Displacement/NearlyConstant.agda
+++ b/src/Mugen/Algebra/Displacement/NearlyConstant.agda
@@ -95,7 +95,7 @@ module NearlyConst
 
   -- Helper type for motives.
   is-compact-case : ∀ {x base : ⌞ 𝒟 ⌟} → Dec (x ≡ base) → Type
-  is-compact-case p = 
+  is-compact-case p =
     Dec-elim _
       (λ _ → ⊥)
       (λ _ → ⊤)
@@ -103,7 +103,7 @@ module NearlyConst
 
   -- Propositional computation helpers for 'is-compact'
   ¬base-is-compact : ∀ xs {x base} → (x ≡ base → ⊥) → is-compact base (xs #r x)
-  ¬base-is-compact xs {x = x} {base = base} ¬base with x ≡? base 
+  ¬base-is-compact xs {x = x} {base = base} ¬base with x ≡? base
   ... | yes base! = ¬base base!
   ... | no _ = tt
 
@@ -184,9 +184,9 @@ module NearlyConst
 
   --------------------------------------------------------------------------------
   -- Vanishing Lists
-  -- 
+  --
   -- We say a list vanishes relative to some base 'b' if it /only/ contains 'b'.
-  -- Furthermore, we say a /backward/ list compacts relative to some base if 
+  -- Furthermore, we say a /backward/ list compacts relative to some base if
   -- it's compaction is equal to [].
   --
   -- These conditions may seems somewhat redundant. Why not define one as
@@ -247,14 +247,14 @@ module NearlyConst
   compacts-head-∷ base x xs compacts =
     vanish-head-∷ base x xs $
     subst (vanishes base) (fwd-bwd (x ∷ xs)) $
-    vanishes-fwd base (bwd (x ∷ xs)) compacts 
+    vanishes-fwd base (bwd (x ∷ xs)) compacts
 
   compacts-tail-∷ : ∀ base x xs → compact base (bwd (x ∷ xs)) ≡ [] → compact base (bwd xs) ≡ []
   compacts-tail-∷ base x xs compacts =
     compacts-bwd base xs $
     vanish-tail-∷ base x xs $
     subst (vanishes base) (fwd-bwd (x ∷ xs)) $
-    vanishes-fwd base (bwd (x ∷ xs)) compacts 
+    vanishes-fwd base (bwd (x ∷ xs)) compacts
 
   compact-vanishr-++r : ∀ {base} xs ys → compact base ys ≡ [] → compact base (xs ++r ys) ≡ compact base xs
   compact-vanishr-++r {base = base} xs [] ys-vanish = refl
@@ -316,7 +316,7 @@ module NearlyConst
 
   --------------------------------------------------------------------------------
   -- Merging Lists
-  -- 
+  --
   -- We start by defining how to merge two lists without performing
   -- compaction.
 
@@ -463,7 +463,7 @@ module NearlyConst
       ∎
   ... | no ¬base =
     refl
- 
+
   --------------------------------------------------------------------------------
   -- Compact Support Lists
   --
@@ -556,7 +556,7 @@ module NearlyConst
     compact (xs .base) (xs .elts)
       ≡⟨ elts-compact xs ⟩
     xs .elts ∎
-  
+
   -- Lifting of 'merge-assoc' to support lists.
   merge-assoc : ∀ xs ys zs → merge xs (merge ys zs) ≡ merge (merge xs ys) zs
   merge-assoc xs ys zs = support-list-path 𝒟.associative $
@@ -704,19 +704,19 @@ module NearlyConst
   ... | lt _ = pf
   ... | eq _ = pf
   ... | gt y<x = lift (𝒟.<-irrefl (𝒟.≡-transl x≡y y<x))
-  merge-list≤-step≤ _ _ _ _ {x = x} {y = y} (inr x<y) pf with cmp x y 
+  merge-list≤-step≤ _ _ _ _ {x = x} {y = y} (inr x<y) pf with cmp x y
   ... | lt _ = pf
   ... | eq _ = pf
   ... | gt y<x = lift (𝒟.<-asym x<y y<x)
 
   merge-list<-step< : ∀ b1 xs b2 ys {x y} → x < y → merge-list≤ b1 xs b2 ys → tri-rec (merge-list≤ b1 xs b2 ys) (merge-list< b1 xs b2 ys) (Lift _ ⊥) (cmp x y)
-  merge-list<-step< _ _ _ _ {x = x} {y = y} x<y pf with cmp x y 
+  merge-list<-step< _ _ _ _ {x = x} {y = y} x<y pf with cmp x y
   ... | lt _ = pf
   ... | eq x≡y = absurd (𝒟.<-irrefl (𝒟.≡-transl (sym x≡y) x<y))
   ... | gt y<x = lift (𝒟.<-asym x<y y<x)
 
   merge-list<-step≡ : ∀ b1 xs b2 ys {x y} → x ≡ y → merge-list< b1 xs b2 ys → tri-rec (merge-list≤ b1 xs b2 ys) (merge-list< b1 xs b2 ys) (Lift _ ⊥) (cmp x y)
-  merge-list<-step≡ _ _ _ _ {x = x} {y = y} x≡y pf with cmp x y 
+  merge-list<-step≡ _ _ _ _ {x = x} {y = y} x≡y pf with cmp x y
   ... | lt x<y = absurd (𝒟.<-irrefl (𝒟.≡-transl (sym x≡y) x<y))
   ... | eq _ = pf
   ... | gt y<x = lift (𝒟.<-irrefl (𝒟.≡-transl x≡y y<x))
@@ -847,20 +847,20 @@ module NearlyConst
       ... | lt x<b2 = merge-list<-step< b1 xs b3 [] (𝒟.<-trans x<b2 b2<b3) (go≤ xs [] [] xs<ys (inr b2<b3))
       ... | eq x≡b2 = merge-list<-step< b1 xs b3 [] (𝒟.≡-transl x≡b2 b2<b3) (go≤ xs [] [] (weaken-< b1 xs b2 [] xs<ys) (inr b2<b3))
       go (x ∷ xs) [] (z ∷ zs) xs<ys ys<zs with cmp x b2 | cmp b2 z
-      ... | lt x<b2 | lt b2<z = merge-list<-step< b1 xs b3 zs (𝒟.<-trans x<b2 b2<z) (go≤ xs [] zs xs<ys ys<zs) 
-      ... | lt x<b2 | eq b2≡z = merge-list<-step< b1 xs b3 zs (𝒟.≡-transr x<b2 b2≡z) (go≤ xs [] zs xs<ys (weaken-< b2 [] b3 zs ys<zs))  
-      ... | eq x≡b2 | lt b2<z = merge-list<-step< b1 xs b3 zs (𝒟.≡-transl x≡b2 b2<z) (go≤ xs [] zs (weaken-< b1 xs b2 [] xs<ys) ys<zs)  
-      ... | eq x≡b2 | eq b2≡z = merge-list<-step≡ b1 xs b3 zs (x≡b2 ∙ b2≡z) (go xs [] zs xs<ys ys<zs)  
+      ... | lt x<b2 | lt b2<z = merge-list<-step< b1 xs b3 zs (𝒟.<-trans x<b2 b2<z) (go≤ xs [] zs xs<ys ys<zs)
+      ... | lt x<b2 | eq b2≡z = merge-list<-step< b1 xs b3 zs (𝒟.≡-transr x<b2 b2≡z) (go≤ xs [] zs xs<ys (weaken-< b2 [] b3 zs ys<zs))
+      ... | eq x≡b2 | lt b2<z = merge-list<-step< b1 xs b3 zs (𝒟.≡-transl x≡b2 b2<z) (go≤ xs [] zs (weaken-< b1 xs b2 [] xs<ys) ys<zs)
+      ... | eq x≡b2 | eq b2≡z = merge-list<-step≡ b1 xs b3 zs (x≡b2 ∙ b2≡z) (go xs [] zs xs<ys ys<zs)
       go (x ∷ xs) (y ∷ ys) [] xs<ys ys<zs with cmp x y | cmp y b3
-      ... | lt x<y | lt y<b3 = merge-list<-step< b1 xs b3 [] (𝒟.<-trans x<y y<b3) (go≤ xs ys [] xs<ys ys<zs) 
-      ... | lt x<y | eq y≡b3 = merge-list<-step< b1 xs b3 [] (𝒟.≡-transr x<y y≡b3) (go≤ xs ys [] xs<ys (weaken-< b2 ys b3 [] ys<zs)) 
-      ... | eq x≡y | lt y<b3 = merge-list<-step< b1 xs b3 [] (𝒟.≡-transl x≡y y<b3) (go≤ xs ys [] (weaken-< b1 xs b2 ys xs<ys) ys<zs) 
-      ... | eq x≡y | eq y≡b3 = merge-list<-step≡ b1 xs b3 [] (x≡y ∙ y≡b3) (go xs ys [] xs<ys ys<zs) 
+      ... | lt x<y | lt y<b3 = merge-list<-step< b1 xs b3 [] (𝒟.<-trans x<y y<b3) (go≤ xs ys [] xs<ys ys<zs)
+      ... | lt x<y | eq y≡b3 = merge-list<-step< b1 xs b3 [] (𝒟.≡-transr x<y y≡b3) (go≤ xs ys [] xs<ys (weaken-< b2 ys b3 [] ys<zs))
+      ... | eq x≡y | lt y<b3 = merge-list<-step< b1 xs b3 [] (𝒟.≡-transl x≡y y<b3) (go≤ xs ys [] (weaken-< b1 xs b2 ys xs<ys) ys<zs)
+      ... | eq x≡y | eq y≡b3 = merge-list<-step≡ b1 xs b3 [] (x≡y ∙ y≡b3) (go xs ys [] xs<ys ys<zs)
       go (x ∷ xs) (y ∷ ys) (z ∷ zs) xs<ys ys<zs with cmp x y | cmp y z
-      ... | lt x<y | lt y<z = merge-list<-step< b1 xs b3 zs (𝒟.<-trans x<y y<z) (go≤ xs ys zs xs<ys ys<zs) 
-      ... | lt x<y | eq y≡z = merge-list<-step< b1 xs b3 zs (𝒟.≡-transr x<y y≡z) (go≤ xs ys zs xs<ys (weaken-< b2 ys b3 zs ys<zs)) 
-      ... | eq x≡y | lt y<z = merge-list<-step< b1 xs b3 zs (𝒟.≡-transl x≡y y<z) (go≤ xs ys zs (weaken-< b1 xs b2 ys xs<ys) ys<zs) 
-      ... | eq x≡y | eq y≡z = merge-list<-step≡ b1 xs b3 zs (x≡y ∙ y≡z) (go xs ys zs xs<ys ys<zs) 
+      ... | lt x<y | lt y<z = merge-list<-step< b1 xs b3 zs (𝒟.<-trans x<y y<z) (go≤ xs ys zs xs<ys ys<zs)
+      ... | lt x<y | eq y≡z = merge-list<-step< b1 xs b3 zs (𝒟.≡-transr x<y y≡z) (go≤ xs ys zs xs<ys (weaken-< b2 ys b3 zs ys<zs))
+      ... | eq x≡y | lt y<z = merge-list<-step< b1 xs b3 zs (𝒟.≡-transl x≡y y<z) (go≤ xs ys zs (weaken-< b1 xs b2 ys xs<ys) ys<zs)
+      ... | eq x≡y | eq y≡z = merge-list<-step≡ b1 xs b3 zs (x≡y ∙ y≡z) (go xs ys zs xs<ys ys<zs)
 
   --------------------------------------------------------------------------------
   -- Heterogenous Compositions
@@ -919,7 +919,7 @@ module NearlyConst
       ... | eq x≡b2 = step< xs [] [] (𝒟.≡-transl x≡b2 b2<b3) xs≤ys (inr b2<b3)
       go (x ∷ xs) [] (z ∷ zs) xs≤ys ys<zs with cmp x b2 | cmp b2 z
       ... | lt x<b2 | lt b2<z = step< xs [] zs (𝒟.<-trans x<b2 b2<z) xs≤ys ys<zs
-      ... | lt x<b2 | eq b2≡z = step< xs [] zs (𝒟.≡-transr x<b2 b2≡z) xs≤ys (weaken-< b2 [] b3 zs ys<zs) 
+      ... | lt x<b2 | eq b2≡z = step< xs [] zs (𝒟.≡-transr x<b2 b2≡z) xs≤ys (weaken-< b2 [] b3 zs ys<zs)
       ... | eq x≡b2 | lt b2<z = step< xs [] zs (𝒟.≡-transl x≡b2 b2<z) xs≤ys ys<zs
       ... | eq x≡b2 | eq b2≡z = step≤ xs [] zs (inl (x≡b2 ∙ b2≡z)) xs≤ys ys<zs
       go (x ∷ xs) (y ∷ ys) [] xs≤ys ys<zs with cmp x y | cmp y b3
@@ -1041,7 +1041,7 @@ module NearlyConst
         |> ⊎-mapl $ λ p →
           let ys≡[] : ys ≡ []
               ys≡[] = bwd-inj $ ap elts (sym p)
-              
+
               b1≡b2 : b1 ≡ b2
               b1≡b2 = ap base p
 
@@ -1055,7 +1055,7 @@ module NearlyConst
         |> ⊎-mapl $ λ p →
           let xs≡[] : xs ≡ []
               xs≡[] = bwd-inj $ ap elts p
-              
+
               b1≡b2 : b1 ≡ b2
               b1≡b2 = ap base p
 
@@ -1299,7 +1299,7 @@ module NearlyConst
     index b (fwd (compact b (([] #r x) ◁⊗ xs))) (suc n)         ≡⟨ ap (λ ϕ → index b (fwd (compact b ϕ)) (suc n)) (◁⊗-bwd ([] #r x) xs) ⟩
     index b (fwd (compact b (([] #r x) ++r bwd xs))) (suc n)    ≡⟨ ap (λ ϕ → index b (fwd ϕ) (suc n)) (compact-++r ([] #r x) (bwd xs) (cs #r c) (p ∙ sym cs#r-compact)) ⟩
     index b (fwd (compact b (([] #r x) ++r (cs #r c)))) (suc n) ≡⟨ ap (λ ϕ → index b (fwd ϕ) (suc n)) (compact-done (([] #r x) ++r cs) c≠base) ⟩
-    index b (fwd ((([] #r x) ++r cs) #r c)) (suc n)             ≡⟨ ap (λ ϕ → index b ϕ (suc n)) (fwd-++r ([] #r x) (cs #r c)) ⟩     
+    index b (fwd ((([] #r x) ++r cs) #r c)) (suc n)             ≡⟨ ap (λ ϕ → index b ϕ (suc n)) (fwd-++r ([] #r x) (cs #r c)) ⟩
     index b (fwd (cs #r c)) n                                   ≡˘⟨ ap (λ ϕ → index b (fwd ϕ) n) p ⟩
     index b (fwd (compact b (bwd xs))) n                        ≡⟨ index-compact b xs n ⟩
     index b xs n ∎
diff --git a/src/Mugen/Algebra/Displacement/NonPositive.agda b/src/Mugen/Algebra/Displacement/NonPositive.agda
index be024d7..d741bf3 100644
--- a/src/Mugen/Algebra/Displacement/NonPositive.agda
+++ b/src/Mugen/Algebra/Displacement/NonPositive.agda
@@ -49,7 +49,7 @@ NonPositive+⊆Int+ = to-displacement-subalgebra subalg where
   subalg : make-displacement-subalgebra NonPositive+ Int+
   subalg .make-displacement-subalgebra.into x = - x
   subalg .make-displacement-subalgebra.pres-ε = refl
-  subalg .make-displacement-subalgebra.pres-⊗ = +ℤ-negate 
+  subalg .make-displacement-subalgebra.pres-⊗ = +ℤ-negate
   subalg .make-displacement-subalgebra.strictly-mono x y = negate-anti-mono y x
   subalg .make-displacement-subalgebra.inj = negate-inj _ _
 
diff --git a/src/Mugen/Algebra/Displacement/Product.agda b/src/Mugen/Algebra/Displacement/Product.agda
index 43df39f..732a509 100644
--- a/src/Mugen/Algebra/Displacement/Product.agda
+++ b/src/Mugen/Algebra/Displacement/Product.agda
@@ -163,7 +163,7 @@ module ProductProperties {o r} {𝒟₁ 𝒟₂ : Displacement-algebra o r}
 
       ⊗×-right-invariant : ∀ x y z → x ⊗×≤ y → (x ⊗× z) ⊗×≤ (y ⊗× z)
       ⊗×-right-invariant x y z (both≤ x1≤y1 x2≤y2) = both≤ (𝒟₁-ordered-monoid.right-invariant x1≤y1) (𝒟₂-ordered-monoid.right-invariant x2≤y2)
-        
+
   --------------------------------------------------------------------------------
   -- Joins
 
diff --git a/src/Mugen/Algebra/OrderedMonoid.agda b/src/Mugen/Algebra/OrderedMonoid.agda
index c3c509c..5409252 100644
--- a/src/Mugen/Algebra/OrderedMonoid.agda
+++ b/src/Mugen/Algebra/OrderedMonoid.agda
@@ -29,14 +29,14 @@ record is-ordered-monoid
   field
     has-is-monoid : is-monoid ε _⊗_
     invariant     : ∀ {w x y z} → w ≤ y → x ≤ z → (w ⊗ x) ≤ (y ⊗ z)
-    
+
   open is-monoid has-is-monoid public
 
   left-invariant : ∀ {x y z} → y ≤ z → (x ⊗ y) ≤ (x ⊗ z)
   left-invariant y≤z = invariant ≤-refl y≤z
 
   right-invariant : ∀ {x y z} → x ≤ y → (x ⊗ z) ≤ (y ⊗ z)
-  right-invariant x≤y = invariant x≤y ≤-refl 
+  right-invariant x≤y = invariant x≤y ≤-refl
 
 record Ordered-monoid-on {o r : Level} (A : Poset o r) : Type (o ⊔ lsuc r) where
   field
diff --git a/src/Mugen/Cat/HierarchyTheory/Properties.agda b/src/Mugen/Cat/HierarchyTheory/Properties.agda
index a8af376..9ccd2fa 100644
--- a/src/Mugen/Cat/HierarchyTheory/Properties.agda
+++ b/src/Mugen/Cat/HierarchyTheory/Properties.agda
@@ -91,7 +91,7 @@ module _ {o r} (H : Hierarchy-theory o r) (Δ : Strict-order o r) (Ψ : Set (lsu
     ι₁-monic g h p = ext λ α →
       inl-inj (inr-inj (p #ₚ α))
 
-  
+
   --------------------------------------------------------------------------------
   -- Construction of the functor T
   -- Section 3.4, Lemma 3.8
diff --git a/src/Mugen/Data/Coimage.agda b/src/Mugen/Data/Coimage.agda
index a15011c..986b1a6 100644
--- a/src/Mugen/Data/Coimage.agda
+++ b/src/Mugen/Data/Coimage.agda
@@ -127,7 +127,7 @@ Coim-map₂ : ∀ {f : A → B}
             → Coim f → Coim f → Coim f
 Coim-map₂ h h-pres = Coim-rec₂ squash
   (λ x y → inc (h x y))
-  (λ w x y z p q → glue (h w y) (h x z) (h-pres w x y z p q)) 
+  (λ w x y z p q → glue (h w y) (h x z) (h-pres w x y z p q))
 
 
 module Coim-Path (f : A → B) (B-set : is-set B) where
@@ -157,4 +157,4 @@ module Coim-Path (f : A → B) (B-set : is-set B) where
 
   Coim-effectful : ∀ {x y} → Path (Coim f) (inc x) (inc y) → f x ≡ f y
   Coim-effectful = Coim-path
-          
+
diff --git a/src/Mugen/Data/Int.agda b/src/Mugen/Data/Int.agda
index 65e4ea1..d17086f 100644
--- a/src/Mugen/Data/Int.agda
+++ b/src/Mugen/Data/Int.agda
@@ -336,8 +336,8 @@ diff-negsuc-< zero zero = tt
 diff-negsuc-< zero (suc y) = <-suc y
 diff-negsuc-< (suc x) zero = tt
 diff-negsuc-< (suc x) (suc y) = begin-<
-  negsuc (suc y) <⟨ -1ℤ-< (negsuc y) ⟩ 
-  negsuc y       <⟨ diff-negsuc-< x y ⟩ 
+  negsuc (suc y) <⟨ -1ℤ-< (negsuc y) ⟩
+  negsuc y       <⟨ diff-negsuc-< x y ⟩
   diff x y       <∎
 
 diff-left-invariant : ∀ x y z → z < y → diff x y <ℤ diff x z
@@ -425,7 +425,7 @@ negate-anti-mono (suc x) (suc y) (s≤s x<y) = x<y
 
 ℤ-Strict-order : Strict-order lzero lzero
 ℤ-Strict-order = to-strict-order mk where
-  mk : make-strict-order _ _ 
+  mk : make-strict-order _ _
   mk .make-strict-order._<_ = _<ℤ_
   mk .make-strict-order.<-irrefl = <ℤ-irrefl _
   mk .make-strict-order.<-trans = <ℤ-trans _ _ _
diff --git a/src/Mugen/Data/List.agda b/src/Mugen/Data/List.agda
index 782b4e2..7165752 100644
--- a/src/Mugen/Data/List.agda
+++ b/src/Mugen/Data/List.agda
@@ -22,7 +22,7 @@ module _ {ℓ} {A : Type ℓ} (aset : is-set A) where
 
   ++-is-magma : is-magma {A = List A} _++_
   ++-is-magma .has-is-set = ListPath.List-is-hlevel 0 aset
-  
+
   ++-is-semigroup : is-semigroup {A = List A} _++_
   ++-is-semigroup .has-is-magma = ++-is-magma
   ++-is-semigroup .associative {x} {y} {z} = sym (++-assoc x y z)
@@ -69,7 +69,7 @@ replicater (suc n) a = replicater n a #r a
 -- Left action of backwards lists upon lists.
 _⊗▷_ : Bwd A → List A → List A
 [] ⊗▷ ys = ys
-(xs #r x) ⊗▷ ys = xs ⊗▷ (x ∷ ys) 
+(xs #r x) ⊗▷ ys = xs ⊗▷ (x ∷ ys)
 
 -- Right action of lists upon backwards lists.
 _◁⊗_ : Bwd A → List A → Bwd A
@@ -182,7 +182,7 @@ Bwd-is-hlevel n ahl = is-hlevel≃ (2 + n) Bwd≃List (List-is-hlevel n ahl)
 
 instance
   H-Level-Bwd : ∀ {n} {k} → ⦃ H-Level A (2 + n) ⦄ → H-Level (Bwd A) (2 + n + k)
-  H-Level-Bwd {n = n} ⦃ x ⦄ = 
+  H-Level-Bwd {n = n} ⦃ x ⦄ =
     basic-instance (2 + n) (Bwd-is-hlevel n (H-Level.has-hlevel x))
 
 
diff --git a/src/Mugen/Order/Coproduct.agda b/src/Mugen/Order/Coproduct.agda
index b2bcc6d..1b5c41f 100644
--- a/src/Mugen/Order/Coproduct.agda
+++ b/src/Mugen/Order/Coproduct.agda
@@ -26,7 +26,7 @@ module Strict-order-coproduct
   inl x ⊕≤ inl y = x A.≤ y
   inl x ⊕≤ inr y = Lift _ ⊥
   inr x ⊕≤ inl y = Lift _ ⊥
-  inr x ⊕≤ inr y = x B.≤ y 
+  inr x ⊕≤ inr y = x B.≤ y
 
   from-⊕≤ : (x y : ⌞ A ⌟ ⊎ ⌞ B ⌟) → x ⊕≤ y → non-strict _⊕<_ x y
   from-⊕≤ (inl x) (inl y) (inl x≡y) = inl (ap inl x≡y)
diff --git a/src/Mugen/Order/LeftInvariantRightCentered.agda b/src/Mugen/Order/LeftInvariantRightCentered.agda
index e3aca94..c36e6ab 100644
--- a/src/Mugen/Order/LeftInvariantRightCentered.agda
+++ b/src/Mugen/Order/LeftInvariantRightCentered.agda
@@ -43,13 +43,13 @@ module _ {o r} {A B : Strict-order o r} {b : ⌞ B ⌟} where
        → (a3≡a4 : fst y ≡ fst z) → (b3<b4 : snd y B.< snd z)
        → P (biased a1≡a2 b1<b2) (biased a3≡a4 b3<b4))
     → (∀ (a1≡a2 : fst w ≡ fst x) → (b1<b2 : snd w B.< snd x)
-       → (a3<a4 : fst y A.< fst z) → (b3≤b : snd y B.≤ b) → (b≤b4 : b B.≤ snd z) 
+       → (a3<a4 : fst y A.< fst z) → (b3≤b : snd y B.≤ b) → (b≤b4 : b B.≤ snd z)
        → P (biased a1≡a2 b1<b2) (centred a3<a4 b3≤b b≤b4))
     → (∀ (a1<a2 : fst w A.< fst x) → (b1≤b : snd w B.≤ b) → (b≤b2 : b B.≤ snd x)
        → (a3≡a4 : fst y ≡ fst z) → (b3<b4 : snd y B.< snd z)
        → P (centred a1<a2 b1≤b b≤b2) (biased a3≡a4 b3<b4))
     → (∀ (a1<a2 : fst w A.< fst x) → (b1≤b : snd w B.≤ b) → (b≤b2 : b B.≤ snd x)
-       → (a3<a4 : fst y A.< fst z) → (b3≤b : snd y B.≤ b) → (b≤b4 : b B.≤ snd z) 
+       → (a3<a4 : fst y A.< fst z) → (b3≤b : snd y B.≤ b) → (b≤b4 : b B.≤ snd z)
        → P (centred a1<a2 b1≤b b≤b2) (centred a3<a4 b3≤b b≤b4))
     → (∀ p q → is-prop (P p q))
     → ∀ p q → P p q
@@ -100,4 +100,4 @@ A ⋉ B [ b ] = to-strict-order order where
   order .make-strict-order.<-irrefl {x} = ⋉-irrefl x
   order .make-strict-order.<-trans {x} {y} {z} = ⋉-trans x y z
   order .make-strict-order.<-thin = trunc
-  order .make-strict-order.has-is-set = ×-is-hlevel 2 A.has-is-set B.has-is-set 
+  order .make-strict-order.has-is-set = ×-is-hlevel 2 A.has-is-set B.has-is-set
diff --git a/src/Mugen/Order/README.md b/src/Mugen/Order/README.md
index 6385cd7..a1d13d9 100644
--- a/src/Mugen/Order/README.md
+++ b/src/Mugen/Order/README.md
@@ -1,7 +1,7 @@
 # Order Theory
 
 This directory consists of the definition of a strict order, along with a handful
-of useful instance. These are mostly used in the definition of the 
+of useful instance. These are mostly used in the definition of the
 [category of strict orders](https://github.com/RedPRL/agda-mugen/blob/main/src/Mugen/Cat/StrictOrders.agda),
 as well as the definition of [displacement algebras](https://github.com/RedPRL/agda-mugen/blob/main/src/Mugen/Algebra/Displacement.agda)
 and their various [instances](https://github.com/RedPRL/agda-mugen/blob/main/src/Mugen/Algebra/Displacement/)
diff --git a/src/Mugen/Prelude.agda b/src/Mugen/Prelude.agda
index 6be0970..83103b0 100644
--- a/src/Mugen/Prelude.agda
+++ b/src/Mugen/Prelude.agda
@@ -27,8 +27,8 @@ dec-map to from (yes p) = yes (to p)
 dec-map to from (no ¬p) = no (λ q → ¬p (from q))
 
 record
-  Right-actionlike {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} 
-    ⦃ au : Underlying A ⦄ ⦃ bu : Underlying B ⦄ 
+  Right-actionlike {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'}
+    ⦃ au : Underlying A ⦄ ⦃ bu : Underlying B ⦄
     (F : A → B → Type ℓ'') : Typeω where
   field
     ⟦_⟧ʳ : ∀ {A B} → F A B → ⌞ A ⌟ → ⌞ B ⌟ → ⌞ A ⌟
@@ -41,7 +41,7 @@ open Right-actionlike ⦃...⦄ public
 
 subst₂ : ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁} {B : Type ℓ₂} (P : A → B → Type ℓ₃) {a1 a2 : A} {b1 b2 : B}
        → a1 ≡ a2 → b1 ≡ b2 → P a1 b1 → P a2 b2
-subst₂ P p q x = subst (λ a → P a _) p (subst (λ b → P _ b) q x) 
+subst₂ P p q x = subst (λ a → P a _) p (subst (λ b → P _ b) q x)
 
 record Reveal_·_is_ {a b} {A : Type a} {B : A → Type b}
                     (f : (x : A) → B x) (x : A) (y : B x) :
@@ -60,4 +60,4 @@ x |> f = f x
 {-# INLINE _|>_ #-}
 
 over : ∀ {ℓ} {A : Type ℓ} {x y : A} {f : A → A} → (∀ x → f x ≡ x) → f x ≡ f y → x ≡ y
-over {x = x} {y = y} p q =  sym (p x) ·· q ·· p y 
+over {x = x} {y = y} p q =  sym (p x) ·· q ·· p y