style: remove all trailing whitespace

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′}

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

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 _ _

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
 

src/Mugen/Algebra/Displacement/NearlyConstant.agda

@@ -95,15 +95,15 @@ 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 _
       (λ _ → ⊥)
       (λ _ → ⊤)
       p
 
   -- 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 ∎

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 _ _
 

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
 

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

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

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
-          
+

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 _ _ _

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))