From 7c9714cbcfb77a93a5cd4a3931fba977c6b39866 Mon Sep 17 00:00:00 2001 From: Shreck Ye Date: Thu, 21 Sep 2023 19:23:01 +0800 Subject: [PATCH] Fix a minor grammar mistake in Structure.agda --- Cubical/Foundations/Structure.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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