2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/logic.ma".
14 inductive Sigma: Type[1] ≝
15 mk_Sigma: ∀p1: Type[0]. p1 → Sigma.
17 definition p1: Sigma → Type[0].
21 definition p2: ∀S:Sigma. p1 S.
25 inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝
26 jmrefl : jmeq A x A x.
28 definition eqProp ≝ λA:Prop.eq A.
30 lemma K : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
31 #A #x #h @(refl ? h: eqProp ? ? ?).
35 ∀A,B:Type[0].∀E:A=B. A → B.
36 #A #B #E cases E #X @X
40 ∀Aa,Bb:Sigma.∀E:Aa=Bb.
41 cast (p1 Aa) (p1 Bb) ? (p2 Aa) = p2 Bb.
43 | #Aa #Bb #E >E cases Bb #B #b normalize % ]
46 lemma gral: ∀A.∀x,y:A.
47 mk_Sigma A x = mk_Sigma A y → x=y.
48 #A #x #y #E lapply (tech1 ?? E)
49 generalize in ⊢ (??(???%?)? → ?) #E1
50 normalize in E1; >(K ?? E1) normalize
55 ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
56 #A #x #y #E cases E in ⊢ (???%); %
61 (∀y. jmeq A x A y → Type[0]) →
62 (∀y. mk_Sigma A x = mk_Sigma A y → Type[0]).
63 #A #x #f #y #E @(f y) >(gral ??? E) %
66 lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0].
67 P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y.
69 #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E;
71 return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e
74 #E <(sym_eq ??? (K ?? E)) @H
77 definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0].
81 lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
82 PP ? (P x) (jmrefl A x) → ∀y.∀h:jmeq A x A y.PP ? (P y) h.
83 #A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E)
84 lapply (G ?? (curry ?? P) ?? F)
86 | #H whd in H; @(H : PP ? (P b) ?) ]
89 lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
90 P x (jmrefl A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E.