chore: typos

src/Cat/Diagram/Colimit/Base.lagda.md

@@ -652,9 +652,9 @@ is-cocontinuous oshape hshape {C = C} F =
   → preserves-colimit F Diagram
 ```
 
-## Cocompleteness
+# Cocompleteness
 
-A category is **cocomplete** if admits for limits of arbitrary shape.
+A category is **cocomplete** if it admits colimits for diagrams of arbitrary shape.
 However, in the presence of excluded middle, if a category admits
 coproducts indexed by its class of morphisms, then it is automatically
 [thin]. Since excluded middle is independent of type theory, we can not

src/Cat/Diagram/Limit/Base.lagda.md

@@ -237,7 +237,7 @@ triangles
 
 The rest of the data says that $\psi$ is the universal family of maps
 with this property: If $\eta_j : x \to Fj$ is another family of maps
-with the same commutativty property, then each $\eta_j$ factors through
+with the same commutativity property, then each $\eta_j$ factors through
 the apex by a single, _unique_ universal morphism:
 
 ```agda