Fix a minor grammar mistake in Structure.agda

agda · Sep 21, 2023 · 7c9714c · 7c9714c
1 parent f3cf89d
commit 7c9714c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Cubical/Foundations/Structure.agda b/Cubical/Foundations/Structure.agda
@@ -10,7 +10,7 @@ private
     S : Type ℓ → Type ℓ'
 
 -- A structure is a type-family S : Type ℓ → Type ℓ', i.e. for X : Type ℓ and s : S X,
--- the pair (X , s) : TypeWithStr ℓ S means that X is equipped with a S-structure, witnessed by s.
+-- the pair (X , s) : TypeWithStr ℓ S means that X is equipped with an S-structure, witnessed by s.
 
 TypeWithStr : (ℓ : Level) (S : Type ℓ → Type ℓ') → Type (ℓ-max (ℓ-suc ℓ) ℓ')
 TypeWithStr ℓ S = Σ[ X ∈ Type ℓ ] S X