{-# OPTIONS --without-K --safe #-}

open import Level
open import Axiom.Extensionality.Propositional

-- Semantic judgments for Π types
module MLTT.Soundness.Pi (fext : Extensionality 0ℓ (suc 0ℓ)) where

open import Lib
open import Data.Nat.Properties as ℕₚ

open import MLTT.Statics.Properties
open import MLTT.Semantics.Properties.PER fext
open import MLTT.Completeness.Consequences fext
open import MLTT.Completeness.Fundamental fext
open import MLTT.Soundness.Realizability fext
open import MLTT.Soundness.Cumulativity fext
open import MLTT.Soundness.LogRel
open import MLTT.Soundness.ToSyntax fext
open import MLTT.Soundness.Properties.LogRel fext
open import MLTT.Soundness.Properties.Substitutions fext


Π-wf′ :  {i} 
        Γ  S  Se i 
        S  Γ  T  Se i 
        --------------------
        Γ  Π S T  Se i
Π-wf′ {Γ} {S} {T} {i} ⊩S ⊩T
  with ⊩S | ⊩⇒⊢-tm ⊩S | ⊩T | ⊩⇒⊢-tm ⊩T
...  | record { ⊩Γ = ⊩Γ ; lvl = lvl ; krip = Skrip }
     | ⊢S
     | record { ⊩Γ = (⊩∷ ⊩Γ₁ ⊢S₁ gS) ; lvl = lvl₁ ; krip = Tkrip₁ }
     | ⊢T
    with fundamental-⊢t ⊢T
...    | ∷-cong ⊨Γ₁ Srel₁ , n₁ , Trel₁ = record { ⊩Γ = ⊩Γ ; krip = krip }
  where
    krip :  {Δ σ ρ} 
           Δ ⊢s σ  ⊩Γ ® ρ 
           GluExp lvl Δ (Π S T) (Se i) σ ρ
    krip {Δ} {σ} {ρ} σ∼ρ
      with Skrip σ∼ρ | s®⇒⟦⟧ρ ⊩Γ σ∼ρ
    ...  | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦t⟧ = ↘⟦S⟧ ; T∈𝕌 = U i<lvl _ ; t∼⟦t⟧ = S∼⟦S⟧ }
         | ⊨Γ , ρ∈
          with S∼⟦S⟧
    ...      | record { A∈𝕌 = S∈𝕌 ; rel = S∼⟦S⟧ } = record
                { ↘⟦T⟧ = ⟦Se⟧ _
                ; ↘⟦t⟧ = ⟦Π⟧ ↘⟦S⟧
                ; T∈𝕌 = U′ i<lvl
                ; t∼⟦t⟧ = record
                          { t∶T = t[σ] (Π-wf ⊢S ⊢T) ⊢σ
                          ; T≈ = lift-⊢≈-Se (Se-[] _ ⊢σ) i<lvl
                          ; A∈𝕌 = Π S∈𝕌 ΠRTT
                          ; rel = subst  f  f _ _ (Π S∈𝕌 ΠRTT)) (sym (Glu-wellfounded-≡ i<lvl)) rel
                          }
                }
      where
        ⊢σ = s®⇒⊢s ⊩Γ σ∼ρ
        ⊢Δ = proj₁ (presup-s ⊢σ)

        ΠRTT : {a a′ : D} 
               a  a′  El _ S∈𝕌 
               ΠRT T (ρ  a) T (ρ  a′) (𝕌 i)
        ΠRTT {a} {a′} a≈a′ = helper
          where
            ρ≈′ : ρ ∈′  ⊨Γ₁ ⟧ρ
            ρ≈′ = ⊨-irrel ⊨Γ ⊨Γ₁ ρ∈

            a≈a′₁ : a  a′  El _ (RelTyp.T≈T′ (Srel₁ ρ≈′))
            a≈a′₁
              with Srel₁ ρ≈′
            ...  | record { ↘⟦T⟧ = ↘⟦S⟧₁ ; ↘⟦T′⟧ = ↘⟦S′⟧₁ ; T≈T′ = S≈S′ }
                rewrite ⟦⟧-det ↘⟦S⟧₁ ↘⟦S⟧ = El-one-sided S∈𝕌 S≈S′ a≈a′

            helper : ΠRT T (ρ  a) T (ρ  a′) (𝕌 i)
            helper
              with Trel₁ (ρ≈′ , a≈a′₁)
            ...  | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦T′⟧ = ⟦Se⟧ _ ; T≈T′ = U i<n₁ _ }
                 , record { ↘⟦t⟧ = ↘⟦T⟧ ; ↘⟦t′⟧ = ↘⟦T′⟧ ; t≈t′ = T≈T′ }
                rewrite 𝕌-wellfounded-≡-𝕌 _ i<n₁ = record
                                                   { ↘⟦T⟧ = ↘⟦T⟧
                                                   ; ↘⟦T′⟧ = ↘⟦T′⟧
                                                   ; T≈T′ = T≈T′
                                                   }

        rel : Δ  Π S T [ σ ] ®[ i ] Π S∈𝕌 ΠRTT
        rel = record
              { ⊢OT = t[σ]-Se ⊢T (⊢q ⊢σ ⊢S)
              ; T≈ = Π-[] ⊢σ ⊢S ⊢T
              ; krip = helper
              }
          where
            helper :  {Δ′ δ} 
                     Δ′ ⊢w δ  Δ 
                     ΠRel i Δ′ (S [ σ ]) (T [ q σ ]) δ S∈𝕌
                       (_⊢_®[ i ] S∈𝕌)
                        a∈  _⊢_®[ i ] ΠRT.T≈T′ (ΠRTT a∈))
                       (_⊢_∶_®[ i ]_∈El S∈𝕌)
            helper {Δ′} {δ} ⊢δ = record
                                { IT-rel = ®-mon′ S∈𝕌 (subst  f  f _ _ _) (Glu-wellfounded-≡ i<lvl) S∼⟦S⟧) ⊢δ
                                ; OT-rel = helper′
                                }
              where
                ⊢δ′ = ⊢w⇒⊢s ⊢δ

                helper′ :  {s a} 
                          Δ′  s  S [ σ ] [ δ ] ®[ i ] a ∈El S∈𝕌 
                          (a∈ : a ∈′ El _ S∈𝕌) 
                          Δ′  T [ q σ ] [ δ , s ] ®[ i ] ΠRT.T≈T′ (ΠRTT a∈)
                helper′ {s} {a} s∼a a∈
                  with gS (s®-mon ⊩Γ₁ ⊢δ (s®-irrel ⊩Γ ⊩Γ₁ σ∼ρ)) | s®-cons (⊩∷ ⊩Γ₁ ⊢S₁ gS) {t = s} {a} (s®-mon ⊩Γ₁ ⊢δ (s®-irrel ⊩Γ ⊩Γ₁ σ∼ρ))
                ...  | record { ↘⟦T⟧ = ↘⟦S⟧₁ ; T∈𝕌 = S∈𝕌₁ ; T∼⟦T⟧ = S∼⟦S⟧₁ }
                     | f
                    rewrite ⟦⟧-det ↘⟦S⟧₁ ↘⟦S⟧
                      with ΠRTT a∈
                         | Tkrip₁ (f (®El-master S∈𝕌 S∈𝕌₁ S∈𝕌 S∼⟦S⟧₁ s∼a ([∘]-Se ⊢S ⊢σ ⊢δ′)))
                ...      | record { ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ }
                         | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦t⟧ = ↘⟦T⟧₁ ; T∈𝕌 = U i<lvl₁ _ ; t∼⟦t⟧ = T∼⟦T⟧₁ }
                        rewrite Glu-wellfounded-≡ i<lvl₁
                              | ⟦⟧-det ↘⟦T⟧₁ ↘⟦T⟧
                          with T∼⟦T⟧₁
                ...          | record { A∈𝕌 = T∈𝕌 ; rel = rel } = ®-one-sided T∈𝕌 T≈T′ (®-resp-≈ T∈𝕌 rel T[σ∘δ,s]≈T[σ∘wk,v0][δ,s])
                  where
                    T[σ∘δ,s]≈T[σ∘wk,v0][δ,s] : Δ′  T [ (σ  δ) , s ]  T [ (σ  wk) , v 0 ] [ δ , s ]  Se i
                    T[σ∘δ,s]≈T[σ∘wk,v0][δ,s] =
                      begin T [ (σ  δ) , s ]                ≈˘⟨ []-cong-Se″ ⊢T (q∘,≈∘, ⊢σ ⊢S ⊢δ′ ⊢s) 
                            T [ ((σ  wk) , v 0)  (δ , s) ] ≈˘⟨ [∘]-Se
                                                                    ⊢T
                                                                    (s-,
                                                                       (s-∘ (s-wk ⊢S[σ]Δ) ⊢σ)
                                                                       ⊢S
                                                                       (conv (vlookup ⊢S[σ]Δ here) ([∘]-Se ⊢S ⊢σ (s-wk ⊢S[σ]Δ))))
                                                                    (s-, ⊢δ′ (t[σ]-Se ⊢S ⊢σ) ⊢s) 
                            T [ (σ  wk) , v 0 ] [ δ , s ]   
                      where
                        open ER

                        ⊢s = ®El⇒tm S∈𝕌 s∼a
                        ⊢S[σ]Δ = ⊢∷ ⊢Δ (t[σ]-Se ⊢S ⊢σ)

