Soundness and Logical Relations

[HuStmpHrrr]

@Ailrun Let's split work in this issue. List and pick stuff that you want to work on so we don't overlap.

• subtyping
  • Prove per escape lemma along gluing #151
  • Prove subtyping case for soundness #153
  • Change system rules #157
• cumulativity
  • Gluing Cumulativity #150
• realizability
  • working on realizability #140
• typing rules
  • Finish soundness of NbE #113 (Roadmap issue)

[Ailrun]

I will first fix #135.

[HuStmpHrrr]

I will look into realizability. subtyping is gonna be interesting. @Ailrun do you want to handle it? or do you want to swap.

[Ailrun]

By subtyping, you mean subtyping cases? I didn't get it when you said subtyping logrel for soundness, as I expected something like
https://gitlab.com/JasonHuZS/practice/-/blob/master/MLTT/Soundness/Terms.agda#L22-26
(that using syntactic judgement) or similar.

[HuStmpHrrr]

there should be lemmas for subtyping in the logical relations too. it should quantify what happens to the logical relation when there is a subtyping in the domain.

[Ailrun]

You mean something like the following?

Lemma glu_univ_elem_typ_subtyping : forall {i a a' P P' El El' Γ A},
    {{ Sub a <: a' at i }} ->
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
    P Γ A ->
    exists A', {{ Γ ⊢ A ⊆ A' }} /\ P' Γ A'.

(This one is not directly provable)

[HuStmpHrrr]

It should be universal over A', but otherwise I think this should be the theorem. Not sure if there's more.

[Ailrun]

How it can be universal in A'? I mean, A' should be a specific type that corresponds to a', not any supertype of A.

[HuStmpHrrr]

put P' Γ A' in the implication too. you just prove A is a subtype of A'.

[Ailrun]

Then what would that provide? For subtyping cases we need if El G M A m then El' G M A' m for some supertype A', and this requires something like above.

[HuStmpHrrr]

this one will also prove the previous lemma as part of it. proving this one should also work.

[Ailrun]

Ah in that sense.

[Ailrun]

It seems like the subtyping lemmas require realizability. In the following lemma,

Lemma glu_univ_elem_typ_per_univ_escape : forall {i a a' P P' El El' Γ A A'},
    {{ Dom a ≈ a' ∈ per_univ i }} ->
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
    {{ Γ ⊢ A ® P }} ->
    {{ Γ ⊢ A' ® P' }} ->
    {{ Γ ⊢ A ≈ A' : Type@i }}.

we need {{{ Γ, IT ⊢ # 0 : IT[Wk] ® ⇑! A 0 ∈ IEl }}} in pi case, which probably is derivable after realizability.

[HuStmpHrrr]

ok i see. every lemma from Agda is proved?