{-# OPTIONS --without-K --safe #-}
open import Level hiding (_⊔_)
open import Axiom.Extensionality.Propositional
module MLTT.Completeness.Pi (fext : Extensionality 0ℓ (suc 0ℓ)) where
open import Data.Nat
open import Data.Nat.Properties
open import Lib
open import MLTT.Completeness.LogRel
open import MLTT.Completeness.Substitutions fext
open import MLTT.Completeness.Terms fext
open import MLTT.Semantics.Properties.PER fext
Π-[]′ : ∀ {i} →
Γ ⊨s σ ∶ Δ →
Δ ⊨ S ∶ Se i →
S ∷ Δ ⊨ T ∶ Se i →
Γ ⊨ Π S T [ σ ] ≈ Π (S [ σ ]) (T [ q σ ]) ∶ Se i
Π-[]′ {_} {σ} {_} {S} {T} {i} (⊨Γ , ⊨Δ , ⊨σ) (⊨Δ₁ , _ , ⊨S) (∷-cong ⊨Δ₂ rel , _ , ⊨T) = ⊨Γ , _ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
Σ (RelTyp _ (Se i) ρ (Se i) ρ′)
λ rel → RelExp (Π S T [ σ ]) ρ (Π (S [ σ ]) (T [ q σ ])) ρ′ (El _ (RelTyp.T≈T′ rel))
helper {ρ} {ρ′} ρ≈ρ′ = help
where module σ = RelSubst (⊨σ ρ≈ρ′)
help : Σ (RelTyp _ (Se i) ρ (Se i) ρ′)
λ rel → RelExp (Π S T [ σ ]) ρ (Π (S [ σ ]) (T [ q σ ])) ρ′ (El _ (RelTyp.T≈T′ rel))
help
with ⊨S (⊨-irrel ⊨Δ ⊨Δ₁ σ.σ≈δ)
... | record { ⟦T⟧ = .(U i) ; ⟦T′⟧ = .(U i) ; ↘⟦T⟧ = (⟦Se⟧ .i) ; ↘⟦T′⟧ = (⟦Se⟧ .i) ; T≈T′ = U i<j _ }
, record { ⟦t⟧ = ⟦t⟧ ; ⟦t′⟧ = ⟦t′⟧ ; ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦t′⟧ = ↘⟦t′⟧ ; t≈t′ = t≈t′ }
= record
{ ⟦T⟧ = U i
; ⟦T′⟧ = U i
; ↘⟦T⟧ = ⟦Se⟧ i
; ↘⟦T′⟧ = ⟦Se⟧ i
; T≈T′ = U′ i<j
}
, record
{ ⟦t⟧ = Π ⟦t⟧ T σ.⟦σ⟧
; ⟦t′⟧ = Π ⟦t′⟧ (T [ q σ ]) ρ′
; ↘⟦t⟧ = ⟦[]⟧ σ.↘⟦σ⟧ (⟦Π⟧ ↘⟦t⟧)
; ↘⟦t′⟧ = ⟦Π⟧ (⟦[]⟧ σ.↘⟦δ⟧ ↘⟦t′⟧)
; t≈t′ = subst (Π ⟦t⟧ T σ.⟦σ⟧ ≈ Π ⟦t′⟧ (T [ q σ ]) ρ′ ∈_) (sym (𝕌-wellfounded-≡-𝕌 _ i<j))
(result (subst (⟦t⟧ ≈ ⟦t′⟧ ∈_) (𝕌-wellfounded-≡-𝕌 _ i<j) t≈t′))
}
where result : ⟦t⟧ ≈ ⟦t′⟧ ∈ 𝕌 i →
Π ⟦t⟧ T σ.⟦σ⟧ ≈ Π ⟦t′⟧ (T [ q σ ]) ρ′ ∈ 𝕌 i
result S≈ = Π S≈ step
where step : a ≈ a′ ∈ El i S≈ →
ΠRT T (σ.⟦σ⟧ ↦ a) (T [ q σ ]) (ρ′ ↦ a′) (𝕌 i)
step {a} {a′} a≈a′
with σ≈δ₁ ← ⊨-irrel ⊨Δ ⊨Δ₂ σ.σ≈δ = answer
where insert : a ≈ a′ ∈ El _ (RelTyp.T≈T′ (rel σ≈δ₁))
insert
with record { ⟦T⟧ = ⟦T⟧ ; ⟦T′⟧ = ⟦T′⟧ ; ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ } ← rel σ≈δ₁
rewrite ⟦⟧-det ↘⟦T′⟧ ↘⟦t′⟧
| ⟦⟧-det ↘⟦T⟧ ↘⟦t⟧ = 𝕌-irrel S≈ T≈T′ a≈a′
answer : ΠRT T (σ.⟦σ⟧ ↦ a) (T [ q σ ]) (ρ′ ↦ a′) (𝕌 i)
answer
with ⊨T {σ.⟦σ⟧ ↦ a} {σ.⟦δ⟧ ↦ a′} (σ≈δ₁ , insert)
... | record { ⟦T⟧ = .(U i) ; ⟦T′⟧ = .(U i) ; ↘⟦T⟧ = (⟦Se⟧ .i) ; ↘⟦T′⟧ = (⟦Se⟧ .i) ; T≈T′ = U i<j _ }
, re = record
{ ⟦T⟧ = re.⟦t⟧
; ⟦T′⟧ = re.⟦t′⟧
; ↘⟦T⟧ = re.↘⟦t⟧
; ↘⟦T′⟧ = ⟦[]⟧ (⟦q⟧ σ.↘⟦δ⟧) re.↘⟦t′⟧
; T≈T′ = subst (re.⟦t⟧ ≈ re.⟦t′⟧ ∈_) (𝕌-wellfounded-≡-𝕌 _ i<j) re.t≈t′
}
where module re = RelExp re
Π-cong′ : ∀ {i} →
Γ ⊨ S ≈ S′ ∶ Se i →
S ∷ Γ ⊨ T ≈ T′ ∶ Se i →
Γ ⊨ Π S T ≈ Π S′ T′ ∶ Se i
Π-cong′ {_} {S} {S′} {T} {T′} {i} (⊨Γ , _ , S≈S′) (∷-cong ⊨Γ₁ rel , _ , T≈T′) = ⊨Γ , _ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
Σ (RelTyp _ (Se i) ρ (Se i) ρ′)
λ rel → RelExp (Π S T) ρ (Π S′ T′) ρ′ (El _ (RelTyp.T≈T′ rel))
helper {ρ} {ρ′} ρ≈ρ′
with S≈S′ ρ≈ρ′
... | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦T′⟧ = ⟦Se⟧ _ ; T≈T′ = U i<j _ }
, record { ⟦t⟧ = ⟦t⟧ ; ⟦t′⟧ = ⟦t′⟧ ; ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦t′⟧ = ↘⟦t′⟧ ; t≈t′ = t≈t′ }
rewrite 𝕌-wellfounded-≡-𝕌 _ i<j = record
{ ↘⟦T⟧ = ⟦Se⟧ _
; ↘⟦T′⟧ = ⟦Se⟧ _
; T≈T′ = U′ i<j
}
, record
{ ↘⟦t⟧ = ⟦Π⟧ ↘⟦t⟧
; ↘⟦t′⟧ = ⟦Π⟧ ↘⟦t′⟧
; t≈t′ = subst (Π ⟦t⟧ T ρ ≈ Π ⟦t′⟧ T′ ρ′ ∈_) (sym (𝕌-wellfounded-≡-𝕌 _ i<j)) (Π t≈t′ result)
}
where result : a ≈ a′ ∈ El _ t≈t′ →
ΠRT T (ρ ↦ a) T′ (ρ′ ↦ a′) (𝕌 i)
result {a} {a′} a≈a′
with ρ≈ρ′₁ ← ⊨-irrel ⊨Γ ⊨Γ₁ ρ≈ρ′ = answer
where insert : a ≈ a′ ∈ El _ (RelTyp.T≈T′ (rel ρ≈ρ′₁))
insert
with record { ⟦T⟧ = ⟦T⟧ ; ↘⟦T⟧ = ↘⟦T⟧ ; T≈T′ = T≈T′ } ← rel ρ≈ρ′₁
rewrite ⟦⟧-det ↘⟦T⟧ ↘⟦t⟧ = El-one-sided t≈t′ T≈T′ a≈a′
answer : ΠRT T (ρ ↦ a) T′ (ρ′ ↦ a′) (𝕌 i)
answer
with T≈T′ {ρ ↦ a} {ρ′ ↦ a′} (ρ≈ρ′₁ , insert)
... | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦T′⟧ = ⟦Se⟧ _ ; T≈T′ = U i<j _ }
, re = record
{ ↘⟦T⟧ = re.↘⟦t⟧
; ↘⟦T′⟧ = re.↘⟦t′⟧
; T≈T′ = subst (re.⟦t⟧ ≈ re.⟦t′⟧ ∈_) (𝕌-wellfounded-≡-𝕌 _ i<j) re.t≈t′
}
where module re = RelExp re
Λ-cong′ : S ∷ Γ ⊨ t ≈ t′ ∶ T →
Γ ⊨ Λ t ≈ Λ t′ ∶ Π S T
Λ-cong′ {S} {_} {t} {t′} {T} (∷-cong ⊨Γ rel , n , t≈t′) = ⊨Γ , _ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
Σ (RelTyp _ (Π S T) ρ (Π S T) ρ′)
λ rel → RelExp (Λ t) ρ (Λ t′) ρ′ (El _ (RelTyp.T≈T′ rel))
helper {ρ} {ρ′} ρ≈ρ′ = record
{ ↘⟦T⟧ = ⟦Π⟧ S.↘⟦T⟧
; ↘⟦T′⟧ = ⟦Π⟧ S.↘⟦T′⟧
; T≈T′ = Π (𝕌-cumu (m≤m⊔n _ n) S.T≈T′) λ a≈b → proj₁ (Πres a≈b)
}
, record
{ ↘⟦t⟧ = ⟦Λ⟧ t
; ↘⟦t′⟧ = ⟦Λ⟧ t′
; t≈t′ = λ a≈b → proj₂ (Πres a≈b)
}
where module S = RelTyp (rel ρ≈ρ′)
insert : (⊨Γ : ⊨ Γ) →
(rel : ∀ {ρ ρ′} → ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ → RelTyp _ S ρ S ρ′) →
(ρ≈ρ′ : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ) →
a ≈ a′ ∈ El _ (𝕌-cumu (m≤m⊔n _ n) S.T≈T′) →
a ≈ a′ ∈ El _ (RelTyp.T≈T′ (rel ρ≈ρ′))
insert ⊨Γ rel ρ≈ρ′ a≈a′
with record { ⟦T⟧ = ⟦T⟧ ; ⟦T′⟧ = ⟦T′⟧ ; ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ } ← rel ρ≈ρ′
rewrite ⟦⟧-det ↘⟦T⟧ S.↘⟦T⟧ = El-one-sided (𝕌-cumu (m≤m⊔n _ n) S.T≈T′) T≈T′ a≈a′
Πres : (a≈b : a ≈ b ∈ El _ (𝕌-cumu (m≤m⊔n _ n) S.T≈T′)) →
Σ (ΠRT T (ρ ↦ a) T (ρ′ ↦ b) (𝕌 _))
λ rel → Π̂ (Λ t ρ) a (Λ t′ ρ′) b (El _ (ΠRT.T≈T′ rel))
Πres {a} {b} a≈b = answer
where answer : Σ (ΠRT T (ρ ↦ a) T (ρ′ ↦ b) (𝕌 _))
λ rel → Π̂ (Λ t ρ) a (Λ t′ ρ′) b (El _ (ΠRT.T≈T′ rel))
answer
with t≈t′ {ρ ↦ a} {ρ′ ↦ b} (ρ≈ρ′ , insert ⊨Γ rel ρ≈ρ′ a≈b)
... | record { ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ }
, re = record
{ ↘⟦T⟧ = ↘⟦T⟧
; ↘⟦T′⟧ = ↘⟦T′⟧
; T≈T′ = T≈T′₁
}
, record
{ ↘fa = Λ∙ re.↘⟦t⟧
; ↘fa′ = Λ∙ re.↘⟦t′⟧
; fa≈fa′ = 𝕌-irrel T≈T′ T≈T′₁ re.t≈t′
}
where module re = RelExp re
T≈T′₁ = 𝕌-cumu (m≤n⊔m _ n) T≈T′
$-cong′ : Γ ⊨ r ≈ r′ ∶ Π S T →
Γ ⊨ s ≈ s′ ∶ S →
Γ ⊨ r $ s ≈ r′ $ s′ ∶ T [| s ]
$-cong′ {_} {r} {r′} {S} {T} {s} {s′} (⊨Γ , _ , r≈r′) (⊨Γ₁ , _ , s≈s′) = ⊨Γ , _ , helper
where helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
Σ (RelTyp _ (T [| s ]) ρ (T [| s ]) ρ′)
λ rel → RelExp (r $ s) ρ (r′ $ s′) ρ′ (El _ (RelTyp.T≈T′ rel))
helper {ρ} {ρ′} ρ≈ρ′
with ρ≈ρ ← ⊨-irrel ⊨Γ ⊨Γ₁ (⟦⟧ρ-refl ⊨Γ ⊨Γ ρ≈ρ′)
| ρ′≈ρ ← ⊨-irrel ⊨Γ ⊨Γ₁ (⟦⟧ρ-sym′ ⊨Γ ρ≈ρ′)
with r≈r′ ρ≈ρ′
| s≈s′ ρ≈ρ
| s≈s′ ρ′≈ρ
| s≈s′ (⊨-irrel ⊨Γ ⊨Γ₁ ρ≈ρ′)
... | record { ↘⟦T⟧ = ⟦Π⟧ ↘⟦S⟧ ; ↘⟦T′⟧ = ⟦Π⟧ ↘⟦S⟧′ ; T≈T′ = Π iA RT }
, record { ⟦t⟧ = ⟦r⟧ ; ⟦t′⟧ = ⟦r′⟧ ; ↘⟦t⟧ = ↘⟦r⟧ ; ↘⟦t′⟧ = ↘⟦r′⟧ ; t≈t′ = r≈r′ }
| record { ⟦T⟧ = ⟦T⟧₁ ; ⟦T′⟧ = ⟦T′⟧₁ ; ↘⟦T⟧ = ↘⟦T⟧₁ ; ↘⟦T′⟧ = ↘⟦T′⟧₁ ; T≈T′ = T≈T′₁ }
, record { ⟦t⟧ = ⟦t⟧₁ ; ⟦t′⟧ = ⟦t′⟧₁ ; ↘⟦t⟧ = ↘⟦t⟧₁ ; ↘⟦t′⟧ = ↘⟦t′⟧₁ ; t≈t′ = t≈t′₁ }
| record { ⟦T⟧ = ⟦T⟧₂ ; ⟦T′⟧ = ⟦T′⟧₂ ; ↘⟦T⟧ = ↘⟦T⟧₂ ; ↘⟦T′⟧ = ↘⟦T′⟧₂ ; T≈T′ = T≈T′₂ }
, record { ⟦t⟧ = ⟦t⟧₂ ; ⟦t′⟧ = ⟦t′⟧₂ ; ↘⟦t⟧ = ↘⟦t⟧₂ ; ↘⟦t′⟧ = ↘⟦t′⟧₂ ; t≈t′ = t≈t′₂ }
| record { ⟦T⟧ = ⟦T⟧ ; ⟦T′⟧ = ⟦T′⟧ ; ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ }
, record { ⟦t⟧ = ⟦t⟧ ; ⟦t′⟧ = ⟦t′⟧ ; ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦t′⟧ = ↘⟦t′⟧ ; t≈t′ = t≈t′ }
rewrite ⟦⟧-det ↘⟦S⟧ ↘⟦T⟧
| ⟦⟧-det ↘⟦S⟧′ ↘⟦T′⟧
| ⟦⟧-det ↘⟦T⟧₁ ↘⟦T⟧
| ⟦⟧-det ↘⟦T′⟧₁ ↘⟦T′⟧₂
| ⟦⟧-det ↘⟦t′⟧₁ ↘⟦t′⟧₂
| ⟦⟧-det ↘⟦t⟧₁ ↘⟦t⟧ = record
{ ↘⟦T⟧ = ⟦[]⟧ (⟦,⟧ ⟦I⟧ ↘⟦t⟧) RT.↘⟦T⟧
; ↘⟦T′⟧ = ⟦[]⟧ (⟦,⟧ ⟦I⟧ ↘⟦t⟧₂) RT.↘⟦T′⟧
; T≈T′ = RT.T≈T′
}
, record
{ ↘⟦t⟧ = ⟦$⟧ ↘⟦r⟧ ↘⟦t⟧ rs.↘fa
; ↘⟦t′⟧ = ⟦$⟧ ↘⟦r′⟧ ↘⟦t′⟧ rs.↘fa′
; t≈t′ = El-transp RT′.T≈T′ RT.T≈T′ rs.fa≈fa′ (sym (⟦⟧-det RT.↘⟦T⟧ RT′.↘⟦T⟧))
}
where T≈T = 𝕌-trans T≈T′₁ (𝕌-sym T≈T′₂)
srel = El-trans T≈T′₁ (𝕌-sym T≈T′₂) T≈T t≈t′₁ (El-sym T≈T′₂ (𝕌-sym T≈T′₂) t≈t′₂)
module RT = ΠRT (RT (El-one-sided T≈T iA srel))
module RT′ = ΠRT (RT (El-one-sided T≈T′ iA t≈t′))
module rs = Π̂ (r≈r′ (El-one-sided T≈T′ iA t≈t′))
Λ-β′ : S ∷ Γ ⊨ t ∶ T →
Γ ⊨ s ∶ S →
Γ ⊨ Λ t $ s ≈ t [| s ] ∶ T [| s ]
Λ-β′ {S} {_} {t} {T} {s} (∷-cong ⊨Γ rel , _ , ⊨t) (⊨Γ₁ , _ , ⊨s) = ⊨Γ , _ , helper
where
helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
Σ (RelTyp _ (T [| s ]) ρ (T [| s ]) ρ′)
λ rel → RelExp (Λ t $ s) ρ (t [| s ]) ρ′ (El _ (RelTyp.T≈T′ rel))
helper {ρ} {ρ′} ρ≈ρ′
with ⊨s (⊨-irrel ⊨Γ ⊨Γ₁ ρ≈ρ′)
... | record { ↘⟦T⟧ = ↘⟦S⟧ ; ↘⟦T′⟧ = ↘⟦S′⟧ ; T≈T′ = S≈S′ }
, record { ⟦t⟧ = ⟦s⟧ ; ⟦t′⟧ = ⟦s′⟧ ; ↘⟦t⟧ = ↘⟦s⟧ ; ↘⟦t′⟧ = ↘⟦s′⟧ ; t≈t′ = s≈s′ } = helper′
where
s≈s′₁ : ⟦s⟧ ≈ ⟦s′⟧ ∈ El _ (RelTyp.T≈T′ (rel ρ≈ρ′))
s≈s′₁
with record { ↘⟦T⟧ = ↘⟦S⟧₁ ; ↘⟦T′⟧ = ↘⟦S′⟧₁ ; T≈T′ = S≈S′₁ } ← rel ρ≈ρ′
rewrite ⟦⟧-det ↘⟦S⟧ ↘⟦S⟧₁
| ⟦⟧-det ↘⟦S′⟧ ↘⟦S′⟧₁
= 𝕌-irrel S≈S′ S≈S′₁ s≈s′
helper′ : Σ (RelTyp _ (T [| s ]) ρ (T [| s ]) ρ′)
λ rel → RelExp (Λ t $ s) ρ (t [| s ]) ρ′ (El _ (RelTyp.T≈T′ rel))
helper′
with ⊨t (ρ≈ρ′ , s≈s′₁)
... | record { ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ }
, record { ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦t′⟧ = ↘⟦t′⟧ ; t≈t′ = t≈t′ } = record
{ ↘⟦T⟧ = ⟦[]⟧ (⟦,⟧ ⟦I⟧ ↘⟦s⟧) ↘⟦T⟧
; ↘⟦T′⟧ = ⟦[]⟧ ((⟦,⟧ ⟦I⟧ ↘⟦s′⟧)) ↘⟦T′⟧
; T≈T′ = T≈T′
}
, record
{ ↘⟦t⟧ = ⟦$⟧ (⟦Λ⟧ _) ↘⟦s⟧ (Λ∙ ↘⟦t⟧)
; ↘⟦t′⟧ = ⟦[]⟧ (⟦,⟧ ⟦I⟧ ↘⟦s′⟧) ↘⟦t′⟧
; t≈t′ = t≈t′
}
Λ-η′ : Γ ⊨ t ∶ Π S T →
Γ ⊨ t ≈ Λ (t [ wk ] $ v 0) ∶ Π S T
Λ-η′ {_} {t} {S} {T} (⊨Γ , n , ⊨t) = ⊨Γ , _ , helper
where
helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
Σ (RelTyp _ (Π S T) ρ (Π S T) ρ′)
λ rel → RelExp t ρ (Λ (t [ wk ] $ v 0)) ρ′ (El _ (RelTyp.T≈T′ rel))
helper {ρ} {ρ′} ρ≈ρ′
with ⊨t ρ≈ρ′
... | ⊨ΠST@(record { ↘⟦T⟧ = ⟦Π⟧ _ ; ↘⟦T′⟧ = ⟦Π⟧ _ ; T≈T′ = Π iS T≈T′ })
, record { ⟦t⟧ = ⟦t⟧ ; ⟦t′⟧ = ⟦t′⟧ ; ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦t′⟧ = ↘⟦t′⟧ ; t≈t′ = t≈t′ } = ⊨ΠST , record
{ ↘⟦t⟧ = ↘⟦t⟧
; ↘⟦t′⟧ = ⟦Λ⟧ _
; t≈t′ = helper′
}
where
helper′ : {a b : D} (inp : a ≈ b ∈ El _ iS) →
Π̂ (⟦t⟧) a ((Λ (t [ wk ] $ v 0) ρ′)) b (El _ (ΠRT.T≈T′ (T≈T′ inp)))
helper′ {a} {b} inp
with record { ↘fa = ↘fa ; ↘fa′ = ↘fa′ ; fa≈fa′ = fa≈fa′ } ← t≈t′ inp = record
{ ↘fa = ↘fa
; ↘fa′ = Λ∙ (⟦$⟧ (⟦[]⟧ ⟦wk⟧ ↘⟦t′⟧) (⟦v⟧ 0) ↘fa′)
; fa≈fa′ = fa≈fa′
}
Λ-[]′ : Γ ⊨s σ ∶ Δ →
S ∷ Δ ⊨ t ∶ T →
Γ ⊨ Λ t [ σ ] ≈ Λ (t [ q σ ]) ∶ Π S T [ σ ]
Λ-[]′ {_} {σ} {_} {S} {t} {T} (⊨Γ , ⊨Δ , ⊨σ) (∷-cong ⊨Δ₁ Srel₁ , n₁ , ⊨t) = ⊨Γ , _ , helper
where
helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
Σ (RelTyp _ (Π S T [ σ ]) ρ (Π S T [ σ ]) ρ′)
λ rel → RelExp (Λ t [ σ ]) ρ (Λ (t [ q σ ])) ρ′ (El _ (RelTyp.T≈T′ rel))
helper {ρ} {ρ′} ρ≈ρ′
with record { ⟦σ⟧ = ⟦σ⟧ ; ⟦δ⟧ = ⟦δ⟧ ; ↘⟦σ⟧ = ↘⟦σ⟧ ; ↘⟦δ⟧ = ↘⟦δ⟧ ; σ≈δ = σ≈δ } ← ⊨σ ρ≈ρ′
with record { ↘⟦T⟧ = ↘⟦S⟧ ; ↘⟦T′⟧ = ↘⟦S′⟧ ; T≈T′ = S≈S′ } ← Srel₁ (⊨-irrel ⊨Δ ⊨Δ₁ σ≈δ) = record
{ ↘⟦T⟧ = ⟦[]⟧ ↘⟦σ⟧ (⟦Π⟧ ↘⟦S⟧)
; ↘⟦T′⟧ = ⟦[]⟧ ↘⟦δ⟧ (⟦Π⟧ ↘⟦S′⟧)
; T≈T′ = Π (𝕌-cumu (m≤m⊔n _ n₁) S≈S′) return
}
, record
{ ↘⟦t⟧ = ⟦[]⟧ ↘⟦σ⟧ (⟦Λ⟧ _)
; ↘⟦t′⟧ = ⟦Λ⟧ _
; t≈t′ = result
}
where
helper′ : {a b : D} (inp : a ≈ b ∈ El _ (𝕌-cumu (m≤m⊔n _ n₁) S≈S′)) →
Σ (RelTyp n₁ T (⟦σ⟧ ↦ a) T (⟦δ⟧ ↦ b))
λ rel → RelExp t (⟦σ⟧ ↦ a) t (⟦δ⟧ ↦ b) (El _ (RelTyp.T≈T′ rel))
helper′ {a} {b} inp = ⊨t (σ≈δ₁ , a≈b)
where
σ≈δ₁ : ⟦σ⟧ ≈ ⟦δ⟧ ∈ ⟦ ⊨Δ₁ ⟧ρ
σ≈δ₁ = ⊨-irrel ⊨Δ ⊨Δ₁ σ≈δ
a≈b : a ≈ b ∈ El _ (RelTyp.T≈T′ (Srel₁ σ≈δ₁))
a≈b
with record { ↘⟦T⟧ = ↘⟦S⟧₁ ; ↘⟦T′⟧ = ↘⟦S′⟧₁ ; T≈T′ = S≈S′₁ } ← Srel₁ σ≈δ₁
rewrite ⟦⟧-det ↘⟦S⟧₁ ↘⟦S⟧
| ⟦⟧-det ↘⟦S′⟧₁ ↘⟦S′⟧ = 𝕌-irrel (𝕌-cumu (m≤m⊔n _ n₁) S≈S′) S≈S′₁ inp
return : {a b : D} →
a ≈ b ∈ El _ (𝕌-cumu (m≤m⊔n _ n₁) S≈S′) →
ΠRT T (⟦σ⟧ ↦ a) T (⟦δ⟧ ↦ b) (𝕌 (_ ⊔ n₁))
return inp
with record { ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ } ← proj₁ (helper′ inp) = record
{ ↘⟦T⟧ = ↘⟦T⟧
; ↘⟦T′⟧ = ↘⟦T′⟧
; T≈T′ = 𝕌-cumu (m≤n⊔m _ _) T≈T′
}
result : {a b : D} (inp : a ≈ b ∈ El _ (𝕌-cumu (m≤m⊔n _ n₁) S≈S′)) →
Π̂ (Λ t ⟦σ⟧) a ((Λ (t [ q σ ]) ρ′)) b (El _ (ΠRT.T≈T′ (return inp)))
result {a} {b} inp
with helper′ inp
... | record { T≈T′ = T≈T′ }
, record { ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦t′⟧ = ↘⟦t′⟧ ; t≈t′ = t≈t′ } = record
{ ↘fa = Λ∙ ↘⟦t⟧
; ↘fa′ = Λ∙ (⟦[]⟧ (⟦q⟧ ↘⟦δ⟧) ↘⟦t′⟧)
; fa≈fa′ = 𝕌-irrel T≈T′ (𝕌-cumu (m≤n⊔m _ _) T≈T′) t≈t′
}
$-[]′ : Γ ⊨s σ ∶ Δ →
Δ ⊨ r ∶ Π S T →
Δ ⊨ s ∶ S →
Γ ⊨ (r $ s) [ σ ] ≈ r [ σ ] $ s [ σ ] ∶ T [ σ , s [ σ ] ]
$-[]′ {_} {σ} {_} {r} {S} {T} {s} (⊨Γ , ⊨Δ , ⊨σ) (⊨Δ₁ , _ , ⊨r) (⊨Δ₂ , _ , ⊨s) = ⊨Γ , _ , helper
where
helper : ρ ≈ ρ′ ∈ ⟦ ⊨Γ ⟧ρ →
Σ (RelTyp _ (T [ σ , s [ σ ] ]) ρ (T [ σ , s [ σ ] ]) ρ′)
λ rel → RelExp ((r $ s) [ σ ]) ρ (r [ σ ] $ s [ σ ]) ρ′ (El _ (RelTyp.T≈T′ rel))
helper {ρ} {ρ′} ρ≈ρ′
with record { ⟦σ⟧ = ⟦σ⟧ ; ⟦δ⟧ = ⟦δ⟧ ; ↘⟦σ⟧ = ↘⟦σ⟧ ; ↘⟦δ⟧ = ↘⟦δ⟧ ; σ≈δ = σ≈δ } ← ⊨σ ρ≈ρ′
with ⊨r (⊨-irrel ⊨Δ ⊨Δ₁ σ≈δ)
| ⊨s (⊨-irrel ⊨Δ ⊨Δ₂ σ≈δ)
... | record { ↘⟦T⟧ = ⟦Π⟧ ↘⟦S⟧ ; ↘⟦T′⟧ = ⟦Π⟧ ↘⟦S′⟧ ; T≈T′ = Π iS Trel }
, record { ⟦t⟧ = ⟦r⟧ ; ⟦t′⟧ = ⟦r′⟧ ; ↘⟦t⟧ = ↘⟦r⟧ ; ↘⟦t′⟧ = ↘⟦r′⟧ ; t≈t′ = r≈r′ }
| record { ⟦T⟧ = ⟦S⟧₁ ; ⟦T′⟧ = ⟦S′⟧₁ ; ↘⟦T⟧ = ↘⟦S⟧₁ ; ↘⟦T′⟧ = ↘⟦S′⟧₁ ; T≈T′ = S≈S′₁ }
, record { ⟦t⟧ = ⟦s⟧ ; ⟦t′⟧ = ⟦s′⟧ ; ↘⟦t⟧ = ↘⟦s⟧ ; ↘⟦t′⟧ = ↘⟦s′⟧ ; t≈t′ = s≈s′ }
rewrite ⟦⟧-det ↘⟦S⟧ ↘⟦S⟧₁
| ⟦⟧-det ↘⟦S′⟧ ↘⟦S′⟧₁
with record { ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ } ← Trel (𝕌-irrel S≈S′₁ iS s≈s′)
| record { ↘fa = ↘fa ; ↘fa′ = ↘fa′ ; fa≈fa′ = fa≈fa′ } ← r≈r′ (𝕌-irrel S≈S′₁ iS s≈s′) = record
{ ↘⟦T⟧ = ⟦[]⟧ (⟦,⟧ ↘⟦σ⟧ (⟦[]⟧ ↘⟦σ⟧ ↘⟦s⟧)) ↘⟦T⟧
; ↘⟦T′⟧ = ⟦[]⟧ (⟦,⟧ ↘⟦δ⟧ (⟦[]⟧ ↘⟦δ⟧ ↘⟦s′⟧)) ↘⟦T′⟧
; T≈T′ = T≈T′
}
, record
{ ↘⟦t⟧ = ⟦[]⟧ ↘⟦σ⟧ (⟦$⟧ ↘⟦r⟧ ↘⟦s⟧ ↘fa)
; ↘⟦t′⟧ = ⟦$⟧ (⟦[]⟧ ↘⟦δ⟧ ↘⟦r′⟧) (⟦[]⟧ ↘⟦δ⟧ ↘⟦s′⟧) ↘fa′
; t≈t′ = fa≈fa′
}