yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix the typing rules

Browse source
This commit is contained in:
Yiyun Liu 2025-03-03 01:38:22 -05:00
parent 47e21df801
commit b3bd75ad42
3 changed files with 103 additions and 126 deletions
Download patch file Download diff file Expand all files Collapse all files

7
theories/common.v
View file

@ -10,6 +10,13 @@ Inductive lookup : nat -> list PTm -> PTm -> Prop :=
lookup i Γ A -> lookup i Γ A ->
lookup (S i) (cons B Γ) (ren_PTm shift A). lookup (S i) (cons B Γ) (ren_PTm shift A).
Lemma here' A Γ U : U = ren_PTm shift A -> lookup 0 (A :: Γ) U.
Proof. move => ->. apply here. Qed.
Lemma there' i Γ A B U : U = ren_PTm shift A -> lookup i Γ A ->
lookup (S i) (cons B Γ) U.
Proof. move => ->. apply there. Qed.
Derive Inversion lookup_inv with (forall i Γ A, lookup i Γ A). Derive Inversion lookup_inv with (forall i Γ A, lookup i Γ A).
Definition renaming_ok (Γ : list PTm) (Δ : list PTm) (ξ : nat -> nat) := Definition renaming_ok (Γ : list PTm) (Δ : list PTm) (ξ : nat -> nat) :=

77
theories/structural.v
View file

