Library Lambda.CCSum.Types


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Export
 Lambda.MyList.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

Implicit
 Types
 A
 B
 M
 N
 T
 t
 u
 v
 : term.




  Definition
 env := list term.




  Implicit
 Types
 e
 f
 g
 : env.




  Definition
 item_lift t
 e
 n
 :=

    ex2 (fun
 u
 ⇒ t
 = lift (S n
) u
) (fun
 u
 ⇒ item term u
 (e
:list term) n
).




  Inductive
 wf
 : env → Prop
 :=

    | wf_nil : wf
 nil

    | wf_var : ∀ e
 T
 s
, typ e
 T
 (Srt s
) → wf
 (T
 :: e
)

with
 typ : env → term → term → Prop
 :=

  | type_prop : ∀ e
, wf
 e
 → typ e
 (Srt prop) (Srt kind)

  | type_set : ∀ e
, wf
 e
 → typ e
 (Srt set) (Srt kind)

  | type_var :

      ∀ e
,

      wf
 e
 → ∀ (v
 : nat) t
, item_lift t
 e
 v
 → typ e
 (Ref v
) t


  | type_abs :

      ∀ e
 T
 s1
,

      typ e
 T
 (Srt s1
) →

      ∀ M
 (U
 : term) s2
,

      typ (T
 :: e
) U
 (Srt s2
) →

      typ (T
 :: e
) M
 U
 → typ e
 (Abs T
 M
) (Prod T
 U
)

  | type_app :

      ∀ e
 v
 (V
 : term),

      typ e
 v
 V
 →

      ∀ u
 (Ur
 : term),

      typ e
 u
 (Prod V
 Ur
) → typ e
 (App u
 v
) (subst v
 Ur
)	

  | type_pair :

    ∀ e
 (U
 : term) s1
,

      typ e
 U
 (Srt s1
) →

      ∀ u
, typ e
 u
 U
 →

      ∀ V
 s2
, typ (U
 :: e
) V
 (Srt s2
) →

        ∀ v
, typ e
 v
 (subst u
 V
) → 

          typ e
 (Pair (Sum U
 V
) u
 v
) (Sum U
 V
)

  | type_prod :

      ∀ e
 T
 s1
,

      typ e
 T
 (Srt s1
) →

      ∀ (U
 : term) s2
,

      typ (T
 :: e
) U
 (Srt s2
) → typ e
 (Prod T
 U
) (Srt s2
)

  | type_sum :

      ∀ e
 T
 s1
,

      typ e
 T
 (Srt s1
) →

      ∀ (U
 : term) s2
,

      typ (T
 :: e
) U
 (Srt s2
) → typ e
 (Sum T
 U
) (Srt s2
)



  | type_subset :

      ∀ e
 T
 s1
,

      typ e
 T
 (Srt set) →

      ∀ (U
 : term),

      typ (T
 :: e
) U
 (Srt prop) → typ e
 (Subset T
 U
) (Srt set)



  | type_pi1 :

      ∀ e
 t
 U
 V
,

      typ e
 t
 (Sum U
 V
) → typ e
 (Pi1 t
) U




  | type_pi2 :

      ∀ e
 t
 U
 V
,

      typ e
 t
 (Sum U
 V
) → typ e
 (Pi2 t
) (subst (Pi1 t
) V
)



  | type_conv :

      ∀ e
 t
 (U
 V
 : term),

      typ e
 t
 U
 → conv U
 V
 → ∀ s
, typ e
 V
 (Srt s
) → typ e
 t
 V
.




  Hint
 Resolve
 wf_nil type_prop type_set type_var: coc
.




  Lemma
 type_prop_set :

   ∀ s
, is_prop s
 → ∀ e
, wf
 e
 → typ e
 (Srt s
) (Srt kind).




Lemma
 typ_free_db : ∀ e
 t
 T
, typ e
 t
 T
 → free_db (length e
) t
.




  Lemma
 typ_wf : ∀ e
 t
 T
, typ e
 t
 T
 → wf
 e
.




  Lemma
 wf_sort :

   ∀ n
 e
 f
,

   trunc _
 (S n
) e
 f
 →

   wf
 e
 → ∀ t
, item _
 t
 e
 n
 → ∃ s
 : sort, typ f
 t
 (Srt s
).