Add judgement for type subsumption

theories/Core/Syntactic/System/Definitions.v

@@ -25,6 +25,7 @@ Inductive wf_ctx : ctx -> Prop :=
      {{ Γ ⊢ A : Type@i }} ->
      {{ ⊢ Γ , A }} )
 where "⊢ Γ" := (wf_ctx Γ) (in custom judg) : type_scope
+
 with wf_ctx_eq : ctx -> ctx -> Prop :=
 | wf_ctx_eq_empty : {{ ⊢ ⋅ ≈ ⋅ }}
 | wf_ctx_eq_extend :
@@ -35,6 +36,7 @@ with wf_ctx_eq : ctx -> ctx -> Prop :=
      {{ Δ ⊢ A ≈ A' : Type@i }} ->
      {{ ⊢ Γ , A ≈ Δ , A' }} )
 where "⊢ Γ ≈ Γ'" := (wf_ctx_eq Γ Γ') (in custom judg) : type_scope
+
 with wf_exp : ctx -> exp -> typ -> Prop :=
 | wf_univ :
   `( {{ ⊢ Γ }} ->
@@ -84,6 +86,7 @@ with wf_exp : ctx -> exp -> typ -> Prop :=
   `( {{ Γ ⊢ A : Type@i }} ->
      {{ Γ ⊢ A : Type@(S i) }} )
 where "Γ ⊢ M : A" := (wf_exp Γ M A) (in custom judg) : type_scope
+
 with wf_sub : ctx -> sub -> ctx -> Prop :=
 | wf_sub_id :
   `( {{ ⊢ Γ }} ->
@@ -105,6 +108,7 @@ with wf_sub : ctx -> sub -> ctx -> Prop :=
      {{ ⊢ Δ ≈ Δ' }} ->
      {{ Γ ⊢s σ : Δ' }} )
 where "Γ ⊢s σ : Δ" := (wf_sub Γ σ Δ) (in custom judg) : type_scope
+
 with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
 | wf_exp_eq_typ_sub :
   `( {{ Γ ⊢s σ : Δ }} ->
@@ -300,20 +304,65 @@ with wf_sub_mut_ind := Induction for wf_sub Sort Prop
 with wf_sub_eq_mut_ind := Induction for wf_sub_eq Sort Prop.
 
 #[export]
-Hint Constructors wf_ctx wf_ctx_eq wf_exp wf_sub wf_exp_eq wf_sub_eq ctx_lookup: mcltt.
+Hint Constructors wf_ctx wf_ctx_eq wf_exp wf_sub wf_exp_eq wf_sub_eq ctx_lookup : mcltt.
 
 #[export]
-  Instance WfExpPER Γ A : PER (wf_exp_eq Γ A).
+Instance wf_exp_PER Γ A : PER (wf_exp_eq Γ A).
 Proof.
   split.
   - eauto using wf_exp_eq_sym.
   - eauto using wf_exp_eq_trans.
 Qed.
 
 #[export]
-  Instance WfSubPER Γ Δ : PER (wf_sub_eq Γ Δ).
+Instance wf_sub_PER Γ Δ : PER (wf_sub_eq Γ Δ).
 Proof.
   split.
   - eauto using wf_sub_eq_sym.
   - eauto using wf_sub_eq_trans.
 Qed.
+
+Reserved Notation "Γ ⊢ A ⊆ A'" (in custom judg at level 80, Γ custom exp, A custom exp, A' custom exp).
+
+Inductive typ_subsumption : ctx -> typ -> typ -> Prop :=
+| typ_subsumption_typ :
+  `{ {{ ⊢ Γ }} ->
+     {{ Γ ⊢ Type@i ⊆ Type@(S i) }} }
+| typ_subsumption_exp_eq :
+  `{ {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ ⊢ A ⊆ A' }} }
+| typ_subsumption_trans :
+  `{ {{ Γ ⊢ A ⊆ A' }} ->
+     {{ Γ ⊢ A' ⊆ A'' }} ->
+     {{ Γ ⊢ A ⊆ A'' }} }
+where "Γ ⊢ A ⊆ A'" := (typ_subsumption Γ A A') (in custom judg) : type_scope.
+
+#[export]
+Hint Constructors typ_subsumption : mcltt.
+
+#[export]
+Instance typ_subsumption_Transitive Γ : Transitive (typ_subsumption Γ).
+Proof.
+  eauto using typ_subsumption_trans.
+Qed.
+
+Inductive nf_subsumption : nf -> nf -> Prop :=
+| nf_subsumption_typ :
+  `{ nf_subsumption n{{{ Type@i }}} n{{{ Type@(S i) }}} }
+| nf_subsumption_eq :
+  `{ A = A' ->
+     nf_subsumption A A' }
+| nf_subsumption_trans :
+  `{ nf_subsumption A A' ->
+     nf_subsumption A' A'' ->
+     nf_subsumption A A'' }
+.
+
+#[export]
+Hint Constructors nf_subsumption : mcltt.
+
+#[export]
+Instance nf_subsumption_Transitive : Transitive nf_subsumption.
+Proof.
+  eauto using nf_subsumption_trans.
+Qed.

theories/Core/Syntactic/System/Lemmas.v

@@ -652,3 +652,35 @@ Qed.
 
 #[export]
 Hint Resolve sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : mcltt.
+
+Lemma typ_subsumption_ge : forall {Γ i j},
+    {{ ⊢ Γ }} ->
+    i <= j ->
+    {{ Γ ⊢ Type@i ⊆ Type@j }}.
+Proof.
+  induction 2; mauto.
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_ge : mcltt.
+
+Lemma nf_subsumption_ge : forall {i j},
+    i <= j ->
+    nf_subsumption n{{{ Type@i }}} n{{{ Type@j }}}.
+Proof.
+  induction 1; mauto.
+Qed.
+
+#[export]
+Hint Resolve nf_subsumption_ge : mcltt.
+
+Lemma wf_exp_respects_typ_subsumption : forall {Γ M A A'},
+    {{ Γ ⊢ M : A }} ->
+    {{ Γ ⊢ A ⊆ A' }} ->
+    {{ Γ ⊢ M : A' }}.
+Proof.
+  induction 2; mauto.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_respects_typ_subsumption : mcltt.