## Stream: MetaCoq

### Topic: Changing global universes in typing

#### Jason Gross (Dec 06 2022 at 19:39):

Suppose I want to prove `wf_ext Σ -> wf_ext (Σ.1, X) -> (Σ.1, X);;; Γ |- t1 : T -> Σ;;; Γ |- t1 : T`. Is there a lemma that proves something like this? And what's the relationship I need between `X` and `Σ.2`?

#### Matthieu Sozeau (Dec 06 2022 at 19:58):

If X is monomorphic, then this holds, otherwise you need the universe instantiation lemma

#### Jason Gross (Dec 06 2022 at 20:03):

What's the universe instantiation lemma? / where is it?

#### Jason Gross (Dec 06 2022 at 20:04):

(What I have is that `X` is equal to the `cst_universes` of some `ConstantDecl` in `Σ.2`)

#### Jason Gross (Dec 06 2022 at 22:04):

Hm, it seems that all the lemmas in PCUICWeakeningEnvTyp that are close to what I want have the implication in the wrong direction. I want to show that if normalisation holds in Σ, then normalisation will still hold after replacing the universe context of Σ with the universe context from some declaration in Σ. I guess this is actually a kind-of tricky lemma, because we can't just port the typing judgment.

#### Matthieu Sozeau (Dec 07 2022 at 16:46):

The theorem's in PCUICUnivSubstitutionTyp. In the case X is a universe polymorphic extension, then Gamma, t1 and T might depend on universes that would become free in Sigma, so you'll need to find an instantiation for those, in the original \Sigma. Maybe you should rather work with an `empty_ext \Sigma` rather than an arbitrary extension

#### Jason Gross (Dec 07 2022 at 22:39):

Maybe you should rather work with an empty_ext \Sigma rather than an arbitrary extension

This is unfortunately not a freedom I have. Erasure needs to know that normalisation holds in the context of the universes of every polymorphic definition in the global environment. It would be nice if knowing that normalisation holds in the global environment is enough to know that normalisation holds in the context of every constant defined in that environment. So I need to prove something like

``````∀ ϕ,
(exists kn cb, lookup_env Σ kn = Some (ConstantDecl cb) /\ cst_universes cb = ϕ)
→ wf_ext (Σ, Monomorphic_ctx)
→ wf_ext (Σ, ϕ)
→ (∀ Γ t T, ((Σ, Monomorphic_ctx) ;;; Γ |- t : T) → Acc (cored Σ Γ) t)
→ (∀ Γ t T, ((Σ, ϕ) ;;; Γ |- t : T) → Acc (cored Σ Γ) t)
``````

So I was hoping that I could just reuse the same term and prove that `((Σ, ϕ) ;;; Γ |- t : T) → ((Σ, Monomorphic_ctx) ;;; Γ |- t : T) `, but it seems like this is not the case. Instead I need to find some instantiation of the universes in `ϕ` that is consistent with the given typing derivation (is there an easy way to find such? is there a lemma already for this?), perform the substitution (importantly it must be a no-op on `Σ`), and then translate the `cored` proof across the substitution so that I can recover `Acc`. Does this sound right?

Last updated: Feb 04 2023 at 01:03 UTC