From e3d7ac5bbd76cf90d4dde53bc02c41a43cf54732 Mon Sep 17 00:00:00 2001 From: Anders Date: Mon, 8 Jun 2015 14:26:44 +0200 Subject: [PATCH] Add lemSimpl --- examples/prelude.ctt | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/examples/prelude.ctt b/examples/prelude.ctt index ecaebd5..986081c 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -79,12 +79,20 @@ kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c) (r : Id A b d) : Id A c d = comp (<_>A) (p @ i) [ (i = 0) -> q, (i = 1) -> r ] --- lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) --- (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' = --- comp A a [ (j = 0) -> comp A (p @ i) [ (i=1) -> q @ k /\ l], --- (j = 1) -> comp A (p @ i) [ (i=1) -> q' @ k /\ l], --- (k = 0) -> p, --- (k = 1) -> s @ j ] +lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) + (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : + Id (Id A b c) q q' = + comp (<_> A) a + [ (j = 0) -> comp (<_> A) (p @ i) + [ (k = 0) -> p @ i + , (i = 0) -> a + , (i = 1) -> q @ k /\ l] + , (j = 1) -> comp (<_> A) (p @ i) + [ (k = 0) -> p @ i + , (i = 0) -> a + , (i = 1) -> q' @ k /\ l] + , (k = 0) -> p + , (k = 1) -> s @ j ] idfun (A : U) (a : A) : A = a @@ -211,7 +219,7 @@ decConst (A : U) : dec A -> exConst A = split inl a -> (\ (x:A) -> a, \ (x y:A) -> refl A a) inr h -> (\ (x:A) -> x, \ (x y:A) -> efq (Id A x y) (h x)) -stableConst (A : U) (sA: stable A) : exConst A = +stableConst (A : U) (sA: stable A) : exConst A = (\ (x:A) -> sA (dNeg A x),\ (x y:A) -> sA (propNeg (neg A) (dNeg A x) (dNeg A y) @ i)) discrete (A : U) : U = (a b : A) -> dec (Id A a b) -- 2.34.1