diff --git a/src/CwF.lagda.md b/src/CwF.lagda.md
index db57a4b..f2ea340 100644
--- a/src/CwF.lagda.md
+++ b/src/CwF.lagda.md
@@ -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]
 
-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
@@ -172,4 +172,4 @@ Lastly, it is required that the weakening map behaves as expected under composit
            {a : ∣ Tr Δ (A ⟦ δ ⟧) ∣}
          → ⟨ δ , a ⟩ ∘ γ 
          ≡ ⟨ δ ∘ γ , transport (sym (⟦⟧-tr-comp δ γ A)) (a [ γ ]) ⟩
-```
\ No newline at end of file
+```