rachel/cwfs
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

CwF: update wording to reflect change from CwF to is-CwF

Browse Source
This commit is contained in:
Rachel Lambda Samuelsson 2022-10-08 13:17:12 +02:00
parent e704dde2a3
commit d31b3ab50b
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/CwF.lagda.md
View File

@ -47,7 +47,7 @@ A Category with families, a CwF, is a category in which we can interpret the syn
This file defines a CwF, without any particular type formers. Here CwFs are thought of as GATs (generalised algebraic theories), as is presented in a paper by Abel, Coquand and Dybjer. [@abd2008] This file defines a CwF, without any particular type formers. Here CwFs are thought of as GATs (generalised algebraic theories), as is presented in a paper by Abel, Coquand and Dybjer. [@abd2008]
A CwF is defined as a precategory $\mathcal C$ equipped with a contravariant functor $\mathcal F : \mathcal C^{op} \to \mathcal Fam$, fufilling the properties listed below. A category $\mathcal C$ is said to be a CwF if there is a contravariant functor $\mathcal F : \mathcal C^{op} \to \mathcal Fam$, and it fufills the laws of the GAT.
``` ```
record is-CwF {o h f : Level} (𝓒 : Precategory o h) : Type (lsuc (o ⊔ h ⊔ f)) where record is-CwF {o h f : Level} (𝓒 : Precategory o h) : Type (lsuc (o ⊔ h ⊔ f)) where
@ -172,4 +172,4 @@ Lastly, it is required that the weakening map behaves as expected under composit
{a : ∣ Tr Δ (A ⟦ δ ⟧) ∣} {a : ∣ Tr Δ (A ⟦ δ ⟧) ∣}
→ ⟨ δ , a ⟩ ∘ γ → ⟨ δ , a ⟩ ∘ γ
≡ ⟨ δ ∘ γ , transport (sym (⟦⟧-tr-comp δ γ A)) (a [ γ ]) ⟩ ≡ ⟨ δ ∘ γ , transport (sym (⟦⟧-tr-comp δ γ A)) (a [ γ ]) ⟩
``` ```