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

Update the typing rules with projections

Browse source
This commit is contained in:
Yiyun Liu 2025-02-08 22:45:07 -05:00
parent 5996c45526
commit 0c83044d72
2 changed files with 23 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

1
theories/logrel.v
View file

@ -24,6 +24,7 @@ Inductive InterpExt {n} i (I : nat -> PTm n -> Prop) : PTm n -> (PTm n -> Prop)
| InterpExt_Ne A : | InterpExt_Ne A :
SNe A -> SNe A ->
⟦ A ⟧ i ;; I ↘ (fun a => exists v, rtc TRedSN a v /\ SNe v) ⟦ A ⟧ i ;; I ↘ (fun a => exists v, rtc TRedSN a v /\ SNe v)
| InterpExt_Bind p A B PA PF : | InterpExt_Bind p A B PA PF :
⟦ A ⟧ i ;; I ↘ PA -> ⟦ A ⟧ i ;; I ↘ PA ->
(forall a, PA a -> exists PB, PF a PB) -> (forall a, PA a -> exists PB, PF a PB) ->

28
theories/typing.v
View file

@ -108,21 +108,37 @@ with LEq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
i <= j -> i <= j ->
Γ ⊢ PUniv i : PTm n ≲ PUniv j Γ ⊢ PUniv i : PTm n ≲ PUniv j
| Su_Bind n Γ p (A0 A1 : PTm n) B0 B1 : | Su_Pi n Γ (A0 A1 : PTm n) B0 B1 :
⊢ Γ ->
Γ ⊢ A1 ≲ A0 -> Γ ⊢ A1 ≲ A0 ->
funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≲ B1 -> funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≲ B1 ->
Γ ⊢ PBind p A0 B0 ≲ PBind p A1 B1 Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1
| Su_Sig n Γ (A0 A1 : PTm n) B0 B1 :
⊢ Γ ->
Γ ⊢ A0 ≲ A1 ->
funcomp (ren_PTm shift) (scons A1 Γ) ⊢ B0 ≲ B1 ->
Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1
| Su_Eq n Γ (A : PTm n) B i : | Su_Eq n Γ (A : PTm n) B i :
Γ ⊢ A ≡ B ∈ PUniv i -> Γ ⊢ A ≡ B ∈ PUniv i ->
Γ ⊢ A ≲ B Γ ⊢ A ≲ B
| Su_Bind_Proj1 n Γ p (A0 A1 : PTm n) B0 B1 : | Su_Pi_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
Γ ⊢ PBind p A0 B0 ≲ PBind p A1 B1 -> Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
Γ ⊢ A1 ≲ A0 Γ ⊢ A1 ≲ A0
| Su_Bind_Proj2 n Γ p (a0 a1 A0 A1 : PTm n) B0 B1 : | Su_Sig_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
Γ ⊢ PBind p A0 B0 ≲ PBind p A1 B1 -> Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
Γ ⊢ A0 ≲ A1
| Su_Pi_Proj2 n Γ (a0 a1 A0 A1 : PTm n) B0 B1 :
Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
Γ ⊢ a0 ≡ a1 ∈ A1 ->
Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1
| Su_Sig_Proj2 n Γ (a0 a1 A0 A1 : PTm n) B0 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