Merge pull request #247 from FintanH/patch-2

fix typo
agda · Feb 12, 2021 · 29e969b · 29e969b
2 parents 3ef03f7 + c48bbba
commit 29e969b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Categories/Category/Core.agda b/src/Categories/Category/Core.agda
@@ -54,7 +54,7 @@ record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
     ; isEquivalence = equiv
     }
 
-  -- When a category is quatified, it is convenient to refer to the levels from a module,
+  -- When a category is quantified, it is convenient to refer to the levels from a module,
   -- so we do not have to explicitly quantify over a category when universe levels do not
   -- play a big part in a proof (which is the case probably all the time).
   o-level : Level