{-# OPTIONS --without-K --safe #-} open import Level open import Axiom.Extensionality.Propositional -- Semantic judgments for universes module NonCumulative.Completeness.Universe (fext : Extensionality 0ℓ (suc 0ℓ)) where open import Data.Nat.Properties open import Lib open import NonCumulative.Completeness.LogRel open import NonCumulative.Semantics.Properties.PER fext Se-≈′ : ∀ i → ⊨ Γ → ---------------------------------- Γ ⊨ Se i ≈ Se i ∶[ 2 + i ] Se (1 + i) Se-≈′ i ⊨Γ = ⊨Γ , helper where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ → ------------------------------------------------------------ Σ (RelTyp _ (Se (1 + i)) ρ (Se (1 + i)) ρ′) λ rel → RelExp (Se i) ρ (Se i) ρ′ (El _ (RelTyp.T≈T′ rel)) helper ρ≈ρ′ = record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦T′⟧ = ⟦Se⟧ _ ; T≈T′ = U′ } , record { ↘⟦t⟧ = ⟦Se⟧ _ ; ↘⟦t′⟧ = ⟦Se⟧ _ ; t≈t′ = U′ } Se-[]′ : ∀ i → Γ ⊨s σ ∶ Δ → ---------------------------------- Γ ⊨ Se i [ σ ] ≈ Se i ∶[ 2 + i ] Se (1 + i) Se-[]′ {_} {σ} i (⊨Γ , ⊨Δ , ⊨σ) = ⊨Γ , helper where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ → ----------------------------------------------------------------- Σ (RelTyp _ (Se (1 + i)) ρ (Se (1 + i)) ρ′) λ rel → RelExp (Se i [ σ ]) ρ (Se i) ρ′ (El _ (RelTyp.T≈T′ rel)) helper ρ≈ρ′ = record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦T′⟧ = ⟦Se⟧ _ ; T≈T′ = U′ } , record { ↘⟦t⟧ = ⟦[]⟧ ↘⟦σ⟧ (⟦Se⟧ _) ; ↘⟦t′⟧ = ⟦Se⟧ _ ; t≈t′ = U′ } where open RelSubst (⊨σ ρ≈ρ′)