From: Anders <mortberg@chalmers.se>
Date: Mon, 8 Jun 2015 12:26:44 +0000 (+0200)
Subject: Add lemSimpl
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=e3d7ac5bbd76cf90d4dde53bc02c41a43cf54732;p=cubicaltt.git

Add lemSimpl
---

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 =
   <i> 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' =
---   <j> <k> comp A a [ (j = 0) -> <i> comp A (p @ i) [ (i=1) -> <l> q @ k /\ l],
---                      (j = 1) -> <i> comp A (p @ i) [ (i=1) -> <l> 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' =
+   <j k> comp (<_> A) a
+           [ (j = 0) -> <i> comp (<_> A) (p @ i)
+                              [ (k = 0) -> <l> p @ i
+                              , (i = 0) -> <l> a
+                              , (i = 1) -> <l> q @ k /\ l]
+           , (j = 1) -> <i> comp (<_> A) (p @ i)
+                              [ (k = 0) -> <l> p @ i
+                              , (i = 0) -> <l> a
+                              , (i = 1) -> <l> 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) -> <i>sA (propNeg (neg A) (dNeg A x) (dNeg A y) @ i))
 
 discrete (A : U) : U = (a b : A) -> dec (Id A a b)