From 3d3e890963c6d90d3586e063dd4beba343b1481c Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 2 Nov 2017 23:00:54 -0400 Subject: [PATCH] update lectures --- lectures/lecture1.ctt | 9 ++++++++- lectures/lecture2.ctt | 2 +- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/lectures/lecture1.ctt b/lectures/lecture1.ctt index 9366c86..5226af9 100644 --- a/lectures/lecture1.ctt +++ b/lectures/lecture1.ctt @@ -261,6 +261,13 @@ or : bool -> bool -> bool = split -- appear in the rest of the term (in particular one cannot refer to a -- variable called _). +-- Note also that the syntax is indentation sensitive (like in +-- Haskell), so the following does not parse: +-- +-- foo : bool = let output : bool = +-- true +-- in output + -- Sigma types are built-in and written as (x : A) * B: Sigma (A : U) (B : A -> U) : U = (x : A) * B x @@ -491,7 +498,7 @@ That's all for the first lecture. Next time we will look at: elimination principle for Path types. In particular how to prove transitivity of path types: - trans (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c = + compPath (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c = and that we can substitute Path equal elements: diff --git a/lectures/lecture2.ctt b/lectures/lecture2.ctt index 13e0570..73e4890 100644 --- a/lectures/lecture2.ctt +++ b/lectures/lecture2.ctt @@ -242,7 +242,7 @@ writing the comp after a path-abstraction). The direction j that we are doing the composition in is implicit, more about this below. -} -trans (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c = +compPath (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c = comp (<_> A) (p @ i) [ (i = 0) -> a , (i = 1) -> q ] -- 2.34.1