From: Simon Huber Date: Wed, 3 Jun 2015 14:06:03 +0000 (+0200) Subject: Adapted prelude X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=aa4323460955611ed3a93f690fd51e2ec1adc176;p=cubicaltt.git Adapted prelude --- diff --git a/examples/prelude.ctt b/examples/prelude.ctt index f359fea..9251182 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -19,8 +19,8 @@ funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) 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 +-- 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 substInv (A : U) (P : A -> U) (a b : A) (p : Id A a b) : P b -> P a = subst A P b a ( p @ -i) @@ -35,13 +35,13 @@ 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 +-- 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 inv (A : U) (a b : A) (p : Id A a b) : Id A b a = p @ -i compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = - comp A (p @ i) [ (i = 1) -> q ] + comp A (p @ i) [ (i = 1) -> q, (i=0) -> <_> a ] compId' (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = subst A (Id A a) b c q p @@ -58,28 +58,28 @@ compDown (A : U) (a a' b b' : A) (p : Id A a a') (q: Id A b b') : Id A a' b' -> Id A a b = compUp A a' a b' b (inv A a a' p) (inv A b b' q) -lemCompInv (A:U) (a b c:A) (p:Id A a b) (q:Id A b c) : Id (Id A a b) (compId A a c b (compId A a b c p q) (inv A b c q)) p = - comp A (comp A (p @ i) [(i=1) -> q @ (-j /\ k)]) [(i=1) -> q @ (-j /\ - k)] +-- lemCompInv (A:U) (a b c:A) (p:Id A a b) (q:Id A b c) : Id (Id A a b) (compId A a c b (compId A a b c p q) (inv A b c q)) p = +-- comp A (comp A (p @ i) [(i=1) -> q @ (-j /\ k)]) [(i=1) -> q @ (-j /\ - k)] -lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p) (refl A b) = - comp A (p @ (-i \/ j)) [(i=1) -> p @ (j \/ k)] +-- lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p) (refl A b) = +-- comp A (p @ (-i \/ j)) [(i=1) -> p @ (j \/ k)] test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0) test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1) -compEmpty (A : U) (a b : A) (p : Id A a b) : Id A a b = - comp A (p @ i) [ ] +-- compEmpty (A : U) (a b : A) (p : Id A a b) : Id A a b = +-- comp A (p @ i) [ ] 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) [ (i=1) -> q @ k /\ l], +-- (j = 1) -> comp A (p @ i) [ (i=1) -> q' @ k /\ l], +-- (k = 0) -> p, +-- (k = 1) -> s @ j ] isoId (A B : U) (f : A -> B) (g : B -> A) (s : (y:B) -> Id B (f (g y)) y) @@ -88,9 +88,9 @@ isoId (A B : U) (f : A -> B) (g : B -> A) idfun (A : U) (a : A) : A = a -isoIdRef (A : U) : - Id (Id U A A) (refl U A) (isoId A A (idfun A) (idfun A) (refl A) (refl A)) = - glueLine j i A +-- isoIdRef (A : U) : +-- Id (Id U A A) (refl U A) (isoId A A (idfun A) (idfun A) (refl A) (refl A)) = +-- glueLine j i A -- u -- a0 -----> a1 @@ -136,10 +136,10 @@ propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x)) IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : U = IdP ( P (p @ i)) u0 u1 -lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 : A) - (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdS A P a0 a1 p b0 b1 = - (pP (p @ i) (transport ( P (p @ i /\ j)) b0) - (transport ( P (p @ i \/ -j)) b1)) @ i +-- lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 : A) +-- (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdS A P a0 a1 p b0 b1 = +-- (pP (p @ i) (transport ( P (p @ i /\ j)) b0) +-- (transport ( P (p @ i \/ -j)) b1)) @ i -- Basic data types