Λ-I′ : S  Γ  t  T 
       ------------------
       Γ  Λ t  Π S T
Λ-I′ {S} {Γ} {t} {T} ⊩t
  with ⊩t | ⊩⇒⊢-both ⊩t
...  | record { ⊩Γ = (⊩∷ {i = lvl} ⊩Γ ⊢S gS) ; lvl = lvl₁ ; krip = tkrip₁ }
     | ⊢T , ⊢t
    with fundamental-⊢t ⊢T | fundamental-⊢t ⊢t
...    | ∷-cong ⊨Γ₁ Srel₁ , n₁ , Trel₁
       | ∷-cong ⊨Γ₂ Srel₂ , n₂ , trel₂ = record { ⊩Γ = ⊩Γ ; krip = krip }
  where
    krip :  {Δ σ ρ} 
           Δ ⊢s σ  ⊩Γ ® ρ 
           GluExp (max lvl lvl₁) Δ (Λ t) (Π S T) σ ρ
    krip {Δ} {σ} {ρ} σ∼ρ
      with gS σ∼ρ | s®⇒⟦⟧ρ ⊩Γ σ∼ρ
    ...  | record { ⟦T⟧ = ⟦S⟧ ; ↘⟦T⟧ = ↘⟦S⟧ ; T∈𝕌 = S∈𝕌 ; T∼⟦T⟧ = S∼⟦S⟧ }
         | ⊨Γ , ρ∈ = record
                     { ↘⟦T⟧ = ⟦Π⟧ ↘⟦S⟧
                     ; ↘⟦t⟧ = ⟦Λ⟧ t
                     ; T∈𝕌 = Π S∈𝕌′ ΠRTT
                     ; t∼⟦t⟧ = record
                               { t∶T = t[σ] (Λ-I ⊢t) ⊢σ
                               ; a∈El = Λt∈′El
                               ; ⊢OT = t[σ]-Se ⊢T′ (⊢q ⊢σ ⊢S)
                               ; T≈ = Π-[] ⊢σ ⊢S′ ⊢T′
                               ; krip = Λrel
                               }
                     }
      where
        S∈𝕌′ = 𝕌-cumu (m≤m⊔n lvl lvl₁) S∈𝕌
        ⊢σ   = s®⇒⊢s ⊩Γ σ∼ρ
        ⊢Δ   = proj₁ (presup-s ⊢σ)
        ⊢S′  = lift-⊢-Se-max ⊢S
        ⊢T′  = lift-⊢-Se-max′ ⊢T

        ΠRTT : {a a′ : D} 
               a  a′  El _ S∈𝕌′ 
               ΠRT T (ρ  a) T (ρ  a′) (𝕌 (max lvl lvl₁))
        ΠRTT {a} {a′} a≈a′ = helper
          where
            ρ≈′ : ρ ∈′  ⊨Γ₁ ⟧ρ
            ρ≈′ = ⊨-irrel ⊨Γ ⊨Γ₁ ρ∈

            a≈a′₁ : a  a′  El _ (RelTyp.T≈T′ (Srel₁ ρ≈′))
            a≈a′₁
              with Srel₁ ρ≈′
            ...  | record { ↘⟦T⟧ = ↘⟦S⟧₁ ; ↘⟦T′⟧ = ↘⟦S′⟧₁ ; T≈T′ = S≈S′ }
                rewrite ⟦⟧-det ↘⟦S⟧₁ ↘⟦S⟧ = El-one-sided S∈𝕌′ S≈S′ a≈a′

            helper : ΠRT T (ρ  a) T (ρ  a′) (𝕌 (max lvl lvl₁))
            helper
              with Trel₁ (ρ≈′ , a≈a′₁)
            ...  | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦T′⟧ = ⟦Se⟧ _ ; T≈T′ = U i<n₁ _ }
                 , record { ↘⟦t⟧ = ↘⟦T⟧ ; ↘⟦t′⟧ = ↘⟦T′⟧ ; t≈t′ = T≈T′ }
                rewrite 𝕌-wellfounded-≡-𝕌 _ i<n₁ = record
                                                   { ↘⟦T⟧ = ↘⟦T⟧
                                                   ; ↘⟦T′⟧ = ↘⟦T′⟧
                                                   ; T≈T′ = 𝕌-cumu (m≤n⊔m _ _) T≈T′
                                                   }

        Λt∈′El : {a a′ : D} (a≈a′ : a  a′  El _ S∈𝕌′) 
                 Π̂ (Λ t ρ) a (Λ t ρ) a′ (El _ (ΠRT.T≈T′ (ΠRTT a≈a′)))
        Λt∈′El {a} {a′} a≈a′ = helper
          where
            ρ≈″ : ρ ∈′  ⊨Γ₂ ⟧ρ
            ρ≈″ = ⊨-irrel ⊨Γ ⊨Γ₂ ρ∈

            a≈a′₂ : a  a′  El _ (RelTyp.T≈T′ (Srel₂ ρ≈″))
            a≈a′₂
              with Srel₂ ρ≈″
            ...  | record { ↘⟦T⟧ = ↘⟦S⟧₂ ; ↘⟦T′⟧ = ↘⟦S′⟧₂ ; T≈T′ = S≈S′ }
                rewrite ⟦⟧-det ↘⟦S⟧₂ ↘⟦S⟧ = El-one-sided S∈𝕌′ S≈S′ a≈a′

            helper : Π̂ (Λ t ρ) a (Λ t ρ) a′ (El _ (ΠRT.T≈T′ (ΠRTT a≈a′)))
            helper
              with ΠRTT a≈a′
                 | trel₂ (ρ≈″ , a≈a′₂)
            ...  | record { ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ }
                 | record { ↘⟦T⟧ = ↘⟦T⟧₂ ; ↘⟦T′⟧ = ↘⟦T′⟧₂ ; T≈T′ = T≈T′₂ }
                 , record { ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦t′⟧ = ↘⟦t′⟧ ; t≈t′ = t≈t′ }
                    rewrite ⟦⟧-det ↘⟦T⟧ ↘⟦T⟧₂
                          | ⟦⟧-det ↘⟦T′⟧ ↘⟦T′⟧₂ = record { ↘fa = Λ∙ ↘⟦t⟧ ; ↘fa′ = Λ∙ ↘⟦t′⟧ ; fa≈fa′ = 𝕌-irrel T≈T′₂ T≈T′ t≈t′ }

        Λrel :  {Δ′ δ} 
                 Δ′ ⊢w δ  Δ 
                 ΛRel (max lvl lvl₁) Δ′ (Λ t [ σ ]) (S [ σ ]) (T [ q σ ]) δ (Λ t ρ) S∈𝕌′
                   (_⊢_®[ max lvl lvl₁ ] S∈𝕌′)
                   (_⊢_∶_®[ max lvl lvl₁ ]_∈El S∈𝕌′)
                    a∈  _⊢_∶_®[ max lvl lvl₁ ]_∈El ΠRT.T≈T′ (ΠRTT a∈))
        Λrel {Δ′} {δ} ⊢δ = record
                  { IT-rel = ®-mon S∈𝕌′ S∈𝕌′ (®-cumu S∈𝕌 S∼⟦S⟧ (m≤m⊔n _ _)) ⊢δ
                  ; ap-rel = helper
                  }
          where
            ⊢δ′ = ⊢w⇒⊢s ⊢δ
            ⊢Δ′ = proj₁ (presup-s ⊢δ′)

            helper :  {s a} 
                     Δ′  s  S [ σ ] [ δ ] ®[ max lvl lvl₁ ] a ∈El S∈𝕌′ 
                     (a∈ : a ∈′ El _ S∈𝕌′) 
                     ΛKripke Δ′ (Λ t [ σ ] [ δ ] $ s) (T [ q σ ] [ δ , s ]) (Λ t ρ) a (_⊢_∶_®[ max lvl lvl₁ ]_∈El ΠRT.T≈T′ (ΠRTT a∈))
            helper {s} {a} s∼a a∈
              with gS (s®-mon ⊩Γ ⊢δ σ∼ρ) | s®-cons (⊩∷ ⊩Γ ⊢S gS) {t = s} {a} (s®-mon ⊩Γ ⊢δ σ∼ρ)
            ...  | record { ↘⟦T⟧ = ↘⟦S⟧₁ ; T∈𝕌 = S∈𝕌₁ ; T∼⟦T⟧ = S∼⟦S⟧₁ }
                 | f
                rewrite ⟦⟧-det ↘⟦S⟧₁ ↘⟦S⟧
                  with ΠRTT a∈
                     | tkrip₁ (f (®El-master S∈𝕌′ S∈𝕌₁ S∈𝕌′ S∼⟦S⟧₁ s∼a ([∘]-Se ⊢S′ ⊢σ ⊢δ′)))
            ...      | record { ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ }
                     | record { ↘⟦T⟧ = ↘⟦T⟧₁ ; ↘⟦t⟧ = ↘⟦t⟧₁ ; T∈𝕌 = T∈𝕌₁ ; t∼⟦t⟧ = t∼⟦t⟧₁ }
                    rewrite ⟦⟧-det ↘⟦T⟧₁ ↘⟦T⟧ = record { ↘fa = Λ∙ ↘⟦t⟧₁ ; ®fa = ®El-one-sided T∈𝕌₁′ T≈T′ (®El-resp-T≈ T∈𝕌₁′ (®El-resp-≈ T∈𝕌₁′ (®El-cumu T∈𝕌₁ t∼⟦t⟧₁ (m≤n⊔m _ _)) t[σ∘δ,s]≈Λt[σ][δ]$s) ([]-q-∘-, ⊢T′ ⊢σ ⊢δ′ ⊢s)) }
              where
                T∈𝕌₁′ = 𝕌-cumu (m≤n⊔m lvl lvl₁) T∈𝕌₁
                ⊢s = ®El⇒tm S∈𝕌′ s∼a
                ⊢σ∘δ = s-∘ ⊢δ′ ⊢σ
                ⊢s′ = conv ⊢s ([∘]-Se ⊢S ⊢σ ⊢δ′)
                ⊢s″ = conv ⊢s′ ([]-cong-Se″ ⊢S (s-≈-sym (∘-I ⊢σ∘δ)))

                t[σ∘δ,s]≈Λt[σ][δ]$s : Δ′  t [ (σ  δ) , s ]  Λ t [ σ ] [ δ ] $ s  T [ (σ  δ) , s ]
                t[σ∘δ,s]≈Λt[σ][δ]$s =
                  begin t [ (σ  δ) , s ]        ≈˘⟨ ≈-conv ([]-cong (≈-refl ⊢t) (,-cong (∘-I ⊢σ∘δ) ⊢S (≈-refl ⊢s″))) ([]-cong-Se″ ⊢T (,-cong (∘-I ⊢σ∘δ) ⊢S (≈-refl ⊢s″))) 
                        t [ ((σ  δ)  I) , s ]  ≈˘⟨ ≈-conv ([]-q-, ⊢σ∘δ ⊢S (s-I ⊢Δ′) (conv ⊢s′ (≈-sym ([I] (t[σ]-Se ⊢S ⊢σ∘δ)))) ⊢t) ([]-cong-Se″ ⊢T (,-cong (∘-I ⊢σ∘δ) ⊢S (≈-refl ⊢s″))) 
                        t [ q (σ  δ) ] [| s ]   ≈⟨ ≈-conv t[q[σ∘δ]][|s]≈Λt[σ][δ]$s (≈-sym ([]-q-∘-,′ ⊢T ⊢σ∘δ ⊢s′)) 
                        Λ t [ σ ] [ δ ] $ s      
                  where
                    open ER

                    t[q[σ∘δ]][|s]≈Λt[σ][δ]$s : Δ′  t [ q (σ  δ) ] [| s ]  Λ t [ σ ] [ δ ] $ s  T [ q (σ  δ) ] [| s ]
                    t[q[σ∘δ]][|s]≈Λt[σ][δ]$s =
                      begin t [ q (σ  δ) ] [| s ]  ≈˘⟨ Λ-β (t[σ] ⊢t (⊢q ⊢σ∘δ ⊢S)) ⊢s′ 
                            Λ (t [ q (σ  δ) ]) $ s ≈˘⟨ $-cong (≈-conv (Λ-[] ⊢σ∘δ ⊢t) (Π-[] ⊢σ∘δ ⊢S′ ⊢T′)) (≈-refl ⊢s′) 
                            Λ t [ σ  δ ] $ s       ≈⟨ $-cong (≈-conv ([∘] ⊢δ′ ⊢σ (Λ-I ⊢t)) (Π-[] ⊢σ∘δ ⊢S′ ⊢T′)) (≈-refl ⊢s′) 
                            Λ t [ σ ] [ δ ] $ s     


