From 4066ab922bb8e69238f39b676417779d23651402 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Sat, 6 Jun 2015 11:23:12 +0200 Subject: [PATCH] Update aim.ctt again --- examples/aim.ctt | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/examples/aim.ctt b/examples/aim.ctt index 889092c..babd5cc 100644 --- a/examples/aim.ctt +++ b/examples/aim.ctt @@ -116,7 +116,7 @@ funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) (p : (x : A) -> Id (B x) (f x) (g x)) : Id ((y : A) -> B y) f g = \(a : A) -> (p a) @ i -{- +{- To see that the definition of funExt makes sense we can compute its faces: @@ -637,14 +637,14 @@ intSet : set int = subst U set Z int isoIntZ ZSet -------------------------------------------------------------------------- o Definitional equality for J? Problem pointed out by Dan Licata - with regularity for composition in the universe. However the - system seems to work without regularity (this is work in - progress). + with regularity for composition in the universe. However, the + system might still work without regularity (this is what is being + implemented in the no_regular branch). o Meta-theoretical properties of the system and correctness of the model. Formalization? - o Integration of ideas into other proof assistants (eg Agda)? + o Integration of ideas into other proof assistants (e.g. Agda)? -} @@ -658,6 +658,7 @@ addZero : (a : nat) -> Id nat (add zero a) a = split addCom (a : nat) : (b : nat) -> Id nat (add a b) (add b a) = split zero -> addZero a @ -i - suc b' -> comp nat (suc (addCom a b' @ i)) [ (i = 0) -> suc (add a b') - , (i = 1) -> addSuc b' a @ -j ] + suc b' -> comp (<_> nat) (suc (addCom a b' @ i)) [ (i = 0) -> suc (add a b') + , (i = 1) -> addSuc b' a @ -j ] + -} -- 2.34.1