From: Anders Mörtberg <mortberg@chalmers.se>
Date: Tue, 21 Apr 2015 07:45:24 +0000 (+0200)
Subject: Fix newhedberg
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d8904bfbd60613298b316f59f32a18e4666f39c3;p=cubicaltt.git

Fix newhedberg
---

diff --git a/examples/newhedberg.ctt b/examples/newhedberg.ctt
index 02e9bac..ca180af 100644
--- a/examples/newhedberg.ctt
+++ b/examples/newhedberg.ctt
@@ -16,7 +16,7 @@ decConst (A : U) : dec A -> exConst A = split
 
 hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) :
             Square A a a (refl A a) a b p (f a (refl A a)) (f b p) = 
- transport (<i>Square A a a (refl A a) a p@i (<j>p@i/\j) (f a (refl A a)) (f p@i (<j>p@i/\j)))
+ transport (<i>Square A a a (refl A a) a (p@i) (<j>p@i/\j) (f a (refl A a)) (f (p@i) (<j>p@i/\j)))
     (<i>(f a (refl A a)))
 
 hedberg (A:U) (a b:A) (h: (x:A) -> dec (Id A a x)) (p q : Id A a b) : Id (Id A a b) p q =