From ef4b9faddd9b1a44c26db8aa86e3f3d438351120 Mon Sep 17 00:00:00 2001 From: Erik Post Date: Wed, 22 Mar 2023 21:46:03 +0100 Subject: [PATCH] Fix typos in comments --- src/Categories/Category.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Categories/Category.agda b/src/Categories/Category.agda index 92e00cc43..c00d1ceb4 100644 --- a/src/Categories/Category.agda +++ b/src/Categories/Category.agda @@ -10,10 +10,10 @@ private variable o ℓ e : Level --- Convenience functions for working over mupliple categories at once: +-- Convenience functions for working over multiple categories at once: -- C [ x , y ] (for x y objects of C) - Hom_C(x , y) -- C [ f ≈ g ] (for f g arrows of C) - that f and g are equivalent arrows --- C [ f ∘ g ] (for f g composables arrows of C) - composition in C +-- C [ f ∘ g ] (for f g composable arrows of C) - composition in C infix 10 _[_,_] _[_≈_] _[_∘_] _[_,_] : (C : Category o ℓ e) → (X : Category.Obj C) → (Y : Category.Obj C) → Set ℓ