pre-commit

UniMath · Dec 8, 2023 · c1d761e · c1d761e
1 parent da28830
commit c1d761e
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/src/foundation/commuting-triangles-of-identifications.lagda.md b/src/foundation/commuting-triangles-of-identifications.lagda.md
@@ -50,7 +50,7 @@ module _
   coherence-triangle-identifications' left right top = (top ∙ right) ＝ left
 ```
 
-### Properties
+## Properties
 
 ### Whiskering of triangles of identifications
 

diff --git a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md
@@ -116,7 +116,6 @@ so it suffices to invoke the flattening lemma for coequalizers.
 **Proof:** The diagram we construct is
 
 ```text
-
                              --------->
   Σ ((n, a) : Σ ℕ A) P(iₙ a) ---------> Σ ((n, a) : Σ ℕ A) P(iₙ a) -----> Σ (x : X) P(x)
             |                                     |                            |
-Original file line number
+Diff line change
@@ Expand Up @@
     **Proof:** The diagram we construct is
     ```text
                                  --------->
       Σ ((n, a) : Σ ℕ A) P(iₙ a) ---------> Σ ((n, a) : Σ ℕ A) P(iₙ a) -----> Σ (x : X) P(x)
                 |                                     |                            |
@@ Expand Down @@