From c6579b4b2c8462a83ed44bbabe4cbf5e1f647787 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Sat, 22 Oct 2016 12:03:11 -0400 Subject: [PATCH] update demo --- examples/demo.ctt | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/examples/demo.ctt b/examples/demo.ctt index 966da19..f91fe0f 100644 --- a/examples/demo.ctt +++ b/examples/demo.ctt @@ -18,7 +18,7 @@ Makoto Takeya. Mini-TT is a variant Martin-Löf type theory with data types. cubiclaltt extends Mini-TT with: - o Name abstraction and application + o Path types o Compositions o Equivalences can be transformed into equalities o Some higher inductive types @@ -45,21 +45,21 @@ not : bool -> bool = split {- - Identity types, names and formulas + Path types, names and formulas -------------------------------------------------------------------------- -An element in ID A B is a line in the universe connecting A and B: +An element in PATH A B is a line in the universe connecting A and B: |- A Type |- B Type ------------------------------ - |- ID A B Type + |- PATH A B Type PathP is heterogeneous equality: - |- P : ID A B |- a : A |- b : B + |- P : PATH A B |- a : A |- b : B ----------------------------------------------- |- PathP P a b Type -- 2.34.1