EverythingHome
{-# OPTIONS --without-K --safe #-}

open import Level
open import Axiom.Extensionality.Propositional

-- Semantic judgments for universes
module NonCumulative.Ascribed.Completeness.Universe (fext : Extensionality 0ℓ (suc 0ℓ)) where

open import Data.Nat.Properties

open import Lib
open import NonCumulative.Ascribed.Completeness.LogRel

open import NonCumulative.Ascribed.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 (⊨σ ρ≈ρ′)