Fix newhedberg

diff --git a/examples/newhedberg.ctt b/examples/newhedberg.ctt
index 02e9bac7ca75e494233300314e7f4f2c26c4af60..ca180af4eb7ee08c27cee3295061be305acbed36 100644 (file)
--- a/examples/newhedberg.ctt
+++ b/examples/newhedberg.ctt
@@ -16,7 +16,7 @@ decConst (A : U) : dec A -> exConst A = split
 \r
 hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) :\r
             Square A a a (refl A a) a b p (f a (refl A a)) (f b p) = \r
- 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)))\r
+ 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)))\r
     (<i>(f a (refl A a)))\r
 \r
 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 =\r