From: Anders Mörtberg Date: Thu, 11 May 2017 16:55:32 +0000 (+0200) Subject: lecture1 X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=519aaa4fb220669eb8aed9d66378a3e9b4985ab1;p=cubicaltt.git lecture1 --- diff --git a/lectures/lecture1.ctt b/lectures/lecture1.ctt index 4bb1162..9e16c9d 100644 --- a/lectures/lecture1.ctt +++ b/lectures/lecture1.ctt @@ -141,7 +141,8 @@ model: to nominal sets with 01 substitutions: "An Equivalent Presentation of the Bezem-Coquand-Huber Category of - Cubical Sets" by Andrew Pitts. + Cubical Sets" + Andrew Pitts https://arxiv.org/abs/1401.7807 Before implementing cubicaltt (so in 2013-2014) we implemented a @@ -198,6 +199,9 @@ idfun : (A : U) (a : A) -> A = -- Or even better like this: idfun (A : U) (a : A) : A = a +-- The syntax for Pi types is like in Agda, so (x : A) -> B +-- corresponds to Pi (x : A). B or forall (x : A), B. + -- Note that the second idfun shadows the first, so when one uses -- idfun later this will refer to the last defined one. -- TODO: This is a little dangerous if one have a long development and @@ -422,8 +426,8 @@ congbin (A B C : U) (f : A -> B -> C) (a a' : A) (b b' : B) -- type. We could have a version of undefined which is annotated with -- the type (similar to what we have for split), but this hasn't been -- implemented yet. Note that it is often useful to define a local --- undefined definition using let-in or where and keep the body --- undefined when trying to prove complicated things. +-- definition using let-in or where and keep the body of it undefined +-- when trying to prove complicated things. -- We get a short proof of function extensionality using Path types: funExt (A B : U) (f g : A -> B) @@ -457,6 +461,9 @@ funExt2 (A B C : U) (f g : A -> B -> C) compf (f g : bool -> bool) : bool -> bool = \(b : bool) -> g (f b) +-- WARNING: we couldn't have called the above function comp as comp is +-- a reserved keyword. + notK' : Path (bool -> bool) (compf not not) (idfun bool) = \(b : bool) -> notK b @ i