CwFs: grammatical error (last small commit today, I promise)
This commit is contained in:
parent
79d8c80446
commit
efd7a84631
|
@ -55,7 +55,7 @@ record is-CwF {o h f : _} (𝓒 : Precategory o h) : Type (lsuc (o ⊔ h ⊔ f))
|
||||||
𝓕 : Functor (𝓒 ^op) (Fams 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 Precategory 𝓒
|
||||||
open Functor 𝓕
|
open Functor 𝓕
|
||||||
|
|
Loading…
Reference in New Issue
Block a user