+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "apps_2/MLTT1_1/syntax.ma".
+
+(* PRIMITIVE GLOBAL CONSTANTS **********************************************)
+
+(* symbolic names for referring the primitive global constants *)
+
+definition empty ≝ 0. (* empty type *)
+
+definition erec ≝ 1. (* empty eliminator *)
+
+definition one ≝ 2. (* unit type *)
+
+definition tt ≝ 3. (* unit constructor *)
+
+definition orec ≝ 4. (* unit eliminator *)
+
+definition nat ≝ 5. (* natural numbers type *)
+
+definition zero ≝ 6. (* natural numbers constructor: zero *)
+
+definition succ ≝ 7. (* natural numbers constructor: successor *)
+
+definition nrec ≝ 8. (* natural numbers eliminator *)
+
+definition ii ≝ 9. (* intensional identity type *)
+
+definition refl ≝ 10. (* intensional identity constructor *)
+
+definition irec ≝ 11. (* intensional identity eliminator *)
+
+definition sum ≝ 12. (* disjoint sum type *)
+
+definition sn ≝ 13. (* disjoint sum constructor: left *)
+
+definition dx ≝ 14. (* disjoint sum constructor: right *)
+
+definition srec ≝ 15. (* disjoint sum eliminator *)
+
+definition prod ≝ 16. (* dependent product type *)
+
+definition pair ≝ 17. (* dependent product constructor *)
+
+definition prec ≝ 18. (* dependent product eliminator *)
+
+definition fun ≝ 19. (* dependent function type *)
+
+definition abst ≝ 20. (* dependent function constructor *)
+
+definition ap ≝ 21. (* dependent function eliminator *)
+
+definition univ ≝ 22. (* first universe type *)
+
+definition ue ≝ 23. (* first universe constructor: empty *)
+
+definition uo ≝ 24. (* first universe constructor: one *)
+
+definition un ≝ 25. (* first universe constructor: nat *)
+
+definition ui ≝ 26. (* first universe constructor: ii *)
+
+definition us ≝ 27. (* first universe constructor: sum *)
+
+definition up ≝ 28. (* first universe constructor: union *)
+
+definition uf ≝ 29. (* first universe constructor: fun *)
+
+definition urec ≝ 30. (* first universe eliminator *)
+
+definition primitives ≝ 31. (* number of primitive constants *)
+
+(* primitive global environment *)
+
+definition Gp: lenv ≝
+ ⋆
+ Λ □ (* empty *)
+ Λ □ ⤏ □ (* erec *)
+ Λ □ (* one *)
+ Λ □ (* tt *)
+ Λ □ ⤏ □ ⤏ □ (* orec *)
+ Λ □ (* nat *)
+ Λ □ (* zero *)
+ Λ □ ⤏ □ (* succ *)
+ Λ □ ⤏ □ ⤏ (□ ⤏ □ ⤏ □) ⤏ □ (* nrec *)
+ Λ □ ⤏ □ ⤏ □ ⤏ □ (* ii *)
+ Λ □ ⤏ □ (* refl *)
+ Λ □ ⤏ (□ ⤏ □) ⤏ □ (* irec *)
+ Λ □ ⤏ □ ⤏ □ (* sum *)
+ Λ □ ⤏ □ (* sn *)
+ Λ □ ⤏ □ (* dx *)
+ Λ □ ⤏ (□ ⤏ □) ⤏ (□ ⤏ □) ⤏ □ (* srec *)
+ Λ □ ⤏ (□ ⤏ □) ⤏ □ (* prod *)
+ Λ □ ⤏ □ ⤏ □ (* pair *)
+ Λ □ ⤏ (□ ⤏ □ ⤏ □) ⤏ □ (* prec *)
+ Λ □ ⤏ (□ ⤏ □) ⤏ □ (* fun *)
+ Λ (□ ⤏ □) ⤏ □ (* abst *)
+ Λ □ ⤏ □ ⤏ □ (* ap *)
+ Λ □ (* univ *)
+ Λ □ (* ue *)
+ Λ □ (* uo *)
+ Λ □ (* un *)
+ Λ □ ⤏ □ ⤏ □ ⤏ □ (* ui *)
+ Λ □ ⤏ □ ⤏ □ (* us *)
+ Λ □ ⤏ (□ ⤏ □) ⤏ □ (* up *)
+ Λ □ ⤏ (□ ⤏ □) ⤏ □ (* uf *)
+ Λ □ ⤏ □ (* urec *)
+.
+
+(* notation for applying the primitive constants *)
+
+interpretation
+ "empty type (MLTT)"
+ 'Empty = (TAtom (GRef empty)).
+
+interpretation
+ "empty eliminator (MLTT)"
+ 'ERec T = (TPair Appl T (TAtom (GRef erec))).
+
+interpretation
+ "unit type (MLTT)"
+ 'One = (TAtom (GRef one)).
+
+interpretation
+ "unit constructor (MLTT)"
+ 'TT = (TAtom (GRef tt)).
+
+interpretation
+ "unit eliminator (MLTT)"
+ 'SRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef srec)))).
+
+interpretation
+ "natural numbers type (MLTT)"
+ 'Nat = (TAtom (GRef nat)).
+
+interpretation
+ "natural numbers constructor: zero (MLTT)"
+ 'Zero = (TAtom (GRef zero)).
+
+interpretation
+ "natural numbers constructor: successor (MLTT)"
+ 'Succ T = (TPair Appl T (TAtom (GRef succ))).
+
+interpretation
+ "natural numbers eliminator (MLTT)"
+ 'NRec T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef nrec))))).
+
+interpretation
+ "intensional identity type (MLTT)"
+ 'II T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ii))))).
+
+interpretation
+ "intensional identity constructor (MLTT)"
+ 'Refl T = (TPair Appl T (TAtom (GRef refl))).
+
+interpretation
+ "intensional identity eliminator (MLTT)"
+ 'IRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef irec)))).
+
+interpretation
+ "sum type (MLTT)"
+ 'Sum T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef sum)))).
+
+interpretation
+ "sum constructorL left (MLTT)"
+ 'Sn T = (TPair Appl T (TAtom (GRef sn))).
+
+interpretation
+ "sum constructor: right (MLTT)"
+ 'Dx T = (TPair Appl T (TAtom (GRef dx))).
+
+interpretation
+ "sum eliminator (MLTT)"
+ 'SRec T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef srec))))).
+
+interpretation
+ "product type (MLTT)"
+ 'Prod T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef prod)))).
+
+interpretation
+ "product constructor (MLTT)"
+ 'Pair T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef pair)))).
+
+interpretation
+ "product eliminator (MLTT)"
+ 'PRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef prec)))).
+
+interpretation
+ "function type (MLTT)"
+ 'Fun T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef fun)))).
+
+interpretation
+ "function constructor (MLTT)"
+ 'Abst T = (TPair Appl T (TAtom (GRef abst))).
+
+interpretation
+ "function eliminator (MLTT)"
+ 'AP T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ap)))).
+
+interpretation
+ "first universe type (MLTT)"
+ 'Univ = (TAtom (GRef univ)).
+
+interpretation
+ "first universe constructor: empty (MLTT)"
+ 'UE = (TAtom (GRef ue)).
+
+interpretation
+ "first universe constructor: one (MLTT)"
+ 'UO = (TAtom (GRef us)).
+
+interpretation
+ "first universe constructor: nat (MLTT)"
+ 'UN = (TAtom (GRef un)).
+
+interpretation
+ "first universe constructor: ii (MLTT)"
+ 'UI T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ui))))).
+
+interpretation
+ "first universe constructor: sum (MLTT)"
+ 'US T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef us)))).
+
+interpretation
+ "first universe constructor: product (MLTT)"
+ 'UP T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef up)))).
+
+interpretation
+ "first universe constructor: function (MLTT)"
+ 'UF T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef uf)))).
+
+interpretation
+ "first universe eliminator (MLTT)"
+ 'URec T = (TPair Appl T (TAtom (GRef urec))).