From 3e5c05962656cde29eb0c55e1ebe76ad868e9550 Mon Sep 17 00:00:00 2001 From: Anders Date: Mon, 13 Apr 2015 17:01:13 +0200 Subject: [PATCH] Update README --- README.md | 2 +- examples/helix.ctt | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/README.md b/README.md index 0f15562..5e49a55 100644 --- a/README.md +++ b/README.md @@ -60,7 +60,7 @@ References and notes typing rules of the system * [Lecture Notes on Cubical - sets](http://www.cse.chalmers.se/~coquand/course1.pdf) + sets](http://www.cse.chalmers.se/~coquand/course3.pdf) * Voevodsky's page on [univalent foundations](http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html) diff --git a/examples/helix.ctt b/examples/helix.ctt index df89a0b..c6ee49e 100644 --- a/examples/helix.ctt +++ b/examples/helix.ctt @@ -1,7 +1,6 @@ module helix where import circle -import hedberg import retract encode (x:S1) (p:Id S1 base x) : helix x = subst S1 helix base x p zeroZ -- 2.34.1