From: Simon Huber <hubsim@gmail.com>
Date: Wed, 24 Jun 2015 09:50:42 +0000 (+0200)
Subject: Equations for subst and J
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f155a8cad6d1f290b72088348853029df6c283ac;p=cubicaltt.git

Equations for subst and J
---

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index ef39041..f161fb8 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -25,8 +25,9 @@ substTrans (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
 subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
   transport (mapOnPath A U P a b p) e
 
--- substRefl (A : U) (P : A -> U) (a : A) (e : P a) :
---   Id (P a) (subst A P a a (refl A a) e) e = refl (P a) e
+substEq (A : U) (P : A -> U) (a : A) (e : P a)
+  : Id (P a) e (subst A P a a (refl A a) e) =
+  fill (<_> P a) e []
 
 substInv (A : U) (P : A -> U) (a b : A) (p : Id A a b) : P b -> P a =
  subst A P b a (<i> p @ -i)
@@ -41,8 +42,11 @@ J (A : U) (a : A) (C : (x : A) -> Id 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)
 
--- defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) :
---        Id (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d
+JEq (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a))
+  : Id (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
+    where T (z : singl A a) : U = C (z.1) (z.2)
+
 
 inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
 
@@ -144,7 +148,9 @@ propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x))
 
 lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a :A) : 
           (a1 : A) (p : Id A a a1) (b0 : P a) (b1 : P a1) -> IdP (<i>P (p@i)) b0 b1 =
- J A a (\ (a1 : A) (p : Id A a a1) -> (b0 : P a) (b1 : P a1) -> IdP (<i>P (p@i)) b0 b1) rem
+ J A a (\ (a1 : A) (p : Id A a a1) ->
+          (b0 : P a) (b1 : P a1) -> IdP (<i>P (p@i)) b0 b1)
+   rem
  where rem : (b0 b1:P a) -> Id (P a) b0 b1 = pP a
 
 lemSig (A : U) (B : A -> U) (pB : (x : A) -> prop (B x))