diff --git a/src/CwF/Structures.lagda.md b/src/CwF/Structures.lagda.md
index 4badb7f..995c9fe 100644
--- a/src/CwF/Structures.lagda.md
+++ b/src/CwF/Structures.lagda.md
@@ -5,9 +5,9 @@ open import CwF.Base
 module CwF.Structures where
 ```
 
-This file defines several additional structures a CwF might have, such as Pi types, universes, sigma types, and identity types.
+This file defines several additional structures a CwF might have, such as pi types, universes, sigma types, and identity types.
 
-First are Pi types, because a type theory without them are pretty uninteresting.
+First are pi types, because a type theory without them are pretty uninteresting.
 ```
 record has-Pi {o h f : _} {𝓒 : Precategory o h}
               (cwf : is-CwF {o} {h} {f} 𝓒) : Type (lsuc (o ⊔ h ⊔ f)) where
@@ -71,4 +71,4 @@ Lastly comes the star of the show, $\beta$ reduction.
     Cβ : {Γ : Ob} (A : ∣ Ty Γ ∣) (B : ∣ Ty (Γ ; A) ∣) (b : ∣ Tr (Γ ; A) B ∣)
          (a : ∣ Tr Γ A ∣)
        → app (Cλ A B b) a ≡ b [ ⟨id, a ⟩ ]
-```
\ No newline at end of file
+```