Definition of Validity

theories/LogicalRelation.v

@@ -1376,7 +1376,7 @@ Section MoreDefs.
     : [LogRel@{i j k l} l | Γ ||- A]< k > :=
     LRbuild (LRId (LogRelRec l) IA IAad).
 
-    Record WLogRel@{i j k l} (l : TypeLevel) wl Γ A :=
+  Record WLogRel@{i j k l} (l : TypeLevel) wl Γ A :=
     { WT : DTree wl  ;
       WRed {wl'} (Ho : over_tree wl wl' WT) :
       [ LogRel@{i j k l} l | Γ ||- A ]< wl' > ;

theories/LogicalRelation/Escape.v

@@ -295,3 +295,23 @@ Ltac escape :=
     try pose proof (X := escapeEqTerm RA H) ;
     block H
   end; unblock.
+
+Ltac Wescape :=
+  repeat lazymatch goal with
+  | [H : W[_ ||-< _ > _]< _ > |- _] => 
+    let X := fresh "Esc" H in
+    try pose proof (X := Wescape H) ;
+    block H
+  | [H : W[_ ||-<_> _ ≅ _ | ?RA ]< _ > |- _] =>
+    let X := fresh "Esc" H in
+    try pose proof (X := WescapeEq RA H) ;
+    block H
+  | [H : W[_ ||-<_> _ : _ | ?RA]< _ > |- _] =>
+    let X := fresh "R" H in
+    try pose proof (X := WescapeTerm RA H) ;
+    block H
+  | [H : W[_ ||-<_> _ ≅ _ : _ | ?RA]< _ > |- _] =>
+    let X := fresh "R" H in
+    try pose proof (X := WescapeEqTerm RA H) ;
+    block H
+  end; unblock.

theories/LogicalRelation/Id.v

@@ -316,7 +316,7 @@ Proof.
   pose proof (IdRedTy_inv (invLRId RIAxy)) as [eA ex ey].
   pose proof (hred := Re.(IdRedTm.red)); unfold_id_outTy; rewrite <-eA,<-ex,<-ey in hred.
   eapply redSubstTerm.
-  - About redTmFwd. pose proof (redTmFwdConv Re hred (IdProp_whnf _ _ (IdRedTm.prop Re))) as [Rnf Rnfeq].
+  - pose proof (redTmFwdConv Re hred (IdProp_whnf _ _ (IdRedTm.prop Re))) as [Rnf Rnfeq].
     eapply LRTmRedConv.
     2: eapply idElimPropRed; tea; exact (IdRedTm.prop Re).
     unshelve eapply LRTyEqSym.

theories/LogicalRelation/Irrelevance.v

@@ -1311,3 +1311,13 @@ Ltac irrelevance0 :=
 Ltac irrelevance := irrelevance0 ; [|eassumption] ; try first [reflexivity| now bsimpl].
 
 Ltac irrelevanceRefl := irrelevance0 ; [reflexivity|].
+
+Ltac Wirrelevance0 :=
+  lazymatch goal with
+  | [|- W[_ ||-<_> _ ≅ _ | _ ]< _ > ] => eapply WLRTyEqIrrelevant'
+  | [|- W[_ ||-<_> _ : _ | _ ]< _ > ] => eapply WLRTmRedIrrelevant'
+  | [|- W[_ ||-<_> _ ≅ _ : _ | _ ]< _ > ] => eapply WLRTmEqIrrelevant'
+  | [|- W[_ ||-<_> _ : _ | _]< _ > × [_ ||-<_> _≅ _ : _ | _]< _ >] => eapply WLRTmTmEqIrrelevant'
+  end.
+
+Ltac Wirrelevance := Wirrelevance0 ; [|eassumption] ; try first [reflexivity| now bsimpl].

theories/LogicalRelation/Neutral.v

@@ -633,6 +633,27 @@ Proof.
   intros; now eapply completeness.
 Qed.
 
+Lemma WneuTerm {l wl Γ A} (RA : W[Γ ||-<l> A]< wl >) {n} :
+  [Γ |- n : A]< wl > ->
+  [Γ |- n ~ n : A]< wl > ->
+  W[Γ ||-<l> n : A | RA]< wl >.
+Proof.
+  intros ; unshelve econstructor ; [now econstructor | intros].
+  eapply neuTerm ; [now eapply ty_Ltrans | ].
+  now eapply convneu_Ltrans.
+Qed.
+
+Lemma WneuTermEq {l wl Γ A} (RA : W[Γ ||-<l> A]< wl >) {n n'} :
+  [Γ |- n : A]< wl > ->
+  [Γ |- n' : A]< wl > ->
+  [Γ |- n ~ n' : A]< wl > ->
+  W[Γ ||-<l> n ≅ n' : A| RA]< wl >.
+Proof.
+  intros ; unshelve econstructor ; [now econstructor | intros].
+  eapply neuTermEq ; [ | | now eapply convneu_Ltrans ].
+  all: now eapply ty_Ltrans.
+Qed.
+
 Lemma var0conv {l wl Γ A A'} (RA : [Γ ,, A ||-<l> A']< wl >) :
   [Γ,, A |- A⟨↑⟩ ≅ A']< wl > ->
   [Γ |- A]< wl > ->
@@ -653,4 +674,13 @@ Proof.
   eapply reflLRTyEq.
 Qed.
 
+Lemma Wvar0 {l wl Γ A A'} (RA : W[Γ ,, A ||-<l> A']< wl >) :
+  A⟨↑⟩ = A' ->
+  [Γ |- A]< wl > ->
+  W[Γ ,, A ||-<l> tRel 0 : A' | RA]< wl >.
+Proof.
+  intros eq HA ; unshelve econstructor ; [now econstructor | ].
+  intros wl' Hover Hover' ; eapply var0 ; [eassumption | ].
+  now eapply wft_Ltrans ; [eapply over_tree_le | ].
+Qed.
 End Neutral.

theories/LogicalRelation/Weakening.v

@@ -545,5 +545,17 @@ Lemma wkEq@{i j k l} {wl Γ Δ A B l} (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]< wl >) (lr
       all: eapply (IA.(IdRedTy.tyKripkeTmEq) _ _ _ (idε _) (idε _)); [now rewrite wk_comp_runit| irrelevance].
       Unshelve. all: tea.
   Qed.
+
+  Lemma WwkTermEq {wl Γ Δ t u A l} (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]< wl >) (lrA : W[Γ ||-<l> A]< wl >) : 
+    W[Γ ||-<l> t ≅ u : A | lrA]< wl > -> W[Δ ||-<l> t⟨ρ⟩ ≅ u⟨ρ⟩: A⟨ρ⟩ | Wwk ρ wfΔ lrA]< wl >.
+  Proof.
+    intros [].
+    exists WTTmEq.
+    intros.
+    eapply wkTermEq.
+    now eapply WRedTmEq.
+  Qed.
+
+
 End Weakenings.
 

theories/Notations.v

@@ -268,14 +268,14 @@ Reserved Notation "[ Γ ||-Id< l > t ≅ u : A | RA ]< p >" (at level 0, Γ, p,
 
 
 (** ** Validity notations *)
-Reserved Notation "[||-v Γ ]" (at level 0, Γ at level 50).
-Reserved Notation "[ Δ ||-v σ : Γ | VΓ | wfΔ ]" (at level 0, Δ, σ, Γ, VΓ, wfΔ at level 50).
-Reserved Notation "[ Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | vσ ]" (at level 0, Δ, σ, σ', Γ, VΓ, wfΔ, vσ at level 50).
-Reserved Notation "[ Γ ||-v< l > A | VΓ ]" (at level 0, Γ, l , A, VΓ at level 50).
-Reserved Notation "[ P | Δ ||-v σ : Γ | wfΔ ]" (at level 0, P, Δ, σ, Γ, wfΔ at level 50).
-Reserved Notation "[ P | Δ ||-v σ ≅ σ' : Γ | wfΔ | vσ ]"  (at level 0, P, Δ, σ, σ', Γ, wfΔ, vσ at level 50).
-Reserved Notation "[ R | ||-v Γ ]"  (at level 0, R, Γ at level 50).
-Reserved Notation "[ R | Δ ||-v σ : Γ | RΓ | wfΔ ]"  (at level 0, R, Δ, σ, Γ, RΓ, wfΔ at level 50).
-Reserved Notation "[ R | Δ ||-v σ ≅ σ' : Γ | RΓ | wfΔ | vσ ]" (at level 0, R, Δ, σ, σ', Γ, RΓ, wfΔ, vσ at level 50).
-Reserved Notation "[ P | Γ ||-v< l > A ]"  (at level 0, P, Γ, l, A at level 50).
+Reserved Notation "[||-v Γ ]< wl >" (at level 0, wl, Γ at level 50).
+Reserved Notation "[ Δ ||-v σ : Γ | VΓ | wfΔ ]< wl >" (at level 0, Δ, σ, wl, Γ, VΓ, wfΔ at level 50).
+Reserved Notation "[ Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | vσ ]< wl >" (at level 0, Δ, σ, σ', wl, Γ, VΓ, wfΔ, vσ at level 50).
+Reserved Notation "[ Γ ||-v< l > A | VΓ ]< wl >" (at level 0, wl, Γ, l , A, VΓ at level 50).
+Reserved Notation "[ P | Δ ||-v σ : Γ | wfΔ ]< wl >" (at level 0, P, Δ, σ, wl, Γ, wfΔ at level 50).
+Reserved Notation "[ P | Δ ||-v σ ≅ σ' : Γ | wfΔ | vσ ]< wl >"  (at level 0, P, Δ, σ, σ', wl, Γ, wfΔ, vσ at level 50).
+Reserved Notation "[ R | ||-v Γ ]< wl >"  (at level 0, R, wl, Γ at level 50).
+Reserved Notation "[ R | Δ ||-v σ : Γ | RΓ | wfΔ ]< wl >"  (at level 0, R, Δ, σ, wl, Γ, RΓ, wfΔ at level 50).
+Reserved Notation "[ R | Δ ||-v σ ≅ σ' : Γ | RΓ | wfΔ | vσ ]< wl >" (at level 0, R, Δ, σ, σ', wl, Γ, RΓ, wfΔ, vσ at level 50).
+Reserved Notation "[ P | Γ ||-v< l > A ]< wl >"  (at level 0, P, wl, Γ, l, A at level 50).