From 7f3c7a7cfe60f98da46e6958bec62bac4675ccd2 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 22 Feb 2018 23:51:53 -0500 Subject: [PATCH] add an alternative proof of J --- examples/prelude.ctt | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 6465191..408dbf3 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -66,6 +66,19 @@ J (A : U) (a : A) (C : (x : A) -> Path A a x -> U) subst (singl A a) T (a, refl A a) (x, p) (contrSingl A a x p) d where T (z : singl A a) : U = C (z.1) (z.2) +-- Normal form of J: +-- comp ( C (p @ i) ( p @ i /\ j)) d [] + +-- Alternative proof of J +J' (A : U) (a : A) (C : (x : A) -> Path A a x -> U) + (d : C a (<_> a)) (x : A) (p : Path A a x) : C x p = + transport ( C (comp (<_> A) a [(i=0) -> <_> a,(i=1) -> p]) + (fill (<_> A) a [(i=0) -> <_> a,(i=1) -> p])) d + +-- Normal form of J': +-- comp ( C (comp (<_> A) a [ (i=0) -> <_> a, (i=1) -> p ]) +-- ( comp (<_> A) a [ (i=0) -> <_> a, (i=1) -> p @ j /\ k, (j=0) -> <_> a ])) d [] + JEq (A : U) (a : A) (C : (x : A) -> Path A a x -> U) (d : C a (refl A a)) : Path (C a (refl A a)) d (J A a C d a (refl A a)) = substEq (singl A a) T (a, refl A a) d @@ -74,7 +87,7 @@ JEq (A : U) (a : A) (C : (x : A) -> Path A a x -> U) (d : C a (refl A a)) inv (A : U) (a b : A) (p : Path A a b) : Path A b a = p @ -i 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 = 1) -> q, (i=0) -> a ] + comp (A) (p @ i) [ (i=0) -> a, (i=1) -> q ] compPath' (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c = subst A (Path A a) b c q p -- 2.34.1