diff --git a/Cubical/Foundations/Structure.agda b/Cubical/Foundations/Structure.agda
index 87b2b5bf62..099bb8a2eb 100644
--- 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