From 8d082302f9e36b3406bcbfadfabf242a80c526a4 Mon Sep 17 00:00:00 2001 From: depsterr Date: Fri, 28 Oct 2022 16:23:22 +0200 Subject: [PATCH] change text to better reflect current state --- src/CwF/Structures.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. ```