{-# OPTIONS --without-K --safe #-}
module MLTT.Soundness.LogRel where
open import Lib hiding (lookup)
open import Data.Nat
open import Data.Nat.Properties
open import MLTT.Statics public
open import MLTT.Semantics.Domain public
open import MLTT.Semantics.Evaluation public
open import MLTT.Semantics.PER public
open import MLTT.Soundness.Weakening public
infix 4 _⊢_∶N®_∈Nat
data _⊢_∶N®_∈Nat : Ctx → Exp → D → Set where
ze : Γ ⊢ t ≈ ze ∶ N →
Γ ⊢ t ∶N® ze ∈Nat
su : Γ ⊢ t ≈ su t′ ∶ N →
Γ ⊢ t′ ∶N® a ∈Nat →
Γ ⊢ t ∶N® su a ∈Nat
ne : (c∈ : c ∈′ Bot) →
(∀ {Δ σ} → Δ ⊢w σ ∶ Γ → let (u , _) = c∈ (len Δ) in Δ ⊢ t [ σ ] ≈ Ne⇒Exp u ∶ N) →
Γ ⊢ t ∶N® ↑ A c ∈Nat
pattern ne′ c∈ krip = ne {A = N} c∈ krip
record ΠRel i Δ IT OT (σ : Subst)
(iA : A ≈ B ∈ 𝕌 i)
(RI : Ctx → Typ → Set)
(RO : ∀ {a a′} → a ≈ a′ ∈ El i iA → Ctx → Typ → Set)
(Rs : Ctx → Exp → Typ → D → Set) : Set where
field
IT-rel : RI Δ (IT [ σ ])
OT-rel : Rs Δ s (IT [ σ ]) a → (a∈ : a ∈′ El i iA) → RO a∈ Δ (OT [ σ , s ])
record GluΠ i Γ T {A B}
(iA : A ≈ B ∈ 𝕌 i)
(RI : Ctx → Typ → Set)
(RO : ∀ {a a′} → a ≈ a′ ∈ El i iA → Ctx → Typ → Set)
(Rs : Ctx → Exp → Typ → D → Set) : Set where
field
IT : Typ
OT : Typ
⊢OT : IT ∷ Γ ⊢ OT ∶ Se i
T≈ : Γ ⊢ T ≈ Π IT OT ∶ Se i
krip : Δ ⊢w σ ∶ Γ → ΠRel i Δ IT OT σ iA RI RO Rs
record ΛKripke Δ t T f a (R$ : Ctx → Exp → Typ → D → Set) : Set where
field
fa : D
↘fa : f ∙ a ↘ fa
®fa : R$ Δ t T fa
record ΛRel i Δ t IT OT (σ : Subst ) f
(iA : A ≈ B ∈ 𝕌 i)
(RI : Ctx → Typ → Set)
(Rs : Ctx → Exp → Typ → D → Set)
(R$ : ∀ {a a′} → a ≈ a′ ∈ El i iA → Ctx → Exp → Typ → D → Set) : Set where
field
IT-rel : RI Δ (IT [ σ ])
ap-rel : Rs Δ s (IT [ σ ]) b → (b∈ : b ∈′ El i iA) → ΛKripke Δ (t [ σ ] $ s) (OT [ σ , s ]) f b (R$ b∈)
flipped-ap-rel : (b∈ : b ∈′ El i iA) → ∀ {s} → Rs Δ s (IT [ σ ]) b → ΛKripke Δ (t [ σ ] $ s) (OT [ σ , s ]) f b (R$ b∈)
flipped-ap-rel b∈ R = ap-rel R b∈
record GluΛ i Γ t T a {A B T′ T″ ρ ρ′}
(iA : A ≈ B ∈ 𝕌 i)
(RT : ∀ {a a′} → a ≈ a′ ∈ El i iA → ΠRT T′ (ρ ↦ a) T″ (ρ′ ↦ a′) (𝕌 i))
(RI : Ctx → Typ → Set)
(Rs : Ctx → Exp → Typ → D → Set)
(R$ : ∀ {a a′} → a ≈ a′ ∈ El i iA → Ctx → Exp → Typ → D → Set) : Set where
field
t∶T : Γ ⊢ t ∶ T
a∈El : a ∈′ El i (Π iA RT)
IT : Typ
OT : Typ
⊢OT : IT ∷ Γ ⊢ OT ∶ Se i
T≈ : Γ ⊢ T ≈ Π IT OT ∶ Se i
krip : Δ ⊢w σ ∶ Γ → ΛRel i Δ t IT OT σ a iA RI Rs R$
record GluU j i Γ t T A (R : A ∈′ 𝕌 j → Set) : Set where
field
t∶T : Γ ⊢ t ∶ T
T≈ : Γ ⊢ T ≈ Se j ∶ Se i
A∈𝕌 : A ∈′ 𝕌 j
rel : R A∈𝕌
record GluNe i Γ t T (c∈⊥ : c ∈′ Bot) (C≈C′ : C ≈ C′ ∈ Bot) : Set where
field
t∶T : Γ ⊢ t ∶ T
⊢T : Γ ⊢ T ∶ Se i
krip : Δ ⊢w σ ∶ Γ →
let V , _ = C≈C′ (len Δ)
u , _ = c∈⊥ (len Δ)
in Δ ⊢ T [ σ ] ≈ Ne⇒Exp V ∶ Se i
× Δ ⊢ t [ σ ] ≈ Ne⇒Exp u ∶ T [ σ ]
module Glu i (rec : ∀ {j} → j < i → ∀ {A B} → Ctx → Typ → A ≈ B ∈ 𝕌 j → Set) where
infix 4 _⊢_®_ _⊢_∶_®_∈El_
mutual
_⊢_®_ : Ctx → Typ → A ≈ B ∈ 𝕌 i → Set
Γ ⊢ T ® ne C≈C′ = Γ ⊢ T ∶ Se i × ∀ {Δ σ} → Δ ⊢w σ ∶ Γ → let V , _ = C≈C′ (len Δ) in Δ ⊢ T [ σ ] ≈ Ne⇒Exp V ∶ Se i
Γ ⊢ T ® N = Γ ⊢ T ≈ N ∶ Se i
Γ ⊢ T ® U {j} j<i eq = Γ ⊢ T ≈ Se j ∶ Se i
Γ ⊢ T ® Π iA RT = GluΠ i Γ T iA (_⊢_® iA) (λ a∈ → _⊢_® ΠRT.T≈T′ (RT a∈)) (_⊢_∶_®_∈El iA)
_⊢_∶_®_∈El_ : Ctx → Exp → Typ → D → A ≈ B ∈ 𝕌 i → Set
Γ ⊢ t ∶ T ® a ∈El ne C≈C′ = Σ (a ∈′ Neu) λ { (ne c∈⊥) → GluNe i Γ t T c∈⊥ C≈C′ }
Γ ⊢ t ∶ T ® a ∈El N = Γ ⊢ t ∶N® a ∈Nat × Γ ⊢ T ≈ N ∶ Se i
Γ ⊢ t ∶ T ® a ∈El U {j} j<i eq = GluU j i Γ t T a (rec j<i Γ t)
Γ ⊢ t ∶ T ® a ∈El Π iA RT = GluΛ i Γ t T a iA RT (_⊢_® iA) (_⊢_∶_®_∈El iA) (λ b∈ → _⊢_∶_®_∈El ΠRT.T≈T′ (RT b∈))
Glu-wellfounded : ∀ i {j} → j < i → ∀ {A B} → Ctx → Typ → A ≈ B ∈ 𝕌 j → Set
Glu-wellfounded .(suc _) {j} (s≤s j<i) = Glu._⊢_®_ j λ j′<j → Glu-wellfounded _ (≤-trans j′<j j<i)
private
module G i = Glu i (Glu-wellfounded i)
infix 4 _⊢_®[_]_ _⊢_∶_®[_]_∈El_
_⊢_®[_]_ : Ctx → Typ → ∀ i → A ≈ B ∈ 𝕌 i → Set
Γ ⊢ T ®[ i ] A≈B = G._⊢_®_ i Γ T A≈B
_⊢_∶_®[_]_∈El_ : Ctx → Exp → Typ → ∀ i → D → A ≈ B ∈ 𝕌 i → Set
Γ ⊢ t ∶ T ®[ i ] a ∈El A≈B = G._⊢_∶_®_∈El_ i Γ t T a A≈B
infix 4 _⊢_∶_®↓[_]_∈El_ _⊢_∶_®↑[_]_∈El_ _⊢_®↑[_]_
record _⊢_∶_®↓[_]_∈El_ Γ t T i c (A≈B : A ≈ B ∈ 𝕌 i) : Set where
field
t∶T : Γ ⊢ t ∶ T
T∼A : Γ ⊢ T ®[ i ] A≈B
c∈⊥ : c ∈′ Bot
krip : Δ ⊢w σ ∶ Γ → let u , _ = c∈⊥ (len Δ) in Δ ⊢ t [ σ ] ≈ Ne⇒Exp u ∶ T [ σ ]
record _⊢_∶_®↑[_]_∈El_ Γ t T i a (A≈B : A ≈ B ∈ 𝕌 i) : Set where
field
t∶T : Γ ⊢ t ∶ T
T∼A : Γ ⊢ T ®[ i ] A≈B
a∈⊤ : ↓ A a ≈ ↓ B a ∈ Top
krip : Δ ⊢w σ ∶ Γ → let w , _ = a∈⊤ (len Δ) in Δ ⊢ t [ σ ] ≈ Nf⇒Exp w ∶ T [ σ ]
record _⊢_®↑[_]_ Γ T i (A≈B : A ≈ B ∈ 𝕌 i) : Set where
field
t∶T : Γ ⊢ T ∶ Se i
A∈⊤ : A ≈ B ∈ TopT
krip : Δ ⊢w σ ∶ Γ → let W , _ = A∈⊤ (len Δ) in Δ ⊢ T [ σ ] ≈ Nf⇒Exp W ∶ Se i
record Glu∷ i Γ σ T Δ (ρ : Env) (R : Ctx → Subst → Env → Set) : Set where
field
⊢σ : Γ ⊢s σ ∶ T ∷ Δ
pσ : Subst
v0σ : Exp
⟦T⟧ : D
≈pσ : Γ ⊢s p σ ≈ pσ ∶ Δ
≈v0σ : Γ ⊢ v 0 [ σ ] ≈ v0σ ∶ T [ pσ ]
↘⟦T⟧ : ⟦ T ⟧ drop ρ ↘ ⟦T⟧
T∈𝕌 : ⟦T⟧ ∈′ 𝕌 i
t∼ρ0 : Γ ⊢ v0σ ∶ (T [ pσ ]) ®[ i ] (lookup ρ 0) ∈El T∈𝕌
step : R Γ pσ (drop ρ)
record GluTyp i Δ T (σ : Subst) ρ : Set where
field
⟦T⟧ : D
↘⟦T⟧ : ⟦ T ⟧ ρ ↘ ⟦T⟧
T∈𝕌 : ⟦T⟧ ∈′ 𝕌 i
T∼⟦T⟧ : Δ ⊢ T [ σ ] ®[ i ] T∈𝕌
infix 4 ⊩_ _⊢s_∶_®_
mutual
data ⊩_ : Ctx → Set where
⊩[] : ⊩ []
⊩∷ : ∀ {i} (⊩Γ : ⊩ Γ) →
Γ ⊢ T ∶ Se i →
(∀ {Δ σ ρ} → Δ ⊢s σ ∶ ⊩Γ ® ρ → GluTyp i Δ T σ ρ) →
⊩ (T ∷ Γ)
_⊢s_∶_®_ : Ctx → Subst → ⊩ Δ → Env → Set
Δ ⊢s σ ∶ ⊩[] ® ρ = Δ ⊢s σ ∶ []
Δ ⊢s σ ∶ ⊩∷ {Γ} {T} {i} ⊩Γ ⊢T gT ® ρ = Glu∷ i Δ σ T Γ ρ (_⊢s_∶ ⊩Γ ®_)
⊩⇒⊢ : ⊩ Γ → ⊢ Γ
⊩⇒⊢ ⊩[] = ⊢[]
⊩⇒⊢ (⊩∷ ⊩Γ ⊢T _) = ⊢∷ (⊩⇒⊢ ⊩Γ) ⊢T
record GluExp i Δ t T (σ : Subst) ρ : Set where
field
⟦T⟧ : D
⟦t⟧ : D
↘⟦T⟧ : ⟦ T ⟧ ρ ↘ ⟦T⟧
↘⟦t⟧ : ⟦ t ⟧ ρ ↘ ⟦t⟧
T∈𝕌 : ⟦T⟧ ∈′ 𝕌 i
t∼⟦t⟧ : Δ ⊢ t [ σ ] ∶ T [ σ ] ®[ i ] ⟦t⟧ ∈El T∈𝕌
record GluSubst Δ τ (⊩Γ′ : ⊩ Γ′) σ ρ : Set where
field
⟦τ⟧ : Env
↘⟦τ⟧ : ⟦ τ ⟧s ρ ↘ ⟦τ⟧
τσ∼⟦τ⟧ : Δ ⊢s τ ∘ σ ∶ ⊩Γ′ ® ⟦τ⟧
infix 4 _⊩_∶_ _⊩s_∶_
record _⊩_∶_ Γ t T : Set where
field
⊩Γ : ⊩ Γ
lvl : ℕ
krip : Δ ⊢s σ ∶ ⊩Γ ® ρ → GluExp lvl Δ t T σ ρ
record _⊩s_∶_ Γ τ Γ′ : Set where
field
⊩Γ : ⊩ Γ
⊩Γ′ : ⊩ Γ′
krip : Δ ⊢s σ ∶ ⊩Γ ® ρ → GluSubst Δ τ ⊩Γ′ σ ρ