pre-commit

CODINGSTYLE.md

@@ -128,8 +128,12 @@ strategic endeavour to ensure the longevity, vitality, and success of the
     a = construction-of-a
   ```
 
-- **Lambda expressions**: When a lambda expression appears as the argument of a function, we always wrap it in parentheses. We do this even if it is the last argument of a function, and thus isn't strictly required to
-  be parenthesized. Note that in some rare cases, a lambda expression might appear at the top level. In this case we don't require the lambda expression to be parenthesized.
+- **Lambda expressions**: When a lambda expression appears as the argument of a
+  function, we always wrap it in parentheses. We do this even if it is the last
+  argument of a function, and thus isn't strictly required to be parenthesized.
+  Note that in some rare cases, a lambda expression might appear at the top
+  level. In this case we don't require the lambda expression to be
+  parenthesized.
 
   There are multiple syntaxes for writing lambda expressions in Agda. Generally,
   you have the following options:

src/foundation/isolated-elements.lagda.md

@@ -213,8 +213,7 @@ is-prop-is-isolated :
   {l1 : Level} {A : UU l1} (a : A) → is-prop (is-isolated a)
 is-prop-is-isolated a =
   is-prop-is-inhabited
-    ( λ H →
-      is-prop-Π (λ x → is-prop-is-decidable (is-prop-eq-isolated-element a H x)))
+    ( λ H → is-prop-Π (is-prop-is-decidable ∘ is-prop-eq-isolated-element a H))
 
 is-isolated-Prop :
   {l1 : Level} {A : UU l1} (a : A) → Prop l1
@@ -327,7 +326,8 @@ is-retraction-map-inv-maybe-structure-isolated-element :
   {l1 : Level} (X : UU l1) (x : isolated-element X) →
   ( map-inv-maybe-structure-isolated-element X x ∘
     map-maybe-structure-isolated-element X x) ~ id
-is-retraction-map-inv-maybe-structure-isolated-element X (x , dx) (inl (y , f)) =
+is-retraction-map-inv-maybe-structure-isolated-element
+  X (x , dx) (inl (y , f)) =
   ap
     ( cases-map-inv-maybe-structure-isolated-element X (x , dx) y)
     ( eq-is-prop (is-prop-is-decidable (is-prop-eq-isolated-element x dx y)))