Λ-E′ :  {i} 
       S  Γ  T  Se i 
       Γ  r  Π S T 
       Γ  s  S 
       ---------------------
       Γ  r $ s  T [| s ]
Λ-E′ {S} {_} {T} {r} {s} {i} ⊩T@record { ⊩Γ = ⊩SΓ@(⊩∷ {i = j} ⊩Γ ⊢S Skrip) ; krip = Tkrip } ⊩r ⊩s = record
  { ⊩Γ   = ⊩Γ
  ; lvl  = i
  ; krip = helper
  }
  where module r = _⊩_∶_ ⊩r
        module s = _⊩_∶_ ⊩s
        ⊢T = ⊩⇒⊢-tm ⊩T
        ⊢w = ⊩⇒⊢-tm ⊩r
        ⊢s = ⊩⇒⊢-tm ⊩s

        helper : Δ ⊢s σ  ⊩Γ ® ρ  GluExp i Δ (r $ s) (T [| s ]) σ ρ
        helper {Δ} {σ} {ρ} σ∼ρ
          with s®⇒⊢s ⊩Γ σ∼ρ | s.krip (s®-irrel ⊩Γ s.⊩Γ σ∼ρ) | r.krip (s®-irrel ⊩Γ r.⊩Γ σ∼ρ)
        ...  | ⊢σ
             | record { ⟦T⟧ = ⟦S⟧ ; ⟦t⟧ = ⟦s⟧ ; ↘⟦T⟧ = ↘⟦S⟧ ; ↘⟦t⟧ = ↘⟦s⟧ ; T∈𝕌 = S∈𝕌 ; t∼⟦t⟧ = s∼⟦s⟧ }
             | record { ⟦T⟧ = .(Π _ T ρ) ; ⟦t⟧ = ⟦r⟧ ; ↘⟦T⟧ = ⟦Π⟧ ↘⟦S⟧′ ; ↘⟦t⟧ = ↘⟦r⟧ ; T∈𝕌 = Π iA RT ; t∼⟦t⟧ = r∼⟦r⟧ }
             rewrite ⟦⟧-det ↘⟦S⟧′ ↘⟦S⟧
             with Skrip σ∼ρ | s®-cons ⊩SΓ σ∼ρ
        ...     | record { ↘⟦T⟧ = ↘⟦S⟧″ ; T∈𝕌 = S∈𝕌′ ; T∼⟦T⟧ = S∼⟦S⟧ } | cons
                rewrite ⟦⟧-det ↘⟦S⟧″ ↘⟦S⟧
                with Tkrip (cons (®El-irrel S∈𝕌 S∈𝕌′ S∼⟦S⟧ s∼⟦s⟧))
        ...        | record { ⟦t⟧ = ⟦T⟧ ; ↘⟦T⟧ = ⟦Se⟧ .i ; ↘⟦t⟧ = ↘⟦T⟧ ; T∈𝕌 = U i< _ ; t∼⟦t⟧ = T∼⟦T⟧ }
                   rewrite Glu-wellfounded-≡ i< = help
          where ⊢Δ = proj₁ (presup-s ⊢σ)
                module Λ where
                  open GluΛ r∼⟦r⟧ public
                  open ΛRel (krip (⊢wI ⊢Δ)) public

                  ⊢IT : Δ  IT  Se _
                  ⊢IT = ®Π-wf iA RT (®El⇒® (Π iA RT) r∼⟦r⟧)

                module U = GluU T∼⟦T⟧

                pair : Δ  S [ σ ]  Λ.IT [ I ]  Se (max j r.lvl) × Δ  s [ σ ]  Λ.IT [ I ] ®[ r.lvl ] ⟦s⟧ ∈El iA
                pair
                  with Λ.IT-rel
                ...  | IT-rel = eq , ®El-master S∈𝕌 iA Rcumu IT-rel s∼⟦s⟧ eq
                  where Rcumu = 𝕌-cumu (m≤n⊔m j r.lvl) iA
                        eq    = ®⇒≈ Rcumu
                                    (®-one-sided (𝕌-cumu (m≤m⊔n j r.lvl) S∈𝕌′) Rcumu (®-cumu S∈𝕌′ S∼⟦S⟧ (m≤m⊔n j r.lvl)))
                                    (®-cumu iA IT-rel (m≤n⊔m j r.lvl))

                eq₁ : Δ  S [ σ ]  Λ.IT [ I ]  Se (max j r.lvl)
                eq₁ = proj₁ pair
                s∼a : Δ  s [ σ ]  Λ.IT [ I ] ®[ r.lvl ] ⟦s⟧ ∈El iA
                s∼a = proj₂ pair

                a∈ : ⟦s⟧ ∈′ El r.lvl iA
                a∈ = ®El⇒∈El iA s∼a

                help : GluExp i Δ (r $ s) (T [| s ]) σ ρ
                help
                  with Λ.ap-rel s∼a a∈
                ...  | record { fa = fa ; ↘fa = ↘fa ; ®fa = ®fa }
                     with RT a∈
                ...     | record { ↘⟦T⟧ = ↘⟦T⟧′ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ }
                        rewrite ⟦⟧-det ↘⟦T⟧′ ↘⟦T⟧
                              | ⟦⟧-det ↘⟦T′⟧ ↘⟦T⟧ = record
                  { ⟦T⟧   = ⟦T⟧
                  ; ⟦t⟧   = fa
                  ; ↘⟦T⟧  = ⟦[]⟧ (⟦,⟧ ⟦I⟧ ↘⟦s⟧) ↘⟦T⟧
                  ; ↘⟦t⟧  = ⟦$⟧ ↘⟦r⟧ ↘⟦s⟧ ↘fa
                  ; T∈𝕌   = U.A∈𝕌
                  ; t∼⟦t⟧ = ®El-master T≈T′ U.A∈𝕌 A∈k T∼A (®El-resp-≈ T≈T′ ®fa eq₃) eq₂
                  }
                    where open ER
                          T∼A : Δ  T [| s ] [ σ ] ®[ i ] U.A∈𝕌
                          T∼A = ®-resp-≈ U.A∈𝕌 U.rel (≈-sym ([]-I,-∘ ⊢T ⊢σ ⊢s))

                          k   = max i r.lvl
                          i≤k = m≤m⊔n i r.lvl
                          l≤k = m≤n⊔m i r.lvl
                          A∈k = 𝕌-cumu i≤k U.A∈𝕌

                          eq₂ : Δ  Λ.OT [ I , s [ σ ] ]  T [| s ] [ σ ]  Se _
                          eq₂ = ®⇒≈ A∈k (®-one-sided (𝕌-cumu l≤k T≈T′) A∈k (®-cumu T≈T′ (®El⇒® T≈T′ ®fa) l≤k)) (®-cumu U.A∈𝕌 T∼A i≤k)

                          eq₃ : Δ  r [ σ ] [ I ] $ s [ σ ]  (r $ s) [ σ ]  Λ.OT [| s [ σ ] ]
                          eq₃ = begin
                            r [ σ ] [ I ] $ s [ σ ] ≈⟨ $-cong ([I] (conv (t[σ] ⊢w ⊢σ) Λ.T≈)) (≈-refl (conv (t[σ] ⊢s ⊢σ) (≈-sym ([I]-≈ˡ-Se (≈-sym eq₁))))) 
                            r [ σ ] $ s [ σ ]       ≈˘⟨ ≈-conv ($-[] ⊢σ ⊢w ⊢s) (≈-sym (≈-trans eq₂ ([]-I,-∘ (lift-⊢-Se-max ⊢T) ⊢σ ⊢s))) 
                            (r $ s) [ σ ]