{-# OPTIONS --without-K --safe #-}
open import Level
open import Axiom.Extensionality.Propositional
module Cumulative.Consequences (fext : Extensionality 0ℓ (suc 0ℓ)) where
open import Lib
open import Cumulative.Statics.Properties
open import Cumulative.Semantics.PER
open import Cumulative.Semantics.Readback
open import Cumulative.Semantics.Properties.PER fext
open import Cumulative.Semantics.Realizability fext
open import Cumulative.Completeness fext
open import Cumulative.Completeness.LogRel
open import Cumulative.Completeness.Fundamental fext
open import Cumulative.Completeness.Consequences fext
open import Cumulative.Soundness fext
open import Cumulative.Soundness.LogRel
open import Cumulative.Soundness.Properties.LogRel fext
open import Cumulative.Soundness.Properties.Substitutions fext
open import Cumulative.Soundness.Cumulativity fext
open import Cumulative.Soundness.Realizability fext
open import Cumulative.Soundness.Fundamental fext
Π-≈-inj : ∀ {i} →
Γ ⊢ Π S T ≈ Π S′ T′ ∶ Se i →
Γ ⊢ S ≈ S′ ∶ Se i × S ∷ Γ ⊢ T ≈ T′ ∶ Se i
Π-≈-inj {Γ} {S} {T} {S′} {T′} {i} Π≈
with ⊢Γ , ⊢ΠST , ⊢ΠS′T′ , _ ← presup-≈ Π≈
with ⊢S , ⊢T ← Π-inv ⊢ΠST
| ⊢S′ , ⊢T′ ← Π-inv ⊢ΠS′T′
with ⊨Γ , _ , rel ← fundamental-t≈t′ Π≈
| ⊨SΓ₁@(∷-cong ⊨Γ₁ Srel₁) , _ , rel₁ ← fundamental-⊢t ⊢T
| record { ⊩Γ = ⊩Γ ; krip = Skrip } ← fundamental-⊢t⇒⊩t ⊢S
| record { ⊩Γ = ⊩Γ₁ ; krip = S′krip } ← fundamental-⊢t⇒⊩t ⊢S′
with ρ′ , _ , ρ′init , ρ′init₁ , ρ′∈ ← InitEnvs-related ⊨SΓ₁
rewrite InitEnvs-det ρ′init₁ ρ′init
with s-∷ {ρ = ρ} {A = A} ρinit S↘ ← ρ′init
| ρ∈ , s∈ ← ρ′∈
with rel (⊨-irrel ⊨Γ₁ ⊨Γ ρ∈)
| Skrip (InitEnvs⇒s®I ⊩Γ ρinit)
| S′krip (InitEnvs⇒s®I ⊩Γ₁ ρinit)
... | record { ↘⟦T⟧ = ⟦Se⟧ _ ; T≈T′ = U i< _ }
, record { ⟦t⟧ = Π ⟦S⟧ _ _ ; ⟦t′⟧ = Π ⟦S′⟧ _ _ ; ↘⟦t⟧ = ⟦Π⟧ ↘⟦S⟧ ; ↘⟦t′⟧ = ⟦Π⟧ ↘⟦S′⟧ ; t≈t′ = ΠST≈ΠS′T′ }
| record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦t⟧ = ↘⟦S⟧′ ; T∈𝕌 = U i<′ _ ; t∼⟦t⟧ = S∼⟦S⟧ }
| record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦t⟧ = ↘⟦S′⟧′ ; T∈𝕌 = U i<′₁ _ ; t∼⟦t⟧ = S′∼⟦S′⟧ }
rewrite 𝕌-wellfounded-≡-𝕌 _ i<
| Glu-wellfounded-≡ i<′
| Glu-wellfounded-≡ i<′₁
| ⟦⟧-det ↘⟦S⟧′ ↘⟦S⟧
| ⟦⟧-det ↘⟦S′⟧′ ↘⟦S′⟧
with Π S≈S′ Trel ← ΠST≈ΠS′T′
| record { A∈𝕌 = S∈𝕌 ; rel = Srel } ← S∼⟦S⟧
| record { A∈𝕌 = S′∈𝕌 ; rel = S′rel } ← S′∼⟦S′⟧
with S≈S′′ ← ≈-sym ([I]-≈ˡ-Se (≈-sym ([I]-≈ˡ-Se (®⇒≈ S′∈𝕌 (®-transport S∈𝕌 S′∈𝕌 S≈S′ Srel) S′rel)))) = S≈S′′ , T≈T′-helper
where
s∈₁ : l′ A (len Γ) ∈′ El _ S≈S′
s∈₁
with record { ↘⟦T⟧ = ↘⟦S⟧₁ ; ↘⟦T′⟧ = ↘⟦S′⟧₁ ; T≈T′ = S≈S′₁ } ← Srel₁ ρ∈
rewrite ⟦⟧-det ↘⟦S⟧₁ ↘⟦S⟧ = El-one-sided S≈S′₁ S≈S′ s∈
T≈T′-helper : S ∷ Γ ⊢ T ≈ T′ ∶ Se i
T≈T′-helper
with record { ⊩Γ = ⊩SΓ ; krip = Tkrip } ← fundamental-⊢t⇒⊩t ⊢T
| record { ⊩Γ = ⊩SΓ₁ ; krip = T′krip } ← fundamental-⊢t⇒⊩t (ctxeq-tm (∷-cong (⊢≈-refl ⊢Γ) (≈-sym S≈S′′)) ⊢T′)
with record { ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ } ← Trel s∈₁
| record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦t⟧ = ↘⟦T⟧′ ; T∈𝕌 = U i<′ _ ; t∼⟦t⟧ = T∼⟦T⟧ } ← Tkrip (InitEnvs⇒s®I ⊩SΓ ρ′init)
| record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦t⟧ = ↘⟦T′⟧′ ; T∈𝕌 = U i<′₁ _ ; t∼⟦t⟧ = T′∼⟦T′⟧ } ← T′krip (InitEnvs⇒s®I ⊩SΓ₁ ρ′init)
rewrite Glu-wellfounded-≡ i<′
| Glu-wellfounded-≡ i<′₁
| ⟦⟧-det ↘⟦T⟧′ ↘⟦T⟧
| ⟦⟧-det ↘⟦T′⟧′ ↘⟦T′⟧
with record { A∈𝕌 = T∈𝕌 ; rel = Trel } ← T∼⟦T⟧
| record { A∈𝕌 = T′∈𝕌 ; rel = T′rel } ← T′∼⟦T′⟧ = ≈-sym ([I]-≈ˡ-Se (≈-sym ([I]-≈ˡ-Se (®⇒≈ T′∈𝕌 (®-transport T∈𝕌 T′∈𝕌 T≈T′ Trel) T′rel))))
adjust-Se-lvl : ∀ {i j} →
Γ ⊢ T ≈ T′ ∶ Se i →
Γ ⊢ T ∶ Se j →
Γ ⊢ T′ ∶ Se j →
Γ ⊢ T ≈ T′ ∶ Se j
adjust-Se-lvl T≈T′ ⊢T ⊢T′
with completeness T≈T′ | soundness ⊢T | soundness ⊢T′
... | _
, record { init = init₁ ; nbe = record { ⟦T⟧ = .(U _) ; ↘⟦t⟧ = ↘⟦T⟧ ; ↘⟦T⟧ = ⟦Se⟧ _ ; ↓⟦t⟧ = RU ._ ↘w } }
, record { init = init₂ ; nbe = record { ⟦T⟧ = .(U _) ; ↘⟦t⟧ = ↘⟦T′⟧ ; ↘⟦T⟧ = ⟦Se⟧ _ ; ↓⟦t⟧ = RU ._ ↘w′ } }
| _ , record { init = init₃ ; nbe = record { ⟦T⟧ = .(U _) ; ↘⟦t⟧ = ↘⟦T⟧₁ ; ↘⟦T⟧ = ⟦Se⟧ _ ; ↓⟦t⟧ = RU ._ ↘w₁ } } , T≈w
| _ , record { init = init ; nbe = record { ⟦T⟧ = .(U _) ; ↘⟦t⟧ = ↘⟦T′⟧₁ ; ↘⟦T⟧ = ⟦Se⟧ _ ; ↓⟦t⟧ = RU ._ ↘w′₁ } } , T′≈w
rewrite InitEnvs-det init₁ init
| InitEnvs-det init₂ init
| InitEnvs-det init₃ init
| ⟦⟧-det ↘⟦T⟧₁ ↘⟦T⟧
| ⟦⟧-det ↘⟦T′⟧₁ ↘⟦T′⟧
| Rty-det ↘w₁ ↘w
| Rty-det ↘w′₁ ↘w′ = ≈-trans T≈w (≈-sym T′≈w)
data IsND : D → Set where
ze : IsND ze
su : IsND a → IsND (su a)
data IsN : Nf → Set where
ze : IsN ze
su : IsN w → IsN (su w)
closed-®Nat : [] ⊢ t ∶N® a ∈Nat →
IsND a
closed-®Nat (ze _) = ze
closed-®Nat (su _ t∼a) = su (closed-®Nat t∼a)
closed-®Nat (ne c∈ rel)
with ≈u ← rel (⊢wI ⊢[])
with _ , _ , ⊢u , _ ← presup-≈ ≈u = ⊥-elim (no-closed-Ne ⊢u)
closed-NbE-N : [] ⊢ t ∶ N →
NbE [] t N w →
IsN w
closed-NbE-N ⊢t record { envs = envs ; nbe = record { ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦T⟧ = ⟦N⟧ ; ↓⟦t⟧ = ↓⟦t⟧ } }
with record { ⊩Γ = ⊩[] ; krip = krip } ← fundamental-⊢t⇒⊩t ⊢t
with record { ↘⟦T⟧ = ⟦N⟧ ; ↘⟦t⟧ = ↘⟦t⟧′ ; T∈𝕌 = N ; t∼⟦t⟧ = t∼⟦t⟧ , _ } ← krip {ρ = envs} (s-I ⊢[])
rewrite ⟦⟧-det ↘⟦t⟧′ ↘⟦t⟧ = helper (closed-®Nat t∼⟦t⟧) ↓⟦t⟧
where helper : IsND a → Rf 0 - ↓ N a ↘ w → IsN w
helper ze (Rze .0) = ze
helper (su a) (Rsu .0 ↘w) = su (helper a ↘w)
canonicity-N : [] ⊢ t ∶ N →
∃ λ w → [] ⊢ t ≈ Nf⇒Exp w ∶ N × IsN w
canonicity-N ⊢t
with w , nbe , ≈w ← soundness ⊢t = w , ≈w , closed-NbE-N ⊢t nbe
no-neutral-Se-gen : ∀ {i j} →
t ≡ Ne⇒Exp u →
Γ ⊢ t ∶ T →
Γ ≡ Se i ∷ [] →
Γ ⊢ T ≈ T′ ∶ Se j →
T′ ∈ v 0 ∷ N ∷ Π S S′ ∷ [] →
⊥
no-neutral-Se-gen {_} {v .0} {j = j} refl (vlookup ⊢Γ here) refl T≈ T′∈ = not-Se-≈-bundle (s≤s z≤n) (≈-trans (lift-⊢≈-Se-max {j = j} (≈-sym (Se-[] _ (s-wk ⊢Γ)))) (lift-⊢≈-Se-max′ T≈)) T′∈
no-neutral-Se-gen {_} {rec T z s u} refl (N-E _ _ _ ⊢t) eq T≈ T′∈ = no-neutral-Se-gen {S = N} {S′ = N} refl ⊢t eq (≈-refl (N-wf 0 (proj₁ (presup-tm ⊢t)))) (there (here refl))
no-neutral-Se-gen {_} {u $ n} refl (Λ-E ⊢t _) eq T≈ T′∈ = no-neutral-Se-gen refl ⊢t eq (≈-refl (proj₂ (proj₂ (presup-tm ⊢t)))) (there (there (here refl)))
no-neutral-Se-gen {_} {_} refl (cumu ⊢t) refl T≈ T′∈ = not-Se-≈-bundle (s≤s z≤n) T≈ T′∈
no-neutral-Se-gen {_} {_} refl (conv ⊢t ≈T) eq T≈ T′∈ = no-neutral-Se-gen refl ⊢t eq (≈-trans (lift-⊢≈-Se-max ≈T) (lift-⊢≈-Se-max′ T≈)) T′∈
no-neutral-Se : ∀ {i} →
Se i ∷ [] ⊢ Ne⇒Exp u ∶ v 0 →
⊥
no-neutral-Se ⊢u = no-neutral-Se-gen {S = N} {S′ = N} refl ⊢u refl (≈-refl (conv (vlookup (⊢∷ ⊢[] (Se-wf _ ⊢[])) here) (Se-[] _ (s-wk (⊢∷ ⊢[] (Se-wf _ ⊢[])))))) (here refl)
consistency : ∀ {i} → [] ⊢ t ∶ Π (Se i) (v 0) → ⊥
consistency {_} {i} ⊢t
with fundamental-⊢t⇒⊩t ⊢t
... | record { ⊩Γ = ⊩[] ; lvl = lvl ; krip = krip }
with krip {ρ = emp} (s-I ⊢[])
... | record { ↘⟦T⟧ = ⟦Π⟧ (⟦Se⟧ ._) ; T∈𝕌 = T∈𝕌@(Π iA@(U 0<l _) RT) ; t∼⟦t⟧ = t∼⟦t⟧@record { IT = IT ; OT = OT ; ⊢OT = ⊢OT ; T≈ = T≈ ; krip = krip } }
with ®Π-wf iA RT (®El⇒® T∈𝕌 t∼⟦t⟧)
| krip (⊢wI ⊢[])
| krip (⊢wwk (⊢∷ ⊢[] (t[σ]-Se (®Π-wf iA RT (®El⇒® T∈𝕌 t∼⟦t⟧)) (s-I ⊢[]))))
| Bot⊆El iA (Bot-l 0)
... | ⊢IT
| record { IT-rel = IT-rel }
| record { ap-rel = ap-rel }
| l∈A
with RT l∈A
| ap-rel (®El-resp-T≈ iA (v0®x iA IT-rel) ([]-cong-Se′ ([I] ⊢IT) (s-wk (⊢∷ ⊢[] (t[σ]-Se ⊢IT (s-I ⊢[])))))) l∈A
... | record { ↘⟦T⟧ = ⟦v⟧ .0 ; ↘⟦T′⟧ = ⟦v⟧ .0 ; T≈T′ = ne C≈C′ }
| record { fa = .(↑ _ _) ; ®fa = ne fa≈ , record { krip = krip } } = no-neutral-Se ⊢u′
where ⊢u : IT ∷ [] ⊢ Ne⇒Exp (proj₁ (fa≈ 1)) ∶ OT
⊢u = conv (ctxeq-tm (∷-cong []-≈ ([I] ⊢IT)) (proj₁ (proj₂ (proj₂ (presup-≈ (proj₂ (krip (⊢wI (⊢∷ ⊢[] (t[σ]-Se ⊢IT (s-I ⊢[])))))))))))
(≈-trans ([]-cong-Se′ (≈-trans ([]-cong-Se″ ⊢OT (wk,v0≈I (⊢∷ ⊢[] ⊢IT))) ([I] ⊢OT)) (s-I (⊢∷ ⊢[] ⊢IT))) ([I] ⊢OT))
⊢[Se] = ⊢∷ ⊢[] (Se-wf i ⊢[])
T≈′ : [] ⊢ Π (Se i) (v 0) ≈ Π IT OT ∶ Se _
T≈′ = ≈-trans (lift-⊢≈-Se-max {j = lvl} (≈-sym ([I] (Π-wf (Se-wf i ⊢[]) (cumu (conv (vlookup ⊢[Se] here) (Se-[] i (s-wk ⊢[Se])))))))) (lift-⊢≈-Se-max′ T≈)
IT≈ : [] ⊢ IT ≈ Se i ∶ Se _
IT≈ = ≈-sym (proj₁ (Π-≈-inj T≈′))
OT≈ : Se i ∷ [] ⊢ OT ≈ v 0 ∶ Se _
OT≈ = ≈-sym (proj₂ (Π-≈-inj T≈′))
⊢u′ : Se i ∷ [] ⊢ Ne⇒Exp (proj₁ (fa≈ 1)) ∶ v 0
⊢u′ = conv (ctxeq-tm (∷-cong []-≈ IT≈) ⊢u) OT≈