matita/matita/lib/lambdaN/cube.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "convertibility.ma".
  16 include "types.ma".
  17
  18 (* PURE TYPE SYSTEMS OF THE λ-CUBE ********************************************)
  19
  20 inductive Cube_Ax: nat → nat → Prop ≝
  21   | star_box: Cube_Ax 0 1
  22 .
  23
  24 (* The λPω pure type system (a.k.a. λC or CC) *********************************)
  25
  26 inductive CC_Re: nat → nat → nat → Prop ≝
  27    | star_star: CC_Re 0 0 0
  28    | box_star : CC_Re 1 0 0
  29    | box_box  : CC_Re 1 1 1
  30    | star_box : CC_Re 0 1 1
  31 .
  32
  33 definition CC: pts ≝ mk_pts Cube_Ax CC_Re conv.
  34
  35 (* The λω pure type system (a.k.a. Fω) ****************************************)
  36
  37 inductive FO_Re: nat → nat → nat → Prop ≝
  38    | star_star: FO_Re 0 0 0
  39    | box_star : FO_Re 1 0 0
  40    | box_box  : FO_Re 1 1 1
  41 .
  42
  43 definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv.