Fix alignment where blocks (#670)

Resolves #667.

CODINGSTYLE.md

@@ -121,10 +121,11 @@ strategic endeavour to ensure the longevity, vitality, and success of the
 
   ```agda
   statement : Statement
-  statement = proof
+  statement =
+    some-possibly-long-proof a
     where
-    proof : Proof
-    proof = some-very-long-proof
+    a : type-of-a
+    a = construction-of-a
   ```
 
 ## Code comments

FILE-CONVENTIONS.md

@@ -144,7 +144,7 @@ contents of the file.
 - For a template file see [`TEMPLATE.lagda.md`](TEMPLATE.lagda.md).
 
 - An instructive example of a file with the expected structure is
-  [`foundation.cantor-schroder-bernstein-escardo`](https://raw.githubusercontent.com/UniMath/agda-unimath/master/src/foundation/cantor-schroder-bernstein-escardo.lagda.md).
+  [`order-theory.galois-connections`](https://raw.githubusercontent.com/UniMath/agda-unimath/master/src/order-theory/galois-connections.lagda.md).
 
 ## Note
 

HOWTO-INSTALL.md

@@ -197,17 +197,21 @@ in the library.
 ### Contributing
 
 We welcome and appreciate contributions from the community. If you're interested
-in contributing to the `agda-unimath` library, please follow our guidelines and
-best practices, as well as the instructions below to ensure a smooth setup and
-workflow.
+in contributing to the `agda-unimath` library, you can follow the instructions
+below to ensure a smooth setup and workflow. Also, please make sure to follow
+our [coding style](CODINGSTYLE.md) and
+[design principles](DESIGN-PRINCIPLES.md).
 
 #### <a name="pre-commit-hooks"></a>Pre-commit hooks and Python dependencies
 
 The `agda-unimath` library includes [pre-commit](https://pre-commit.com/) hooks
-that enforce [basic formatting rules](CONTRIBUTING.md). To utilize these hooks,
-if you did not install your environment using Nix, you'll need to install the
-`pre-commit` tool and the hooks' Python dependencies. The easiest way to
-accomplish this is by using the Python package manager `pip`.
+that enforce [basic formatting rules](CONTRIBUTING.md). These will inform you of
+some rule violations in your commits, and for most violations they will also
+automatically apply the required changes.
+
+To utilize these hooks, if you did not install your environment using Nix, you
+will need to install the `pre-commit` tool and the hooks' Python dependencies.
+The easiest way to accomplish this is by using the Python package manager `pip`.
 
 First, make sure that you have the latest version of Python and pip installed on
 your computer; the hooks require Python 3.8 or newer. Then run the following
@@ -224,18 +228,6 @@ Now, before you submit a Pull Request (PR) next time, you can run `pre-commit`
 by staging your changes and executing the command `make pre-commit` from the
 repository's main folder.
 
-To have `pre-commit` run automatically before every commit, run the following
-command:
-
-```shell
-pre-commit install
-```
-
-After this, `pre-commit` will inform you of any rule violations in your
-subsequent commits. For most violations, it will also automatically apply the
-required changes. In such cases, simply stage the new changes and commit again.
-To disable this behaviour again, you can run `pre-commit uninstall`.
-
 Keep in mind that `pre-commit` is also a part of the Continuous Integration
 (CI), so any PR that violates the enforced conventions will be automatically
 blocked from merging.

TEMPLATE.lagda.md

@@ -49,7 +49,7 @@ concept-subconcept = ...
 ## See also
 
 - An instructive example of a file with the expected structure is
-  [`foundation.cantor-schroder-bernstein-escardo`](https://raw.githubusercontent.com/UniMath/agda-unimath/master/src/foundation/cantor-schroder-bernstein-escardo.lagda.md).
+  [`order-theory.galois-connections`](https://raw.githubusercontent.com/UniMath/agda-unimath/master/src/order-theory/galois-connections.lagda.md).
 
 ## References
 

src/category-theory/discrete-categories.lagda.md

@@ -28,19 +28,12 @@ module _
   where
 
   discrete-precategory-Set : Precategory l l
-  discrete-precategory-Set =
-    type-Set X , disc-Hom , composition-structure , id-structure
-    where
-      disc-Hom : type-Set X → type-Set X → Set l
-      disc-Hom x y = set-Prop (x ＝ y , is-set-type-Set X x y)
-
-      composition-structure : associative-composition-structure-Set disc-Hom
-      pr1 composition-structure refl refl = refl
-      pr2 composition-structure refl refl refl = refl
-
-      id-structure :
-        is-unital-composition-structure-Set disc-Hom composition-structure
-      pr1 id-structure x = refl
-      pr1 (pr2 id-structure) refl = refl
-      pr2 (pr2 id-structure) refl = refl
+  pr1 discrete-precategory-Set = type-Set X
+  pr1 (pr2 discrete-precategory-Set) x y =
+    set-Prop (x ＝ y , is-set-type-Set X x y)
+  pr1 (pr1 (pr2 (pr2 discrete-precategory-Set))) = concat' _
+  pr2 (pr1 (pr2 (pr2 discrete-precategory-Set))) refl refl refl = refl
+  pr1 (pr2 (pr2 (pr2 discrete-precategory-Set))) x = refl
+  pr1 (pr2 (pr2 (pr2 (pr2 discrete-precategory-Set)))) _ = right-unit
+  pr2 (pr2 (pr2 (pr2 (pr2 discrete-precategory-Set)))) _ = left-unit
 ```

src/category-theory/slice-precategories.lagda.md

@@ -224,59 +224,59 @@ module _
       ϕ (Z , .(comp-hom-Precategory C f h₁)) (h₁ , refl) (h₂ , β₂) =
       is-contr-Σ-is-prop c d q σ
       where
-        c :
-          type-hom-Precategory
-            ( Slice-Precategory C A)
-            ( Z , comp-hom-Precategory C f h₁)
-            ( W , p)
-        pr1 c = pr1 (pr1 (ϕ Z h₁ h₂ β₂))
-        pr2 c =
-          ( ap
-            ( comp-hom-Precategory C f)
-            ( inv (pr1 (pr2 (pr1 (ϕ Z h₁ h₂ β₂)))))) ∙
-          ( inv (associative-comp-hom-Precategory C f p₁ _) ∙
-          ap
-            ( λ k → comp-hom-Precategory C k (pr1 (pr1 (ϕ Z h₁ h₂ β₂))))
-            ( inv α₁))
-
-        d :
-          ( ( comp-hom-Precategory (Slice-Precategory C A) (p₁ , α₁) c) ＝
-            ( h₁ , refl)) ×
-          ( ( comp-hom-Precategory (Slice-Precategory C A) (p₂ , α₂) c) ＝
-            ( h₂ , β₂))
-        pr1 d =
-          eq-hom-Slice-Precategory C A _ _ (pr1 (pr2 (pr1 (ϕ Z h₁ h₂ β₂))))
-        pr2 d =
-          eq-hom-Slice-Precategory C A _ _ (pr2 (pr2 (pr1 (ϕ Z h₁ h₂ β₂))))
-
-        q :
-          ∀ k →
-          is-prop
-            ( ( comp-hom-Precategory
-                (Slice-Precategory C A) (p₁ , α₁) k ＝ (h₁ , refl)) ×
-              ( comp-hom-Precategory
-                (Slice-Precategory C A) (p₂ , α₂) k ＝ (h₂ , β₂)))
-        q k =
-          is-prop-prod
-            ( is-set-type-Set (hom-Slice-Precategory C A _ _) _ _)
-            ( is-set-type-Set (hom-Slice-Precategory C A _ _) _ _)
-
-        σ :
-          ∀ k →
-          ( ( comp-hom-Precategory
-              ( Slice-Precategory C A)
-              ( p₁ , α₁)
-              ( k)) ＝
-            ( h₁ , refl)) ×
+      c :
+        type-hom-Precategory
+          ( Slice-Precategory C A)
+          ( Z , comp-hom-Precategory C f h₁)
+          ( W , p)
+      pr1 c = pr1 (pr1 (ϕ Z h₁ h₂ β₂))
+      pr2 c =
+        ( ap
+          ( comp-hom-Precategory C f)
+          ( inv (pr1 (pr2 (pr1 (ϕ Z h₁ h₂ β₂)))))) ∙
+        ( inv (associative-comp-hom-Precategory C f p₁ _) ∙
+        ap
+          ( λ k → comp-hom-Precategory C k (pr1 (pr1 (ϕ Z h₁ h₂ β₂))))
+          ( inv α₁))
+
+      d :
+        ( ( comp-hom-Precategory (Slice-Precategory C A) (p₁ , α₁) c) ＝
+          ( h₁ , refl)) ×
+        ( ( comp-hom-Precategory (Slice-Precategory C A) (p₂ , α₂) c) ＝
+          ( h₂ , β₂))
+      pr1 d =
+        eq-hom-Slice-Precategory C A _ _ (pr1 (pr2 (pr1 (ϕ Z h₁ h₂ β₂))))
+      pr2 d =
+        eq-hom-Slice-Precategory C A _ _ (pr2 (pr2 (pr1 (ϕ Z h₁ h₂ β₂))))
+
+      q :
+        ∀ k →
+        is-prop
           ( ( comp-hom-Precategory
-              ( Slice-Precategory C A)
-              ( p₂ , α₂)
-              ( k)) ＝
-            ( h₂ , β₂)) →
-          c ＝ k
-        σ (k , γ) (γ₁ , γ₂) =
-          eq-hom-Slice-Precategory C A _ _
-            ( ap pr1 (pr2 (ϕ Z h₁ h₂ β₂) (k , (ap pr1 γ₁ , ap pr1 γ₂))))
+              (Slice-Precategory C A) (p₁ , α₁) k ＝ (h₁ , refl)) ×
+            ( comp-hom-Precategory
+              (Slice-Precategory C A) (p₂ , α₂) k ＝ (h₂ , β₂)))
+      q k =
+        is-prop-prod
+          ( is-set-type-Set (hom-Slice-Precategory C A _ _) _ _)
+          ( is-set-type-Set (hom-Slice-Precategory C A _ _) _ _)
+
+      σ :
+        ∀ k →
+        ( ( comp-hom-Precategory
+            ( Slice-Precategory C A)
+            ( p₁ , α₁)
+            ( k)) ＝
+          ( h₁ , refl)) ×
+        ( ( comp-hom-Precategory
+            ( Slice-Precategory C A)
+            ( p₂ , α₂)
+            ( k)) ＝
+          ( h₂ , β₂)) →
+        c ＝ k
+      σ (k , γ) (γ₁ , γ₂) =
+        eq-hom-Slice-Precategory C A _ _
+          ( ap pr1 (pr2 (ϕ Z h₁ h₂ β₂) (k , (ap pr1 γ₁ , ap pr1 γ₂))))
 
     map-inv-is-pullback-is-product-Slice-Precategory :
       is-product-Precategory
@@ -285,65 +285,65 @@ module _
     map-inv-is-pullback-is-product-Slice-Precategory ψ W' p₁' p₂' α' =
       is-contr-Σ-is-prop k γ q σ
       where
-        k : type-hom-Precategory C W' W
-        k =
-          pr1
+      k : type-hom-Precategory C W' W
+      k =
+        pr1
+          ( pr1
             ( pr1
+              ( ψ
+                ( W' , comp-hom-Precategory C f p₁')
+                ( p₁' , refl)
+                ( p₂' , α'))))
+
+      γ :
+        (comp-hom-Precategory C p₁ k ＝ p₁') ×
+        (comp-hom-Precategory C p₂ k ＝ p₂')
+      pr1 γ =
+        ap pr1
+          ( pr1
+            ( pr2
               ( pr1
                 ( ψ
                   ( W' , comp-hom-Precategory C f p₁')
                   ( p₁' , refl)
-                  ( p₂' , α'))))
-
-        γ :
-          (comp-hom-Precategory C p₁ k ＝ p₁') ×
-          (comp-hom-Precategory C p₂ k ＝ p₂')
-        pr1 γ =
-          ap pr1
-            ( pr1
-              ( pr2
-                ( pr1
-                  ( ψ
-                    ( W' , comp-hom-Precategory C f p₁')
-                    ( p₁' , refl)
-                    ( p₂' , α')))))
-        pr2 γ =
-          ap pr1
+                  ( p₂' , α')))))
+      pr2 γ =
+        ap pr1
+          ( pr2
             ( pr2
-              ( pr2
-                ( pr1
-                  ( ψ
-                    ( W' , comp-hom-Precategory C f p₁')
-                    ( p₁' , refl)
-                    ( p₂' , α')))))
-
-        q :
-          ∀ k' →
-          is-prop
-            (( comp-hom-Precategory C p₁ k' ＝ p₁') ×
-            ( comp-hom-Precategory C p₂ k' ＝ p₂'))
-        q k' =
-          is-prop-prod
-            ( is-set-type-Set (hom-Precategory C _ _) _ _)
-            ( is-set-type-Set (hom-Precategory C _ _) _ _)
-
-        σ :
-          ( k' : type-hom-Precategory C W' W) →
-          ( γ' :
-            ( comp-hom-Precategory C p₁ k' ＝ p₁') ×
-            ( comp-hom-Precategory C p₂ k' ＝ p₂')) →
-            k ＝ k'
-        σ k' (γ₁ , γ₂) =
-          ap
-            ( pr1 ∘ pr1)
-            ( pr2
-              ( ψ (W' , comp-hom-Precategory C f p₁') (p₁' , refl) (p₂' , α'))
-              ( ( ( k') ,
-                  ( ( ap (comp-hom-Precategory C f) (inv γ₁)) ∙
-                    ( ( inv (associative-comp-hom-Precategory C f p₁ k')) ∙
-                      ( ap (λ l → comp-hom-Precategory C l k') (inv α₁))))) ,
-                ( eq-hom-Slice-Precategory C A _ _ γ₁) ,
-                ( eq-hom-Slice-Precategory C A _ _ γ₂)))
+              ( pr1
+                ( ψ
+                  ( W' , comp-hom-Precategory C f p₁')
+                  ( p₁' , refl)
+                  ( p₂' , α')))))
+
+      q :
+        ∀ k' →
+        is-prop
+          (( comp-hom-Precategory C p₁ k' ＝ p₁') ×
+          ( comp-hom-Precategory C p₂ k' ＝ p₂'))
+      q k' =
+        is-prop-prod
+          ( is-set-type-Set (hom-Precategory C _ _) _ _)
+          ( is-set-type-Set (hom-Precategory C _ _) _ _)
+
+      σ :
+        ( k' : type-hom-Precategory C W' W) →
+        ( γ' :
+          ( comp-hom-Precategory C p₁ k' ＝ p₁') ×
+          ( comp-hom-Precategory C p₂ k' ＝ p₂')) →
+          k ＝ k'
+      σ k' (γ₁ , γ₂) =
+        ap
+          ( pr1 ∘ pr1)
+          ( pr2
+            ( ψ (W' , comp-hom-Precategory C f p₁') (p₁' , refl) (p₂' , α'))
+            ( ( ( k') ,
+                ( ( ap (comp-hom-Precategory C f) (inv γ₁)) ∙
+                  ( ( inv (associative-comp-hom-Precategory C f p₁ k')) ∙
+                    ( ap (λ l → comp-hom-Precategory C l k') (inv α₁))))) ,
+              ( eq-hom-Slice-Precategory C A _ _ γ₁) ,
+              ( eq-hom-Slice-Precategory C A _ _ γ₂)))
 
     equiv-is-pullback-is-product-Slice-Precategory :
       is-pullback-Precategory C A X Y f g W p₁ p₂ α ≃