{-# OPTIONS --without-K --safe #-} open import Level open import Axiom.Extensionality.Propositional -- Going from the gluing model to the syntax module Cumulative.Soundness.ToSyntax (fext : Extensionality 0ℓ (suc 0ℓ)) where open import Lib open import Cumulative.Statics.Properties as Sta open import Cumulative.Semantics.Properties.PER fext open import Cumulative.Completeness.Fundamental fext open import Cumulative.Soundness.LogRel open import Cumulative.Soundness.Properties.LogRel fext open import Cumulative.Soundness.Properties.Substitutions fext ⊩⇒⊢-both : (⊩t : Γ ⊩ t ∶ T) → ---------------------- Γ ⊢ T ∶ Se (_⊩_∶_.lvl ⊩t) × Γ ⊢ t ∶ T ⊩⇒⊢-both ⊩t with InitEnvs-related (fundamental-⊢Γ (⊩⇒⊢ (_⊩_∶_.⊩Γ ⊩t))) ... | _ , _ , ρ∈ , _ = ⊢T , conv ([I]-inv (®El⇒tm T∈𝕌 t∼⟦t⟧)) ([I] ⊢T) where open _⊩_∶_ ⊩t open GluExp (krip (InitEnvs⇒s®I ⊩Γ ρ∈)) ⊢T = [I]-inv (®El⇒ty T∈𝕌 t∼⟦t⟧) ⊩⇒⊢-tm : Γ ⊩ t ∶ T → ------------ Γ ⊢ t ∶ T ⊩⇒⊢-tm ⊩t = proj₂ (⊩⇒⊢-both ⊩t) ⊩⇒⊢-ty : (⊩t : Γ ⊩ t ∶ T) → ------------ Γ ⊢ T ∶ Se (_⊩_∶_.lvl ⊩t) ⊩⇒⊢-ty ⊩t = proj₁ (⊩⇒⊢-both ⊩t) ⊩s⇒⊢s : Γ ⊩s σ ∶ Δ → ------------ Γ ⊢s σ ∶ Δ ⊩s⇒⊢s ⊩σ with InitEnvs-related (fundamental-⊢Γ (⊩⇒⊢ (_⊩s_∶_.⊩Γ ⊩σ))) ... | _ , _ , ρ∈ , _ = ∘I-inv′ (s®⇒⊢s ⊩Γ′ τσ∼⟦τ⟧) where open _⊩s_∶_ ⊩σ open GluSubst (krip (InitEnvs⇒s®I ⊩Γ ρ∈))