From efd7a8463152199cff0ad2089ee9dd5d317b5e6c Mon Sep 17 00:00:00 2001 From: depsterr Date: Sat, 8 Oct 2022 13:21:59 +0200 Subject: [PATCH] CwFs: grammatical error (last small commit today, I promise) --- src/CwF.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/CwF.lagda.md b/src/CwF.lagda.md index 1f8e4c6..2988c6b 100644 --- a/src/CwF.lagda.md +++ b/src/CwF.lagda.md @@ -55,7 +55,7 @@ record is-CwF {o h f : _} (𝓒 : Precategory o h) : Type (lsuc (o ⊔ h ⊔ f)) 𝓕 : Functor (𝓒 ^op) (Fams f) ``` -Two functions, $Ty$ and $Tm$ are defined in terms of $\mathcal F$, giving a contexts set of syntactic types, and terms respectively. +Two functions, $Ty$ and $Tm$ are defined in terms of $\mathcal F$, giving a context's set of syntactic types, and terms respectively. ``` open Precategory 𝓒 open Functor 𝓕