Fix current white space violations

conal · Feb 6, 2024 · cf526fc · cf526fc
1 parent 2e7c521
commit cf526fc
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 6 deletions.
diff --git a/src/Felix/Construct/Comma.agda b/src/Felix/Construct/Comma.agda
@@ -9,7 +9,7 @@ open import Felix.Homomorphism
 
 module Felix.Construct.Comma
    {o₀}{obj₀ : Set o₀} {ℓ₀} (_⇨₀_ : obj₀ → obj₀ → Set ℓ₀) ⦃ _ : Category _⇨₀_ ⦄
-   {o₁}{obj₁ : Set o₁} {ℓ₁} (_⇨₁_ : obj₁ → obj₁ → Set ℓ₁) ⦃ _ : Category _⇨₁_ ⦄ 
+   {o₁}{obj₁ : Set o₁} {ℓ₁} (_⇨₁_ : obj₁ → obj₁ → Set ℓ₁) ⦃ _ : Category _⇨₁_ ⦄
    {o₂}{obj₂ : Set o₂} {ℓ₂} (_⇨₂_ : obj₂ → obj₂ → Set ℓ₂) ⦃ _ : Category _⇨₂_ ⦄
    {q₀} ⦃ _ : Equivalent q₀ _⇨₀_ ⦄ ⦃ _ : L.Category _⇨₀_ ⦄
    {q₁} ⦃ _ : Equivalent q₁ _⇨₁_ ⦄ -- ⦃ _ : L.Category _⇨₁_ ⦄

diff --git a/src/Felix/Construct/Product.agda b/src/Felix/Construct/Product.agda
@@ -203,7 +203,7 @@ module product-homomorphisms where instance
 --     → BooleanH Obj _⇨₂_
 --   booleanH₂ = record { β = id ; β⁻¹ = id }
 
---   strongBooleanH₁ : 
+--   strongBooleanH₁ :
 --       ∀ {q₁} ⦃ _ : Equivalent q₁ _⇨₁_ ⦄ ⦃ _ : Boolean obj₁ ⦄ ⦃ _ : Boolean obj₂ ⦄
 --       ⦃ _ : L.Category _⇨₁_ ⦄
 --     → StrongBooleanH Obj _⇨₁_

diff --git a/src/Felix/Instances/CAT.agda b/src/Felix/Instances/CAT.agda
@@ -73,7 +73,7 @@ toH (mk⤇ Fₒ Fₘ) = record { Fₘ = Fₘ }
 it-⤇ : ∀
   {obj₁ : Set o} {_⇨₁_ : obj₁ → obj₁ → Set ℓ}
   {obj₂ : Set o} {_⇨₂_ : obj₂ → obj₂ → Set ℓ}
-  ⦃ Hₒ : Homomorphismₒ obj₁ obj₂ ⦄ ⦃ H : Homomorphism _⇨₁_ _⇨₂_ ⦄ → 
+  ⦃ Hₒ : Homomorphismₒ obj₁ obj₂ ⦄ ⦃ H : Homomorphism _⇨₁_ _⇨₂_ ⦄ →
   cat _⇨₁_ ⤇ cat _⇨₂_
 it-⤇ ⦃ Hₒ = Hₒ ⦄ ⦃ H = H ⦄ = mk⤇ (Homomorphismₒ.Fₒ Hₒ) (Homomorphism.Fₘ H)
 

diff --git a/src/Felix/Instances/Function/Lift.agda b/src/Felix/Instances/Function/Lift.agda
@@ -42,6 +42,6 @@ module function-lift-instances where instance
   cartH : CartesianH (_⇾_ {a}) (_⇾_ {a ⊔ b})
   cartH = record
      { F-!   = λ _ → refl
-     ; F-▵   = λ _ → refl 
+     ; F-▵   = λ _ → refl
      ; F-exl = λ _ → refl
      ; F-exr = λ _ → refl }
diff --git a/src/Felix/Instances/Pred.agda b/src/Felix/Instances/Pred.agda
@@ -56,7 +56,7 @@ module PRED-functor where instance
 
   H : Homomorphism _⇒_ _⇾_
   H = record { Fₘ = _⇒_.f }
-  
+
   catH : CategoryH _⇒_ _⇾_
   catH = record { F-id = refl ; F-∘ = refl }
 

diff --git a/src/Felix/Raw.agda b/src/Felix/Raw.agda
@@ -157,7 +157,7 @@ record CartesianClosed {obj : Set o}
     : Set (o ⊔ ℓ) where
   private infix 0 _⇨_; _⇨_ = _⇨′_
   field
-    
+
     curry : (a × b ⇨ c) → (a ⇨ (b ⇛ c))
     apply : (a ⇛ b) × a ⇨ b