diff --git a/src/CwF/Structures.lagda.md b/src/CwF/Structures.lagda.md index 96cae3b..7957226 100644 --- a/src/CwF/Structures.lagda.md +++ b/src/CwF/Structures.lagda.md @@ -5,7 +5,7 @@ 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. (currently only pi types) First are pi types, because a type theory without them are pretty uninteresting. ```