{-# OPTIONS --without-K --safe #-}
open import Level
open import Axiom.Extensionality.Propositional
module MLTT.Completeness.Universe (fext : Extensionality 0ℓ (suc 0ℓ)) where
open import Data.Nat.Properties
open import Lib
open import MLTT.Completeness.LogRel
open import MLTT.Semantics.Properties.PER fext
Se-≈′ : ∀ i →
⊨ Γ →
Γ ⊨ Se i ≈ Se 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′ ≤-refl
}
, record
{ ↘⟦t⟧ = ⟦Se⟧ _
; ↘⟦t′⟧ = ⟦Se⟧ _
; t≈t′ = PERDef.U ≤-refl refl
}
Se-[]′ : ∀ i →
Γ ⊨s σ ∶ Δ →
Γ ⊨ Se i [ σ ] ≈ Se 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′ ≤-refl
}
, record
{ ↘⟦t⟧ = ⟦[]⟧ ↘⟦σ⟧ (⟦Se⟧ _)
; ↘⟦t′⟧ = ⟦Se⟧ _
; t≈t′ = PERDef.U ≤-refl refl
}
where open RelSubst (⊨σ ρ≈ρ′)
≈-cumu′ : ∀ {i} →
Γ ⊨ T ≈ T′ ∶ Se i →
Γ ⊨ T ≈ T′ ∶ Se (1 + i)
≈-cumu′ {_} {T} {T′} {i} (⊨Γ , _ , T≈T′) = ⊨Γ , _ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
Σ (RelTyp _ (Se (1 + i)) ρ (Se (1 + i)) ρ′)
λ rel → RelExp T ρ T′ ρ′ (El _ (RelTyp.T≈T′ rel))
helper {ρ} {ρ′} ρ≈ρ′
with T≈T′ ρ≈ρ′
... | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦T′⟧ = ⟦Se⟧ _ ; T≈T′ = U i<j _ }
, record { ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦t′⟧ = ↘⟦t′⟧ ; t≈t′ = t≈t′ }
rewrite 𝕌-wellfounded-≡-𝕌 _ i<j = record
{ ↘⟦T⟧ = ⟦Se⟧ _
; ↘⟦T′⟧ = ⟦Se⟧ _
; T≈T′ = U′ ≤-refl
}
, rel
where rel : RelExp T ρ T′ ρ′ (El (1 + (1 + i)) (U′ ≤-refl))
rel
rewrite 𝕌-wellfounded-≡-𝕌 (1 + (1 + i)) ≤-refl = record
{ ↘⟦t⟧ = ↘⟦t⟧
; ↘⟦t′⟧ = ↘⟦t′⟧
; t≈t′ = 𝕌-cumu-step _ t≈t′
}