@ -1,96 +1,69 @@
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing. Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing.
From Hammer Require Import Tactics. From Hammer Require Import Tactics.
Require Import ssreflect. Require Import ssreflect.
Require Import Psatz. Require Import Psatz.
Lemma wff_mutual : Lemma wff_mutual :
(forall n (Γ : fin n -> PTm n), ⊢ Γ -> True) /\ (forall Γ, ⊢ Γ -> True) /\
(forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ⊢ Γ) /\ (forall Γ (a A : PTm), Γ ⊢ a ∈ A -> ⊢ Γ) /\
(forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ⊢ Γ) /\ (forall Γ (a b A : PTm), Γ ⊢ a ≡ b ∈ A -> ⊢ Γ) /\
(forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> ⊢ Γ). (forall Γ (A B : PTm), Γ ⊢ A ≲ B -> ⊢ Γ).
Proof. apply wt_mutual; eauto. Qed. Proof. apply wt_mutual; eauto. Qed.
#[export]Hint Constructors Wt Wff Eq : wt. #[export]Hint Constructors Wt Wff Eq : wt.
Lemma T_Nat' n Γ : Lemma T_Nat' Γ :
⊢ Γ -> ⊢ Γ ->
Γ ⊢ PNat : PTm n ∈ PUniv 0. Γ ⊢ PNat ∈ PUniv 0.
Proof. apply T_Nat. Qed. Proof. apply T_Nat. Qed.
Lemma renaming_up n m (ξ : fin n -> fin m) Δ Γ A : Lemma renaming_up (ξ : nat -> nat) Δ Γ A :
renaming_ok Δ Γ ξ -> renaming_ok Δ Γ ξ ->
renaming_ok (funcomp (ren_PTm shift) (scons (ren_PTm ξ A) Δ)) (funcomp (ren_PTm shift) (scons A Γ)) (upRen_PTm_PTm ξ) . renaming_ok (cons (ren_PTm ξ A) Δ) (cons A Γ) (upRen_PTm_PTm ξ) .
Proof. Proof.
move => h i. move => h i A0.
destruct i as [i|]. elim /lookup_inv => //=_.
asimpl. rewrite /renaming_ok in h. - move => A1 Γ0 ? [*]. subst. apply here'. by asimpl.
rewrite /funcomp. rewrite -h. - move => i0 Γ0 A1 B h' ? [*]. subst.
by asimpl. apply : there'; eauto. by asimpl.
by asimpl.
Qed. Qed.
Lemma Su_Wt n Γ a i : Lemma Su_Wt Γ a i :
Γ ⊢ a ∈ @PUniv n i -> Γ ⊢ a ∈ PUniv i ->
Γ ⊢ a ≲ a. Γ ⊢ a ≲ a.
Proof. hauto lq:on ctrs:LEq, Eq. Qed. Proof. hauto lq:on ctrs:LEq, Eq. Qed.
Lemma Wt_Univ n Γ a A i Lemma Wt_Univ Γ a A i
(h : Γ ⊢ a ∈ A) : (h : Γ ⊢ a ∈ A) :
Γ ⊢ @PUniv n i ∈ PUniv (S i). Γ ⊢ @PUniv i ∈ PUniv (S i).
Proof. Proof.
hauto lq:on ctrs:Wt use:wff_mutual. hauto lq:on ctrs:Wt use:wff_mutual.
Qed. Qed.
Lemma Bind_Inv n Γ p (A : PTm n) B U : Lemma Bind_Inv Γ p (A : PTm) B U :
Γ ⊢ PBind p A B ∈ U -> Γ ⊢ PBind p A B ∈ U ->
exists i, Γ ⊢ A ∈ PUniv i /\ exists i, Γ ⊢ A ∈ PUniv i /\
funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i /\ (cons A Γ) ⊢ B ∈ PUniv i /\
Γ ⊢ PUniv i ≲ U. Γ ⊢ PUniv i ≲ U.
Proof. Proof.
move E :(PBind p A B) => T h. move E :(PBind p A B) => T h.
move : p A B E. move : p A B E.
elim : n Γ T U / h => //=. elim : Γ T U / h => //=.
- move => n Γ i p A B hA _ hB _ p0 A0 B0 [*]. subst. - move => Γ i p A B hA _ hB _ p0 A0 B0 [*]. subst.
exists i. repeat split => //=. exists i. repeat split => //=.
eapply wff_mutual in hA. eapply wff_mutual in hA.
apply Su_Univ; eauto. apply Su_Univ; eauto.
- hauto lq:on rew:off ctrs:LEq. - hauto lq:on rew:off ctrs:LEq.
Qed. Qed.
(* Lemma Pi_Inv n Γ (A : PTm n) B U : *) Lemma T_App' Γ (b a : PTm) A B U :
(* Γ ⊢ PBind PPi A B ∈ U -> *)
(* exists i, Γ ⊢ A ∈ PUniv i /\ *)
(* funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i /\ *)
(* Γ ⊢ PUniv i ≲ U. *)
(* Proof. *)
(* move E :(PBind PPi A B) => T h. *)
(* move : A B E. *)
(* elim : n Γ T U / h => //=. *)
(* - hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ. *)
(* - hauto lq:on rew:off ctrs:LEq. *)
(* Qed. *)
(* Lemma Bind_Inv n Γ (A : PTm n) B U : *)
(* Γ ⊢ PBind PSig A B ∈ U -> *)
(* exists i, Γ ⊢ A ∈ PUniv i /\ *)
(* funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i /\ *)
(* Γ ⊢ PUniv i ≲ U. *)
(* Proof. *)
(* move E :(PBind PSig A B) => T h. *)
(* move : A B E. *)
(* elim : n Γ T U / h => //=. *)
(* - hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ. *)
(* - hauto lq:on rew:off ctrs:LEq. *)
(* Qed. *)
Lemma T_App' n Γ (b a : PTm n) A B U :
U = subst_PTm (scons a VarPTm) B -> U = subst_PTm (scons a VarPTm) B ->
Γ ⊢ b ∈ PBind PPi A B -> Γ ⊢ b ∈ PBind PPi A B ->
Γ ⊢ a ∈ A -> Γ ⊢ a ∈ A ->
Γ ⊢ PApp b a ∈ U. Γ ⊢ PApp b a ∈ U.
Proof. move => ->. apply T_App. Qed. Proof. move => ->. apply T_App. Qed.
Lemma T_Pair' n Γ (a b : PTm n) A B i U : Lemma T_Pair' Γ (a b : PTm ) A B i U :
U = subst_PTm (scons a VarPTm) B -> U = subst_PTm (scons a VarPTm) B ->
Γ ⊢ a ∈ A -> Γ ⊢ a ∈ A ->
Γ ⊢ b ∈ U -> Γ ⊢ b ∈ U ->
@ -100,7 +73,7 @@ Proof.
move => ->. eauto using T_Pair. move => ->. eauto using T_Pair.
Qed. Qed.
Lemma E_IndCong' n Γ P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 i U : Lemma E_IndCong' Γ P0 P1 (a0 a1 : PTm ) b0 b1 c0 c1 i U :
U = subst_PTm (scons a0 VarPTm) P0 -> U = subst_PTm (scons a0 VarPTm) P0 ->
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ∈ PUniv i -> funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ∈ PUniv i ->
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i -> funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->

145
theories/typing.v
View file

@ -1,240 +1,237 @@
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax. Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
Reserved Notation "Γ ⊢ a ∈ A" (at level 70). Reserved Notation "Γ ⊢ a ∈ A" (at level 70).
Reserved Notation "Γ ⊢ a ≡ b ∈ A" (at level 70). Reserved Notation "Γ ⊢ a ≡ b ∈ A" (at level 70).
Reserved Notation "Γ ⊢ A ≲ B" (at level 70). Reserved Notation "Γ ⊢ A ≲ B" (at level 70).
Reserved Notation "⊢ Γ" (at level 70). Reserved Notation "⊢ Γ" (at level 70).
Inductive Wt : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop := Inductive Wt : list PTm -> PTm -> PTm -> Prop :=
| T_Var n Γ (i : fin n) : | T_Var i Γ A :
⊢ Γ -> ⊢ Γ ->
Γ ⊢ VarPTm i ∈ Γ i lookup i Γ A ->
Γ ⊢ VarPTm i ∈ A
| T_Bind n Γ i p (A : PTm n) (B : PTm (S n)) : | T_Bind Γ i p (A : PTm) (B : PTm) :
Γ ⊢ A ∈ PUniv i -> Γ ⊢ A ∈ PUniv i ->
funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i -> cons A Γ ⊢ B ∈ PUniv i ->
Γ ⊢ PBind p A B ∈ PUniv i Γ ⊢ PBind p A B ∈ PUniv i
| T_Abs n Γ (a : PTm (S n)) A B i : | T_Abs Γ (a : PTm) A B i :
Γ ⊢ PBind PPi A B ∈ (PUniv i) -> Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B -> (cons A Γ) ⊢ a ∈ B ->
Γ ⊢ PAbs a ∈ PBind PPi A B Γ ⊢ PAbs a ∈ PBind PPi A B
| T_App n Γ (b a : PTm n) A B : | T_App Γ (b a : PTm) A B :
Γ ⊢ b ∈ PBind PPi A B -> Γ ⊢ b ∈ PBind PPi A B ->
Γ ⊢ a ∈ A -> Γ ⊢ a ∈ A ->
Γ ⊢ PApp b a ∈ subst_PTm (scons a VarPTm) B Γ ⊢ PApp b a ∈ subst_PTm (scons a VarPTm) B
| T_Pair n Γ (a b : PTm n) A B i : | T_Pair Γ (a b : PTm) A B i :
Γ ⊢ PBind PSig A B ∈ (PUniv i) -> Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
Γ ⊢ a ∈ A -> Γ ⊢ a ∈ A ->
Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B -> Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
Γ ⊢ PPair a b ∈ PBind PSig A B Γ ⊢ PPair a b ∈ PBind PSig A B
| T_Proj1 n Γ (a : PTm n) A B : | T_Proj1 Γ (a : PTm) A B :
Γ ⊢ a ∈ PBind PSig A B -> Γ ⊢ a ∈ PBind PSig A B ->
Γ ⊢ PProj PL a ∈ A Γ ⊢ PProj PL a ∈ A
| T_Proj2 n Γ (a : PTm n) A B : | T_Proj2 Γ (a : PTm) A B :
Γ ⊢ a ∈ PBind PSig A B -> Γ ⊢ a ∈ PBind PSig A B ->
Γ ⊢ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B Γ ⊢ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B
| T_Univ n Γ i : | T_Univ Γ i :
⊢ Γ -> ⊢ Γ ->
Γ ⊢ PUniv i : PTm n ∈ PUniv (S i) Γ ⊢ PUniv i ∈ PUniv (S i)
| T_Nat n Γ i : | T_Nat Γ i :
⊢ Γ -> ⊢ Γ ->
Γ ⊢ PNat : PTm n ∈ PUniv i Γ ⊢ PNat ∈ PUniv i
| T_Zero n Γ : | T_Zero Γ :
⊢ Γ -> ⊢ Γ ->
Γ ⊢ PZero : PTm n ∈ PNat Γ ⊢ PZero ∈ PNat
| T_Suc n Γ (a : PTm n) : | T_Suc Γ (a : PTm) :
Γ ⊢ a ∈ PNat -> Γ ⊢ a ∈ PNat ->
Γ ⊢ PSuc a ∈ PNat Γ ⊢ PSuc a ∈ PNat
| T_Ind s Γ P (a : PTm s) b c i : | T_Ind Γ P (a : PTm) b c i :
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i -> cons PNat Γ ⊢ P ∈ PUniv i ->
Γ ⊢ a ∈ PNat -> Γ ⊢ a ∈ PNat ->
Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P -> Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
Γ ⊢ PInd P a b c ∈ subst_PTm (scons a VarPTm) P Γ ⊢ PInd P a b c ∈ subst_PTm (scons a VarPTm) P
| T_Conv n Γ (a : PTm n) A B : | T_Conv Γ (a : PTm) A B :
Γ ⊢ a ∈ A -> Γ ⊢ a ∈ A ->
Γ ⊢ A ≲ B -> Γ ⊢ A ≲ B ->
Γ ⊢ a ∈ B Γ ⊢ a ∈ B
with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop := with Eq : list PTm -> PTm -> PTm -> PTm -> Prop :=
(* Structural *) (* Structural *)
| E_Refl n Γ (a : PTm n) A : | E_Refl Γ (a : PTm ) A :
Γ ⊢ a ∈ A -> Γ ⊢ a ∈ A ->
Γ ⊢ a ≡ a ∈ A Γ ⊢ a ≡ a ∈ A
| E_Symmetric n Γ (a b : PTm n) A : | E_Symmetric Γ (a b : PTm) A :
Γ ⊢ a ≡ b ∈ A -> Γ ⊢ a ≡ b ∈ A ->
Γ ⊢ b ≡ a ∈ A Γ ⊢ b ≡ a ∈ A
| E_Transitive n Γ (a b c : PTm n) A : | E_Transitive Γ (a b c : PTm) A :
Γ ⊢ a ≡ b ∈ A -> Γ ⊢ a ≡ b ∈ A ->
Γ ⊢ b ≡ c ∈ A -> Γ ⊢ b ≡ c ∈ A ->
Γ ⊢ a ≡ c ∈ A Γ ⊢ a ≡ c ∈ A
(* Congruence *) (* Congruence *)
| E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 : | E_Bind Γ i p (A0 A1 : PTm) B0 B1 :
⊢ Γ ->
Γ ⊢ A0 ∈ PUniv i -> Γ ⊢ A0 ∈ PUniv i ->
Γ ⊢ A0 ≡ A1 ∈ PUniv i -> Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i -> (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i
| E_Abs n Γ (a b : PTm (S n)) A B i : | E_Abs Γ (a b : PTm) A B i :
Γ ⊢ PBind PPi A B ∈ (PUniv i) -> Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
funcomp (ren_PTm shift) (scons A Γ) ⊢ a ≡ b ∈ B -> (cons A Γ) ⊢ a ≡ b ∈ B ->
Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B
| E_App n Γ i (b0 b1 a0 a1 : PTm n) A B : | E_App Γ i (b0 b1 a0 a1 : PTm) A B :
Γ ⊢ PBind PPi A B ∈ (PUniv i) -> Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B -> Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
Γ ⊢ a0 ≡ a1 ∈ A -> Γ ⊢ a0 ≡ a1 ∈ A ->
Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B
| E_Pair n Γ (a0 a1 b0 b1 : PTm n) A B i : | E_Pair Γ (a0 a1 b0 b1 : PTm) A B i :
Γ ⊢ PBind PSig A B ∈ (PUniv i) -> Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
Γ ⊢ a0 ≡ a1 ∈ A -> Γ ⊢ a0 ≡ a1 ∈ A ->
Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B -> Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B ->
Γ ⊢ PPair a0 b0 ≡ PPair a1 b1 ∈ PBind PSig A B Γ ⊢ PPair a0 b0 ≡ PPair a1 b1 ∈ PBind PSig A B
| E_Proj1 n Γ (a b : PTm n) A B : | E_Proj1 Γ (a b : PTm) A B :
Γ ⊢ a ≡ b ∈ PBind PSig A B -> Γ ⊢ a ≡ b ∈ PBind PSig A B ->
Γ ⊢ PProj PL a ≡ PProj PL b ∈ A Γ ⊢ PProj PL a ≡ PProj PL b ∈ A
| E_Proj2 n Γ i (a b : PTm n) A B : | E_Proj2 Γ i (a b : PTm) A B :
Γ ⊢ PBind PSig A B ∈ (PUniv i) -> Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
Γ ⊢ a ≡ b ∈ PBind PSig A B -> Γ ⊢ a ≡ b ∈ PBind PSig A B ->
Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B
| E_IndCong n Γ P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 i : | E_IndCong Γ P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 i :
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ∈ PUniv i -> (cons PNat Γ) ⊢ P0 ∈ PUniv i ->
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i -> (cons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
Γ ⊢ a0 ≡ a1 ∈ PNat -> Γ ⊢ a0 ≡ a1 ∈ PNat ->
Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 -> Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 ->
funcomp (ren_PTm shift) (scons P0 (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) -> (cons P0 ((cons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) ->
Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P0 Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P0
| E_SucCong n Γ (a b : PTm n) : | E_SucCong Γ (a b : PTm) :
Γ ⊢ a ≡ b ∈ PNat -> Γ ⊢ a ≡ b ∈ PNat ->
Γ ⊢ PSuc a ≡ PSuc b ∈ PNat Γ ⊢ PSuc a ≡ PSuc b ∈ PNat
| E_Conv n Γ (a b : PTm n) A B : | E_Conv Γ (a b : PTm) A B :
Γ ⊢ a ≡ b ∈ A -> Γ ⊢ a ≡ b ∈ A ->
Γ ⊢ A ≲ B -> Γ ⊢ A ≲ B ->
Γ ⊢ a ≡ b ∈ B Γ ⊢ a ≡ b ∈ B
(* Beta *) (* Beta *)
| E_AppAbs n Γ (a : PTm (S n)) b A B i: | E_AppAbs Γ (a : PTm) b A B i:
Γ ⊢ PBind PPi A B ∈ PUniv i -> Γ ⊢ PBind PPi A B ∈ PUniv i ->
Γ ⊢ b ∈ A -> Γ ⊢ b ∈ A ->
funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B -> (cons A Γ) ⊢ a ∈ B ->
Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B
| E_ProjPair1 n Γ (a b : PTm n) A B i : | E_ProjPair1 Γ (a b : PTm) A B i :
Γ ⊢ PBind PSig A B ∈ (PUniv i) -> Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
Γ ⊢ a ∈ A -> Γ ⊢ a ∈ A ->
Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B -> Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A
| E_ProjPair2 n Γ (a b : PTm n) A B i : | E_ProjPair2 Γ (a b : PTm) A B i :
Γ ⊢ PBind PSig A B ∈ (PUniv i) -> Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
Γ ⊢ a ∈ A -> Γ ⊢ a ∈ A ->
Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B -> Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
Γ ⊢ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B Γ ⊢ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B
| E_IndZero n Γ P i (b : PTm n) c : | E_IndZero Γ P i (b : PTm) c :
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i -> (cons PNat Γ) ⊢ P ∈ PUniv i ->
Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P -> Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
Γ ⊢ PInd P PZero b c ≡ b ∈ subst_PTm (scons PZero VarPTm) P Γ ⊢ PInd P PZero b c ≡ b ∈ subst_PTm (scons PZero VarPTm) P
| E_IndSuc s Γ P (a : PTm s) b c i : | E_IndSuc Γ P (a : PTm) b c i :
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i -> (cons PNat Γ) ⊢ P ∈ PUniv i ->
Γ ⊢ a ∈ PNat -> Γ ⊢ a ∈ PNat ->
Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P -> Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
Γ ⊢ PInd P (PSuc a) b c ≡ (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ∈ subst_PTm (scons (PSuc a) VarPTm) P Γ ⊢ PInd P (PSuc a) b c ≡ (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ∈ subst_PTm (scons (PSuc a) VarPTm) P
(* Eta *) (* Eta *)
| E_AppEta n Γ (b : PTm n) A B i : | E_AppEta Γ (b : PTm) A B i :
⊢ Γ ->
Γ ⊢ PBind PPi A B ∈ (PUniv i) -> Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
Γ ⊢ b ∈ PBind PPi A B -> Γ ⊢ b ∈ PBind PPi A B ->
Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B
| E_PairEta n Γ (a : PTm n) A B i : | E_PairEta Γ (a : PTm ) A B i :
Γ ⊢ PBind PSig A B ∈ (PUniv i) -> Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
Γ ⊢ a ∈ PBind PSig A B -> Γ ⊢ a ∈ PBind PSig A B ->
Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B
with LEq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop := with LEq : list PTm -> PTm -> PTm -> Prop :=
(* Structural *) (* Structural *)
| Su_Transitive n Γ (A B C : PTm n) : | Su_Transitive Γ (A B C : PTm) :
Γ ⊢ A ≲ B -> Γ ⊢ A ≲ B ->
Γ ⊢ B ≲ C -> Γ ⊢ B ≲ C ->
Γ ⊢ A ≲ C Γ ⊢ A ≲ C
(* Congruence *) (* Congruence *)
| Su_Univ n Γ i j : | Su_Univ Γ i j :
⊢ Γ -> ⊢ Γ ->
i <= j -> i <= j ->
Γ ⊢ PUniv i : PTm n ≲ PUniv j Γ ⊢ PUniv i ≲ PUniv j
| Su_Pi n Γ (A0 A1 : PTm n) B0 B1 i : | Su_Pi Γ (A0 A1 : PTm) B0 B1 i :
⊢ Γ ->
Γ ⊢ A0 ∈ PUniv i -> Γ ⊢ A0 ∈ PUniv i ->
Γ ⊢ A1 ≲ A0 -> Γ ⊢ A1 ≲ A0 ->
funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≲ B1 -> (cons A0 Γ) ⊢ B0 ≲ B1 ->
Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1
| Su_Sig n Γ (A0 A1 : PTm n) B0 B1 i : | Su_Sig Γ (A0 A1 : PTm) B0 B1 i :
⊢ Γ ->
Γ ⊢ A1 ∈ PUniv i -> Γ ⊢ A1 ∈ PUniv i ->
Γ ⊢ A0 ≲ A1 -> Γ ⊢ A0 ≲ A1 ->
funcomp (ren_PTm shift) (scons A1 Γ) ⊢ B0 ≲ B1 -> (cons A1 Γ) ⊢ B0 ≲ B1 ->
Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1
(* Injecting from equalities *) (* Injecting from equalities *)
| Su_Eq n Γ (A : PTm n) B i : | Su_Eq Γ (A : PTm) B i :
Γ ⊢ A ≡ B ∈ PUniv i -> Γ ⊢ A ≡ B ∈ PUniv i ->
Γ ⊢ A ≲ B Γ ⊢ A ≲ B
(* Projection axioms *) (* Projection axioms *)
| Su_Pi_Proj1 n Γ (A0 A1 : PTm n) B0 B1 : | Su_Pi_Proj1 Γ (A0 A1 : PTm) B0 B1 :
Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 -> Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
Γ ⊢ A1 ≲ A0 Γ ⊢ A1 ≲ A0
| Su_Sig_Proj1 n Γ (A0 A1 : PTm n) B0 B1 : | Su_Sig_Proj1 Γ (A0 A1 : PTm) B0 B1 :
Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 -> Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
Γ ⊢ A0 ≲ A1 Γ ⊢ A0 ≲ A1
| Su_Pi_Proj2 n Γ (a0 a1 A0 A1 : PTm n) B0 B1 : | Su_Pi_Proj2 Γ (a0 a1 A0 A1 : PTm ) B0 B1 :
Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 -> Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
Γ ⊢ a0 ≡ a1 ∈ A1 -> Γ ⊢ a0 ≡ a1 ∈ A1 ->
Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1 Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1
| Su_Sig_Proj2 n Γ (a0 a1 A0 A1 : PTm n) B0 B1 : | Su_Sig_Proj2 Γ (a0 a1 A0 A1 : PTm) B0 B1 :
Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 -> Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
Γ ⊢ a0 ≡ a1 ∈ A0 -> Γ ⊢ a0 ≡ a1 ∈ A0 ->
Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1 Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1
with Wff : forall {n}, (fin n -> PTm n) -> Prop := with Wff : list PTm -> Prop :=
| Wff_Nil : | Wff_Nil :
⊢ null ⊢ nil
| Wff_Cons n Γ (A : PTm n) i : | Wff_Cons Γ (A : PTm) i :
⊢ Γ -> ⊢ Γ ->
Γ ⊢ A ∈ PUniv i -> Γ ⊢ A ∈ PUniv i ->
(* -------------------------------- *) (* -------------------------------- *)
⊢ funcomp (ren_PTm shift) (scons A Γ) ⊢ (cons A Γ)
where where
"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B). "Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B).