1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "apps_2/MLTT1_1/syntax.ma".
17 (* PRIMITIVE GLOBAL CONSTANTS **********************************************)
19 (* symbolic names for referring the primitive global constants *)
21 definition empty ≝ 0. (* empty type *)
23 definition erec ≝ 1. (* empty eliminator *)
25 definition one ≝ 2. (* unit type *)
27 definition tt ≝ 3. (* unit constructor *)
29 definition orec ≝ 4. (* unit eliminator *)
31 definition nat ≝ 5. (* natural numbers type *)
33 definition zero ≝ 6. (* natural numbers constructor: zero *)
35 definition succ ≝ 7. (* natural numbers constructor: successor *)
37 definition nrec ≝ 8. (* natural numbers eliminator *)
39 definition ii ≝ 9. (* intensional identity type *)
41 definition refl ≝ 10. (* intensional identity constructor *)
43 definition irec ≝ 11. (* intensional identity eliminator *)
45 definition sum ≝ 12. (* disjoint sum type *)
47 definition sn ≝ 13. (* disjoint sum constructor: left *)
49 definition dx ≝ 14. (* disjoint sum constructor: right *)
51 definition srec ≝ 15. (* disjoint sum eliminator *)
53 definition prod ≝ 16. (* dependent product type *)
55 definition pair ≝ 17. (* dependent product constructor *)
57 definition prec ≝ 18. (* dependent product eliminator *)
59 definition fun ≝ 19. (* dependent function type *)
61 definition abst ≝ 20. (* dependent function constructor *)
63 definition ap ≝ 21. (* dependent function eliminator *)
65 definition univ ≝ 22. (* first universe type *)
67 definition ue ≝ 23. (* first universe constructor: empty *)
69 definition uo ≝ 24. (* first universe constructor: one *)
71 definition un ≝ 25. (* first universe constructor: nat *)
73 definition ui ≝ 26. (* first universe constructor: ii *)
75 definition us ≝ 27. (* first universe constructor: sum *)
77 definition up ≝ 28. (* first universe constructor: union *)
79 definition uf ≝ 29. (* first universe constructor: fun *)
81 definition urec ≝ 30. (* first universe eliminator *)
83 definition primitives ≝ 31. (* number of primitive constants *)
85 (* primitive global environment *)
93 Λ □ ⤏ □ ⤏ □ (* orec *)
97 Λ □ ⤏ □ ⤏ (□ ⤏ □ ⤏ □) ⤏ □ (* nrec *)
98 Λ □ ⤏ □ ⤏ □ ⤏ □ (* ii *)
100 Λ □ ⤏ (□ ⤏ □) ⤏ □ (* irec *)
101 Λ □ ⤏ □ ⤏ □ (* sum *)
104 Λ □ ⤏ (□ ⤏ □) ⤏ (□ ⤏ □) ⤏ □ (* srec *)
105 Λ □ ⤏ (□ ⤏ □) ⤏ □ (* prod *)
106 Λ □ ⤏ □ ⤏ □ (* pair *)
107 Λ □ ⤏ (□ ⤏ □ ⤏ □) ⤏ □ (* prec *)
108 Λ □ ⤏ (□ ⤏ □) ⤏ □ (* fun *)
109 Λ (□ ⤏ □) ⤏ □ (* abst *)
115 Λ □ ⤏ □ ⤏ □ ⤏ □ (* ui *)
117 Λ □ ⤏ (□ ⤏ □) ⤏ □ (* up *)
118 Λ □ ⤏ (□ ⤏ □) ⤏ □ (* uf *)
122 (* notation for applying the primitive constants *)
126 'Empty = (TAtom (GRef empty)).
129 "empty eliminator (MLTT)"
130 'ERec T = (TPair Appl T (TAtom (GRef erec))).
134 'One = (TAtom (GRef one)).
137 "unit constructor (MLTT)"
138 'TT = (TAtom (GRef tt)).
141 "unit eliminator (MLTT)"
142 'SRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef srec)))).
145 "natural numbers type (MLTT)"
146 'Nat = (TAtom (GRef nat)).
149 "natural numbers constructor: zero (MLTT)"
150 'Zero = (TAtom (GRef zero)).
153 "natural numbers constructor: successor (MLTT)"
154 'Succ T = (TPair Appl T (TAtom (GRef succ))).
157 "natural numbers eliminator (MLTT)"
158 'NRec T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef nrec))))).
161 "intensional identity type (MLTT)"
162 'II T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ii))))).
165 "intensional identity constructor (MLTT)"
166 'Refl T = (TPair Appl T (TAtom (GRef refl))).
169 "intensional identity eliminator (MLTT)"
170 'IRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef irec)))).
174 'Sum T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef sum)))).
177 "sum constructorL left (MLTT)"
178 'Sn T = (TPair Appl T (TAtom (GRef sn))).
181 "sum constructor: right (MLTT)"
182 'Dx T = (TPair Appl T (TAtom (GRef dx))).
185 "sum eliminator (MLTT)"
186 'SRec T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef srec))))).
189 "product type (MLTT)"
190 'Prod T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef prod)))).
193 "product constructor (MLTT)"
194 'Pair T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef pair)))).
197 "product eliminator (MLTT)"
198 'PRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef prec)))).
201 "function type (MLTT)"
202 'Fun T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef fun)))).
205 "function constructor (MLTT)"
206 'Abst T = (TPair Appl T (TAtom (GRef abst))).
209 "function eliminator (MLTT)"
210 'AP T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ap)))).
213 "first universe type (MLTT)"
214 'Univ = (TAtom (GRef univ)).
217 "first universe constructor: empty (MLTT)"
218 'UE = (TAtom (GRef ue)).
221 "first universe constructor: one (MLTT)"
222 'UO = (TAtom (GRef us)).
225 "first universe constructor: nat (MLTT)"
226 'UN = (TAtom (GRef un)).
229 "first universe constructor: ii (MLTT)"
230 'UI T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ui))))).
233 "first universe constructor: sum (MLTT)"
234 'US T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef us)))).
237 "first universe constructor: product (MLTT)"
238 'UP T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef up)))).
241 "first universe constructor: function (MLTT)"
242 'UF T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef uf)))).
245 "first universe eliminator (MLTT)"
246 'URec T = (TPair Appl T (TAtom (GRef urec))).