Library Ftypesystem

Require Import Omega.
Require Import List.

Require Import mxx.
Require Import Flanguage.
Require Export typesystem.

Inductive Ftypesystem_v := .

Links: Index_v Table of contents Main page

System Fcc (indexed version)

We write jterm H G a t the indexed term judgment. It is exactly like the lambda term judgment in Ltypesystem_v with index annotations.
Inductive jterm v : tenvaenvtermtypeProp :=
| JVar : H G k x t,
  cobj G CAEnv
  (mS vjobj v H (JT t KStar)) →
  Gnth G x t
  jterm v H G (Var k x) t
| JLam : H G k a t s,
  (mS vjobj v H (JT s KStar)) →
  jobj v H (JT t KStar) →
  jterm v H (GCons G t) a s
  jterm v H G (Lam k a) (TArr t s)
| JApp : H G k a b t s,
  (mS vjobj v H (JT t KStar)) →
  (mS vjobj v H (JT s KStar)) →
  jterm v H G a (TArr t s) →
  jterm v H G b t
  jterm v H G (App k a b) s
| JUnit : H G k,
  cobj H CTEnv
  cobj G CAEnv
  jterm v H G (Unit k) TOne
| JPair : H G k a b t s,
  (mS vjobj v H (JT t KStar)) →
  (mS vjobj v H (JT s KStar)) →
  jterm v H G a t
  jterm v H G b s
  jterm v H G (Pair k a b) (TProd t s)
| JFst : H G k a t s,
  (mS vjobj v H (JT t KStar)) →
  (mS vjobj v H (JT s KStar)) →
  jterm v H G a (TProd t s) →
  jterm v H G (Fst k a) t
| JSnd : H G k a t s,
  (mS vjobj v H (JT t KStar)) →
  (mS vjobj v H (JT s KStar)) →
  jterm v H G a (TProd t s) →
  jterm v H G (Snd k a) s
| JAbsurd : H G k a s,
  jterm v H G a TVoid
  jobj v H (JT s KStar) →
  jterm v H G (Absurd k a) s
| JInl : H G k a t s,
  (mS vjobj v H (JT t KStar)) →
  jobj v H (JT s KStar) →
  jterm v H G a t
  jterm v H G (Inl k a) (TSum t s)
| JInr : H G k a t s,
  jobj v H (JT t KStar) →
  (mS vjobj v H (JT s KStar)) →
  jterm v H G a s
  jterm v H G (Inr k a) (TSum t s)
| JMatch : H G k a bl br tl tr s,
  (mS vjobj v H (JT tl KStar)) →
  (mS vjobj v H (JT tr KStar)) →
  (mS vjobj v H (JT s KStar)) →
  jterm v H G a (TSum tl tr) →
  jterm v H (GCons G tl) bl s
  jterm v H (GCons G tr) br s
  jterm v H G (Match k a bl br) s
| JGen : H G k k' a t,
  (mE vjobj v H (Jwf k' CKind)) →
  (mS vjobj v (HCons H k') (JT t KStar)) →
  jterm v (HCons H k') (lift 1 0 G) a t
  jterm v H G (Gen k a) (TPi k' t)
| JInst : H G k k' a t s,
  (mS vjobj v (HCons H k') (JT t KStar)) →
  jterm v H G a (TPi k' t) →
  jobj v H (JT s k') →
  jterm v H G (Inst k a) (subst s 0 t)
| JCoer : H H' HH' G a t s,
  Happ H H' HH'
  (mS vjobj v H (JH H')) →
  (mS vjobj v HH' (JT t KStar)) →
  jterm v HH' (lift (Hlength H') 0 G) a t
  jobj v H (JC YNil YNil H' t s) →
  jterm v H G a s
.