Require Import base ord ars data.fintype ccomega.sorts ccomega.syntax ccomega.reduction ccomega.subtyping.

Definition ctx n := tm n -> tm n -> Prop.

Reserved Notation "[ Gamma |- ]".
Reserved Notation "[ Gamma |- s :- A ]".

Inductive ext {n} (Gamma : ctx n) (A : tm n) : ctx n.+1 :=
| ext_bound : ext Gamma A (var bound) (rename shift A)
| ext_shift s B : Gamma s B -> ext Gamma A (rename shift s) (rename shift B).

Inductive has_type {n} (Gamma : ctx n) : ctx n :=
| ty_var s A :
    Gamma s A ->
    [ Gamma |- s :- A ]
| ty_sort u :
    [ Gamma |- univ n u :- univ n (sort_succ u) ]
| ty_app A B s t :
    [ Gamma |- s :- prod A B ] ->
    [ Gamma |- t :- A ] ->
    [ Gamma |- app s t :- inst (t .: @var _) B ]
| ty_lam A B s u :
    [ Gamma |- A :- univ n u ] ->
    [ ext Gamma A |- s :- B ] ->
    [ Gamma |- lam s :- prod A B ]
| ty_prod A B u v :
    [ Gamma |- A :- univ n u ] ->
    [ ext Gamma A |- B :- univ n.+1 v ] ->
    [ Gamma |- prod A B :- univ n (sort_prod u v) ]
| ty_sub u A B s :
    A <: B ->
    [ Gamma |- B :- univ n u ] ->
    [ Gamma |- s :- A ] ->
    [ Gamma |- s :- B ]
where "[ Gamma |- s :- A ]" := (@has_type _ Gamma s A).

Definition is_type {n} (Gamma : ctx n) (A : tm n) :=
  exists u, Gamma A (univ n u).

Definition context_ok {n} (Gamma : ctx n) :=
  forall s A, Gamma s A -> is_type (has_type Gamma) A.

Lemma ty_eapp n (Gamma : ctx n) A B C s t :
  C = inst (t .: @var _) B ->
  [ Gamma |- s :- prod A B ] -> [ Gamma |- t :- A ] ->
  [ Gamma |- app s t :- C ].
Proof. move=>->. exact: ty_app. Qed.

Notation "[ Gamma |- s ]" := (is_type (has_type Gamma) s).

Lemma ty_sort_wf n Gamma u : [ Gamma |- univ n u ].
Proof. exists (sort_succ u). exact: ty_sort. Qed.
Hint Resolve ty_sort_wf ty_sort.

Lemma ty_prod_wf n (Gamma : ctx n) A B :
  [ Gamma |- A ] -> [ ext Gamma A |- B ] -> [ Gamma |- prod A B ].
Proof.
  move=> [u tp1] [v tp2]. exists (sort_prod u v). apply: ty_prod.
  - eapply (ty_sub (A := univ _ u)); eauto=> //.
  - eapply (ty_sub (A := univ _ v)); eauto.
Qed.