source: Deliverables/D3.1/C-semantics/oldlib/eq.ma @ 535

Last change on this file since 535 was 488, checked in by campbell, 9 years ago

Some missing equality constants used by destruct.

File size: 2.9 KB
Line 
1include "basics/logic.ma".
2
3axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2]. P (refl ? t) → ∀p.P p.
4
5definition R2 :
6  ∀T0:Type[0].
7  ∀a0:T0.
8  ∀T1:∀x0:T0. a0=x0 → Type[0].
9  ∀a1:T1 a0 (refl ? a0).
10  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
11  ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
12  ∀b0:T0.
13  ∀e0:a0 = b0.
14  ∀b1: T1 b0 e0.
15  ∀e1:R1 ?? T1 a1 ? e0 = b1.
16  T2 b0 e0 b1 e1.
17#T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
18@(eq_rect_Type0 ????? e1);
19@(R1 ?? ? ?? e0);
20@a2;
21qed.
22
23
24definition R3 :
25  ∀T0:Type[0].
26  ∀a0:T0.
27  ∀T1:∀x0:T0. a0=x0 → Type[0].
28  ∀a1:T1 a0 (refl ? a0).
29  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
30  ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
31  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
32      ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
33  ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
34  ∀b0:T0.
35  ∀e0:a0 = b0.
36  ∀b1: T1 b0 e0.
37  ∀e1:R1 ?? T1 a1 ? e0 = b1.
38  ∀b2: T2 b0 e0 b1 e1.
39  ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
40  T3 b0 e0 b1 e1 b2 e2.
41#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
42@(eq_rect_Type0 ????? e2);
43@(R2 ?? ? ???? e0 ? e1);
44@a3;
45qed.
46
47definition R4 :
48  ∀T0:Type[0].
49  ∀a0:T0.
50  ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
51  ∀a1:T1 a0 (refl T0 a0).
52  ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
53  ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
54  ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
55      ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
56  ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
57      a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
58  ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
59      ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
60      ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
61      Type[0].
62  ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
63      a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
64      a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
65                   a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
66                   a3).
67  ∀b0:T0.
68  ∀e0:eq (T0 …) a0 b0.
69  ∀b1: T1 b0 e0.
70  ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
71  ∀b2: T2 b0 e0 b1 e1.
72  ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
73  ∀b3: T3 b0 e0 b1 e1 b2 e2.
74  ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
75  T4 b0 e0 b1 e1 b2 e2 b3 e3.
76#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
77@ (eq_rect_Type0 ????? e3);
78@ (R3 ????????? e0 ? e1 ? e2);
79@ a4;
80qed.
81
Note: See TracBrowser for help on using the repository browser.