Fix typos

UniMath · Dec 12, 2023 · 4597882 · 4597882
1 parent d8b96bb
commit 4597882
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/foundation/commuting-triangles-of-identifications.lagda.md b/src/foundation/commuting-triangles-of-identifications.lagda.md
@@ -107,10 +107,10 @@ of these transformations are equivalences.
 
 These lemmas are useful in proofs involving path algebra, because taking
 `equiv-right-whisk-triangle-identicications` as an example, it provides us with
-two maps: the forward direcation states `(p ＝ q ∙ r) → (p ∙ s ＝ q ∙ (r ∙ s))`,
+two maps: the forward direction states `(p ＝ q ∙ r) → (p ∙ s ＝ q ∙ (r ∙ s))`,
 which allows one to append an identification without needing to reassociate on
-the right, and the backwards direction conversely allows one to concel out an
-identification in parantheses.
+the right, and the backwards direction conversely allows one to cancel out an
+identification in parentheses.
 
 ```agda
 module _

diff --git a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md
@@ -35,7 +35,7 @@ open import synthetic-homotopy-theory.universal-property-sequential-colimits
 
 The {{#concept "flattening lemma" Disambiguation="sequential colimits"}} for
 [sequential colimits](synthetic-homotopy-theory.universal-property-sequential-colimits.md)
-states that coequalizers commute with
+states that sequential colimits commute with
 [dependent pair types](foundation.dependent-pair-types.md). Specifically, given
 a [cocone](synthetic-homotopy-theory.cocones-under-sequential-diagrams.md)