From 0df2b3c7885028dd58623e2c9dd792629eab1894 Mon Sep 17 00:00:00 2001 From: Thierry Coquand Date: Fri, 8 Apr 2016 09:09:00 +0200 Subject: [PATCH] other proof of lemPropF --- examples/prelude.ctt | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 8b1bf39..75f2bce 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -162,12 +162,17 @@ propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x)) (f0 f1 : (x : A) -> B x) : Id ((x : A) -> B x) f0 f1 = \ (x:A) -> (h x (f0 x) (f1 x)) @ i -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 (P (p@i)) b0 b1 = - J A a (\ (a1 : A) (p : Id A a a1) -> - (b0 : P a) (b1 : P a1) -> IdP (P (p@i)) b0 b1) - rem - where rem : (b0 b1:P a) -> Id (P a) b0 b1 = pP a +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) : IdP (P (p@i)) b0 b1 = + pP (p@i) (comp (P (p@i/\j)) b0 [(i=0) -> <_>b0]) (comp (P (p@i\/-j)) b1 [(i=1) -> <_>b1])@i + +-- other proof +-- 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 (P (p@i)) b0 b1 = +-- J A a (\ (a1 : A) (p : Id A a a1) -> +-- (b0 : P a) (b1 : P a1) -> IdP (P (p@i)) b0 b1) +-- rem +-- where rem : (b0 b1:P a) -> Id (P a) b0 b1 = pP a Sigma (A : U) (B : A -> U) : U = (x : A) * B x -- 2.34.1