Merge pull request #11 from jkopanski/fix-whitespace

Fix whitespace

fix-whitespace.yaml

@@ -0,0 +1,13 @@
+included-dirs:
+  - src
+
+included-files:
+  - "*.agda"
+  - "*.md"
+  - "*.org"
+  - "*.nix"
+
+excluded-dirs:
+  - .git
+  - .direnv
+  - result

flake.nix

@@ -21,10 +21,22 @@
         agdaWithStandardLibrary = pkgs.agda.withPackages (_: [ standard-library ]);
 
       in {
-        devShell = pkgs.mkShell {
+        checks.whitespace = pkgs.stdenvNoCC.mkDerivation {
+          name = "check-whitespace";
+          dontBuild = true;
+          src = ./.;
+          doCheck = true;
+          checkPhase = ''
+            ${pkgs.haskellPackages.fix-whitespace}/bin/fix-whitespace --check
+          '';
+          installPhase = ''mkdir "$out"'';
+        };
+
+        devShells.default = pkgs.mkShell {
           buildInputs = [
             agdaWithStandardLibrary
             pkgs.graphviz
+            pkgs.haskellPackages.fix-whitespace
           ];
         };
 

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 _⇨₁_ ⦄

src/Felix/Construct/Product.agda

@@ -202,7 +202,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 _⇨₁_

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)
 

src/Felix/Instances/Function/Lift.agda

@@ -60,6 +60,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 }

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 }
 

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