{-# OPTIONS --without-K --safe #-}
open import Level
open import Axiom.Extensionality.Propositional
module Cumulative.Completeness.Substitutions (fext : Extensionality 0ℓ (suc 0ℓ)) where
open import Data.Nat.Properties
open import Lib hiding (lookup)
open import Cumulative.Completeness.LogRel
open import Cumulative.Semantics.Properties.PER fext
open import Cumulative.Completeness.Contexts fext
open import Cumulative.Completeness.Terms fext
open import Cumulative.Completeness.Universe fext
I-≈′ : ⊨ Γ →
Γ ⊨s I ≈ I ∶ Γ
I-≈′ ⊨Γ = ⊨Γ , ⊨Γ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
RelSubst I ρ I ρ′ ⟦ ⊨Γ ⟧ρ
helper ρ≈ρ′ = record
{ ↘⟦σ⟧ = ⟦I⟧
; ↘⟦δ⟧ = ⟦I⟧
; σ≈δ = ρ≈ρ′
}
wk-≈′ : ⊨ T ∷ Γ →
T ∷ Γ ⊨s wk ≈ wk ∶ Γ
wk-≈′ {T} ⊨TΓ@(∷-cong ⊨Γ _) = ⊨TΓ , ⊨Γ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨TΓ ⟧ρ →
RelSubst wk ρ wk ρ′ ⟦ ⊨Γ ⟧ρ
helper (ρ≈ρ′ , _) = record
{ ↘⟦σ⟧ = ⟦wk⟧
; ↘⟦δ⟧ = ⟦wk⟧
; σ≈δ = ρ≈ρ′
}
∘-cong′ : Γ ⊨s τ ≈ τ′ ∶ Γ′ →
Γ′ ⊨s σ ≈ σ′ ∶ Γ″ →
Γ ⊨s σ ∘ τ ≈ σ′ ∘ τ′ ∶ Γ″
∘-cong′ {_} {τ} {τ′} {_} {σ} {σ′} (⊨Γ , ⊨Γ′ , τ≈τ′) (⊨Γ′₁ , ⊨Γ″ , σ≈σ′) = ⊨Γ , ⊨Γ″ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
RelSubst (σ ∘ τ) ρ (σ′ ∘ τ′) ρ′ ⟦ ⊨Γ″ ⟧ρ
helper ρ≈ρ′ = record
{ σ
; ↘⟦σ⟧ = ⟦∘⟧ τ.↘⟦σ⟧ σ.↘⟦σ⟧
; ↘⟦δ⟧ = ⟦∘⟧ τ.↘⟦δ⟧ σ.↘⟦δ⟧
}
where module τ = RelSubst (τ≈τ′ ρ≈ρ′)
module σ = RelSubst (σ≈σ′ (⊨-irrel ⊨Γ′ ⊨Γ′₁ τ.σ≈δ))
,-cong′ : ∀ {i} →
Γ ⊨s σ ≈ σ′ ∶ Δ →
Δ ⊨ T ∶ Se i →
Γ ⊨ t ≈ t′ ∶ T [ σ ] →
Γ ⊨s σ , t ≈ σ′ , t′ ∶ T ∷ Δ
,-cong′ {_} {σ} {σ′} {_} {T} {t} {t′} (⊨Γ , ⊨Δ , σ≈σ′) (⊨Δ₁ , i , ⊨T) (⊨Γ₁ , j , t≈t′) = ⊨Γ , ∷-cong ⊨Δ helper , helper′
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Δ ⟧ρ →
RelTyp _ T ρ T ρ′
helper = ∷-cong-helper (⊨Δ₁ , i , ⊨T) ⊨Δ
helper′ : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
RelSubst (σ , t) ρ (σ′ , t′) ρ′ ⟦ ∷-cong ⊨Δ helper ⟧ρ
helper′ {ρ} {ρ′} ρ≈ρ′
with ρ≈ρ′₁ ← ⊨-irrel ⊨Γ ⊨Γ₁ ρ≈ρ′
with σ≈σ′ ρ≈ρ′
| t≈t′ ρ≈ρ′₁
... | record { ⟦σ⟧ = ⟦σ⟧ ; ⟦δ⟧ = ⟦δ⟧ ; ↘⟦σ⟧ = ↘⟦σ⟧ ; ↘⟦δ⟧ = ↘⟦δ⟧ ; σ≈δ = σ≈δ }
| record { ↘⟦T⟧ = ⟦[]⟧ ↘⟦σ⟧′ ↘⟦T⟧ ; T≈T′ = T≈T′ }
, record { ⟦t⟧ = ⟦t⟧ ; ⟦t′⟧ = ⟦t′⟧ ; ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦t′⟧ = ↘⟦t′⟧ ; t≈t′ = t≈t′ }
rewrite ⟦⟧s-det ↘⟦σ⟧′ ↘⟦σ⟧ = record
{ ↘⟦σ⟧ = ⟦,⟧ ↘⟦σ⟧ ↘⟦t⟧
; ↘⟦δ⟧ = ⟦,⟧ ↘⟦δ⟧ ↘⟦t′⟧
; σ≈δ = σ≈δ , t≈t′₁
}
where t≈t′₁ : ⟦t⟧ ≈ ⟦t′⟧ ∈ El _ (RelTyp.T≈T′ (helper σ≈δ))
t≈t′₁
with σ≈δ₂ ← ⊨-irrel ⊨Δ ⊨Δ₁ σ≈δ
with ⊨T σ≈δ₂
... | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦T′⟧ = ⟦Se⟧ _ ; T≈T′ = U j<i _ }
, record { ⟦t⟧ = ⟦t⟧₁ ; ↘⟦t⟧ = ↘⟦t⟧₁ ; t≈t′ = t≈t′₁ }
rewrite 𝕌-wellfounded-≡-𝕌 _ j<i
| ⟦⟧-det ↘⟦t⟧₁ ↘⟦T⟧ = El-one-sided T≈T′ t≈t′₁ t≈t′
I-∘′ : Γ ⊨s σ ∶ Δ →
Γ ⊨s I ∘ σ ≈ σ ∶ Δ
I-∘′ {_} {σ} (⊨Γ , ⊨Δ , ⊨σ) = ⊨Γ , ⊨Δ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
RelSubst (I ∘ σ) ρ σ ρ′ ⟦ ⊨Δ ⟧ρ
helper ρ≈ρ′ = record
{ RelSubst (⊨σ ρ≈ρ′)
; ↘⟦σ⟧ = ⟦∘⟧ ↘⟦σ⟧ ⟦I⟧
}
where open RelSubst (⊨σ ρ≈ρ′)
∘-I′ : Γ ⊨s σ ∶ Δ →
Γ ⊨s σ ∘ I ≈ σ ∶ Δ
∘-I′ {_} {σ} (⊨Γ , ⊨Δ , ⊨σ) = ⊨Γ , ⊨Δ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
RelSubst (σ ∘ I) ρ σ ρ′ ⟦ ⊨Δ ⟧ρ
helper ρ≈ρ′ = record
{ RelSubst (⊨σ ρ≈ρ′)
; ↘⟦σ⟧ = ⟦∘⟧ ⟦I⟧ ↘⟦σ⟧
}
where open RelSubst (⊨σ ρ≈ρ′)
∘-assoc′ : ∀ {Γ‴} →
Γ′ ⊨s σ ∶ Γ →
Γ″ ⊨s σ′ ∶ Γ′ →
Γ‴ ⊨s σ″ ∶ Γ″ →
Γ‴ ⊨s σ ∘ σ′ ∘ σ″ ≈ σ ∘ (σ′ ∘ σ″) ∶ Γ
∘-assoc′ {_} {σ} {_} {_} {σ′} {σ″} (⊨Γ′ , ⊨Γ , ⊨σ) (⊨Γ″ , ⊨Γ′₁ , ⊨σ′) (⊨Γ‴ , ⊨Γ″₁ , ⊨σ″) = ⊨Γ‴ , ⊨Γ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ‴ ⟧ρ →
RelSubst (σ ∘ σ′ ∘ σ″) ρ (σ ∘ (σ′ ∘ σ″)) ρ′ ⟦ ⊨Γ ⟧ρ
helper ρ≈ρ′ = record
{ σ
; ↘⟦σ⟧ = ⟦∘⟧ σ″.↘⟦σ⟧ (⟦∘⟧ σ′.↘⟦σ⟧ σ.↘⟦σ⟧)
; ↘⟦δ⟧ = ⟦∘⟧ (⟦∘⟧ σ″.↘⟦δ⟧ σ′.↘⟦δ⟧) σ.↘⟦δ⟧
}
where module σ″ = RelSubst (⊨σ″ ρ≈ρ′)
module σ′ = RelSubst (⊨σ′ (⊨-irrel ⊨Γ″₁ ⊨Γ″ σ″.σ≈δ))
module σ = RelSubst (⊨σ (⊨-irrel ⊨Γ′₁ ⊨Γ′ σ′.σ≈δ))
,-∘′ : ∀ {i} →
Γ′ ⊨s σ ∶ Γ″ →
Γ″ ⊨ T ∶ Se i →
Γ′ ⊨ t ∶ T [ σ ] →
Γ ⊨s τ ∶ Γ′ →
Γ ⊨s (σ , t) ∘ τ ≈ (σ ∘ τ) , t [ τ ] ∶ T ∷ Γ″
,-∘′ {_} {σ} {_} {T} {t} {_} {τ} (⊨Γ′ , ⊨Γ″ , ⊨σ) (⊨Γ″₁ , i , ⊨T) (⊨Γ′₁ , j , ⊨t) (⊨Γ , ⊨Γ′₂ , ⊨τ) = ⊨Γ , ∷-cong ⊨Γ″ helper , helper″
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ″ ⟧ρ →
RelTyp _ T ρ T ρ′
helper = ∷-cong-helper (⊨Γ″₁ , i , ⊨T) ⊨Γ″
helper′ : ∀ {i} →
(A≈B : A ≈ B ∈ 𝕌 i) →
a ≈ b ∈ El i A≈B →
(ρ≈ρ′ : ρ ≈ ρ′ ∈ ⟦ ⊨Γ″ ⟧ρ) →
⟦ T ⟧ ρ ↘ A →
a ≈ b ∈ El _ (RelTyp.T≈T′ (helper ρ≈ρ′))
helper′ {i = i} A≈B a≈b ρ≈ρ′ ↘A
with ρ≈ρ′₁ ← ⊨-irrel ⊨Γ″ ⊨Γ″₁ ρ≈ρ′
with ⊨T ρ≈ρ′₁
... | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦T′⟧ = ⟦Se⟧ _ ; T≈T′ = U j<i _ }
, record { ⟦t⟧ = ⟦T⟧ ; ↘⟦t⟧ = ↘⟦t⟧ ; t≈t′ = T≈T′₁ }
rewrite 𝕌-wellfounded-≡-𝕌 _ j<i
| ⟦⟧-det ↘A ↘⟦t⟧ = El-one-sided A≈B T≈T′₁ a≈b
helper″ : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
RelSubst ((σ , t) ∘ τ) ρ ((σ ∘ τ) , t [ τ ]) ρ′ ⟦ ∷-cong ⊨Γ″ helper ⟧ρ
helper″ {ρ} {ρ′} ρ≈ρ′
with record { ↘⟦σ⟧ = ↘⟦σ⟧ ; ↘⟦δ⟧ = ↘⟦δ⟧ ; σ≈δ = σ≈δ } ← ⊨τ ρ≈ρ′
with ⊨t (⊨-irrel ⊨Γ′₂ ⊨Γ′₁ σ≈δ) | ⊨σ (⊨-irrel ⊨Γ′₂ ⊨Γ′ σ≈δ)
... | record { ↘⟦T⟧ = ⟦[]⟧ ↘⟦σ⟧′ ↘⟦T⟧ ; T≈T′ = T≈T′ }
, record { ⟦t⟧ = ⟦t⟧ ; ⟦t′⟧ = ⟦t′⟧ ; ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦t′⟧ = ↘⟦t′⟧ ; t≈t′ = t≈t′ }
| record { ↘⟦σ⟧ = ↘⟦σ⟧₁ ; ↘⟦δ⟧ = ↘⟦δ⟧₁ ; σ≈δ = σ≈δ₁ }
rewrite ⟦⟧s-det ↘⟦σ⟧′ ↘⟦σ⟧₁ = record
{ ↘⟦σ⟧ = ⟦∘⟧ ↘⟦σ⟧ (⟦,⟧ ↘⟦σ⟧₁ ↘⟦t⟧)
; ↘⟦δ⟧ = ⟦,⟧ (⟦∘⟧ ↘⟦δ⟧ ↘⟦δ⟧₁) (⟦[]⟧ ↘⟦δ⟧ ↘⟦t′⟧)
; σ≈δ = σ≈δ₁ , t≈t′₁
}
where t≈t′₁ : ⟦t⟧ ≈ ⟦t′⟧ ∈ El _ (RelTyp.T≈T′ (helper σ≈δ₁))
t≈t′₁ = helper′ T≈T′ t≈t′ σ≈δ₁ ↘⟦T⟧
p-,′ : Γ′ ⊨s σ ∶ Γ →
Γ′ ⊨ t ∶ T [ σ ] →
Γ′ ⊨s p (σ , t) ≈ σ ∶ Γ
p-,′ {_} {σ} {_} {t} {T} (⊨Γ′ , ⊨Γ , ⊨σ) (⊨Γ′₁ , _ , ⊨t) = ⊨Γ′ , ⊨Γ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ′ ⟧ρ →
RelSubst (p (σ , t)) ρ σ ρ′ ⟦ ⊨Γ ⟧ρ
helper {ρ} {ρ′} ρ≈ρ′ = help
where module σ = RelSubst (⊨σ ρ≈ρ′)
help : RelSubst (p (σ , t)) ρ σ ρ′ ⟦ ⊨Γ ⟧ρ
help
with ⊨t (⊨-irrel ⊨Γ′ ⊨Γ′₁ ρ≈ρ′)
... | record { ↘⟦T⟧ = ⟦[]⟧ ↘⟦σ⟧ ↘⟦T⟧ ; ↘⟦T′⟧ = ⟦[]⟧ ↘⟦σ⟧′ ↘⟦T′⟧ }
, re
rewrite ⟦⟧s-det ↘⟦σ⟧ σ.↘⟦σ⟧
| ⟦⟧s-det ↘⟦σ⟧′ σ.↘⟦δ⟧ = record
{ σ
; ⟦σ⟧ = drop (σ.⟦σ⟧ ↦ re.⟦t⟧)
; ↘⟦σ⟧ = ⟦∘⟧ (⟦,⟧ σ.↘⟦σ⟧ re.↘⟦t⟧) ⟦wk⟧
; σ≈δ = σ.σ≈δ
}
where module re = RelExp re
,-ext′ : Γ′ ⊨s σ ∶ T ∷ Γ →
Γ′ ⊨s σ ≈ p σ , v 0 [ σ ] ∶ T ∷ Γ
,-ext′ {_} {σ} {T} (⊨Γ′ , ⊨TΓ@(∷-cong _ _) , ⊨σ) = ⊨Γ′ , ⊨TΓ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ′ ⟧ρ →
RelSubst σ ρ (p σ , v 0 [ σ ]) ρ′ ⟦ ⊨TΓ ⟧ρ
helper ρ≈ρ′ = record
{ RelSubst (⊨σ ρ≈ρ′)
; ⟦δ⟧ = drop ⟦δ⟧ ↦ lookup ⟦δ⟧ 0
; ↘⟦δ⟧ = ⟦,⟧ (⟦∘⟧ ↘⟦δ⟧ ⟦wk⟧) (⟦[]⟧ ↘⟦δ⟧ (⟦v⟧ 0))
; σ≈δ = σ≈δ
}
where open RelSubst (⊨σ ρ≈ρ′)
s-≈-sym′ : Γ ⊨s σ ≈ σ′ ∶ Δ →
Γ ⊨s σ′ ≈ σ ∶ Δ
s-≈-sym′ {_} {σ} {σ′} (⊨Γ , ⊨Δ , σ≈σ′) = ⊨Γ , ⊨Δ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
RelSubst σ′ ρ σ ρ′ ⟦ ⊨Δ ⟧ρ
helper ρ≈ρ′ = record
{ ↘⟦σ⟧ = ↘⟦δ⟧
; ↘⟦δ⟧ = ↘⟦σ⟧
; σ≈δ = ⟦⟧ρ-sym ⊨Δ ⊨Δ σ≈δ
}
where open RelSubst (σ≈σ′ (⟦⟧ρ-sym ⊨Γ ⊨Γ ρ≈ρ′))
s-≈-trans′ : Γ ⊨s σ ≈ σ′ ∶ Δ →
Γ ⊨s σ′ ≈ σ″ ∶ Δ →
Γ ⊨s σ ≈ σ″ ∶ Δ
s-≈-trans′ {_} {σ} {σ′} {_} {σ″} (⊨Γ , ⊨Δ , σ≈σ′) (⊨Γ′ , ⊨Δ′ , σ′≈σ″) = ⊨Γ , ⊨Δ′ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
RelSubst σ ρ σ″ ρ′ ⟦ ⊨Δ′ ⟧ρ
helper ρ≈ρ′
with σ≈σ′ (⟦⟧ρ-refl ⊨Γ ⊨Γ ρ≈ρ′) | σ′≈σ″ (⊨-irrel ⊨Γ ⊨Γ′ ρ≈ρ′)
... | record { ↘⟦σ⟧ = ↘⟦σ⟧ ; ↘⟦δ⟧ = ↘⟦σ′⟧ ; σ≈δ = σ≈σ′ }
| record { ↘⟦σ⟧ = ↘⟦σ′⟧′ ; ↘⟦δ⟧ = ↘⟦σ″⟧ ; σ≈δ = σ′≈σ″ }
rewrite ⟦⟧s-det ↘⟦σ′⟧ ↘⟦σ′⟧′ = record
{ ↘⟦σ⟧ = ↘⟦σ⟧
; ↘⟦δ⟧ = ↘⟦σ″⟧
; σ≈δ = ⟦⟧ρ-trans ⊨Δ ⊨Δ′ ⊨Δ′ σ≈σ′ σ′≈σ″
}
s-≈-conv′ : Γ ⊨s σ ≈ σ′ ∶ Δ →
⊨ Δ ≈ Δ′ →
Γ ⊨s σ ≈ σ′ ∶ Δ′
s-≈-conv′ {_} {σ} {σ′} (⊨Γ , ⊨Δ , σ≈σ′) Δ≈Δ′ = ⊨Γ , ⊨Δ′ , helper
where ⊨Δ′ = ⊨-refl (⊨-sym Δ≈Δ′)
helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
RelSubst σ ρ σ′ ρ′ ⟦ ⊨Δ′ ⟧ρ
helper ρ≈ρ′ = record
{ RelSubst (σ≈σ′ ρ≈ρ′)
; σ≈δ = ⟦⟧ρ-transport ⊨Δ ⊨Δ′ σ≈δ Δ≈Δ′
}
where open RelSubst (σ≈σ′ ρ≈ρ′)