include "basics/logic.ma".
-inductive Sigma: Type[1] ≝
- mk_Sigma: ∀p1: Type[0]. p1 → Sigma.
+inductive Sigma: Type[2] ≝
+ mk_Sigma: ∀p1: Type[1]. p1 → Sigma.
-definition p1: Sigma → Type[0].
+definition p1: Sigma → Type[1].
#S cases S #Y #_ @Y
qed.
#S cases S #Y #x @x
qed.
-inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝
-jmrefl : jmeq A x A x.
+inductive jmeq (A:Type[1]) (x:A) : ∀B:Type[1]. B →Prop ≝
+refl_jmeq : jmeq A x A x.
+
+notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
+ non associative with precedence 45
+for @{ 'jmsimeq $t $a $u $b }.
+
+notation > "hvbox(n break ≃ m)"
+ non associative with precedence 45
+for @{ 'jmsimeq ? $n ? $m }.
+
+interpretation "john major's equality" 'jmsimeq t x u y = (jmeq t x u y).
+interpretation "john major's reflexivity" 'refl = refl_jmeq.
definition eqProp ≝ λA:Prop.eq A.
qed.
definition cast:
- ∀A,B:Type[0].∀E:A=B. A → B.
+ ∀A,B:Type[1].∀E:A=B. A → B.
#A #B #E cases E #X @X
qed.
lemma gral: ∀A.∀x,y:A.
mk_Sigma A x = mk_Sigma A y → x=y.
#A #x #y #E lapply (tech1 ?? E)
- generalize in ⊢ (??(???%?)? → ?) #E1
+ generalize in ⊢ (??(???%?)? → ?); #E1
normalize in E1; >(K ?? E1) normalize
#H @H
qed.
-axiom daemon: False.
-
lemma jm_to_eq_sigma:
∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
#A #x #y #E cases E in ⊢ (???%); %
qed.
lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
- PP ? (P x) (jmrefl A x) → ∀y.∀h:jmeq A x A y.PP ? (P y) h.
+ PP ? (P x) (refl_jmeq A x) → ∀y.∀h:jmeq A x A y.PP ? (P y) h.
#A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E)
lapply (G ?? (curry ?? P) ?? F)
[ normalize //
qed.
lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
- P x (jmrefl A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E.
+ P x (refl_jmeq A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E.
+
+lemma jmeq_to_eq: ∀A:Type[1]. ∀x,y:A. x≃y → x=y.
+ #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
+qed.
+
+coercion jmeq_to_eq: ∀A:Type[1]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
+
+lemma eq_to_jmeq:
+ ∀A: Type[1].
+ ∀x, y: A.
+ x = y → x ≃ y.
+ //
+qed.