From d8904bfbd60613298b316f59f32a18e4666f39c3 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Tue, 21 Apr 2015 09:45:24 +0200 Subject: [PATCH] Fix newhedberg --- examples/newhedberg.ctt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 (Square A a a (refl A a) a p@i (p@i/\j) (f a (refl A a)) (f p@i (p@i/\j))) + transport (Square A a a (refl A a) a (p@i) (p@i/\j) (f a (refl A a)) (f (p@i) (p@i/\j))) ((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 = -- 2.34.1