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

open import Level hiding (_⊔_)
open import Axiom.Extensionality.Propositional

-- Properties of the gluing models for terms and types
module NonCumulative.Soundness.Properties.Bundle (fext :  {ℓ₁ ℓ₂}  Extensionality ℓ₁ ℓ₂) where

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

open import NonCumulative.Semantics.Properties.PER (fext)
open import NonCumulative.Soundness.LogRel
open import NonCumulative.Soundness.Properties.LogRel (fext)

-- this set of lemmas re-tie the knots to change all the Univ and Glu to their standard forms
-- i.e., 𝕌-wellfounded _ and Glu-wellfounded _

®-Π-𝕌 :  {i j k} 
  (i≡maxjk : i  max j k) 
  (jA : A  A′  𝕌 j) 
  (RT :  {a a′} 
    a  a′  El j jA 
    ΠRT S (ρ  a) S′ (ρ′  a′) (𝕌 k)) 
  (iA : Π j A (S  k) ρ  Π j A′ (S′  k) ρ′  𝕌 i) 
  GluΠ i j k Γ T (𝕌-wellfounded j) jA  (_⊢_®[ j ] jA)  a∈  _⊢_®[ k ] (ΠRT.T≈T′ (RT a∈))) (_⊢_∶_®[ j ]_∈El jA) 
  Γ  T ®[ i ] iA
®-Π-𝕌 {j = j} {k = k} refl jA RT (Π i≡maxjk jA′ RT′ _ _) 
  rewrite 𝕌-wf-gen j (ΠI≤ i≡maxjk)
        | 𝕌-wf-gen k (ΠO≤ i≡maxjk)
        | Glu-wf-gen j (ΠI≤ i≡maxjk)
        | Glu-wf-gen k (ΠO≤ i≡maxjk) = record
    { IT = _
    ; OT = _
    ; ⊢IT = ⊢IT
    ; ⊢OT = ⊢OT
    ; T≈ = T≈
    ; krip = λ ⊢σ  let open ΠRel (krip ⊢σ) in record
      { IT-rel = ®-≡ jA jA′ IT-rel refl
      ; OT-rel = λ  a∈  OT-helper a∈  OT-rel
      }
    }
    where
      open GluΠ 
      OT-helper : (a∈′ : a ∈′ El j jA′) 
                  Δ  s  IT [ σ ] ®[ j ] a ∈El jA′ 
                  (∀ {s a}  Δ  s  IT [ σ ] ®[ j ] a ∈El jA 
                    (a∈ : a ∈′ El j jA) 
                    Δ  OT [ σ , s  IT  j ] ®[ k ] ΠRT.T≈T′ (RT a∈)) 
                  --------------------------------------------------------------
                  Δ  OT [ σ , s  IT  j ] ®[ k ] ΠRT.T≈T′ (RT′ a∈′)
      OT-helper a∈′  OT-rel
        with El-one-sided jA′ jA a∈′
      ... | a∈
          with RT a∈ | RT′ a∈′ | OT-rel (®El-one-sided jA′ jA ) a∈
      ...    | record { ⟦T⟧ = ⟦T⟧ ; ↘⟦T⟧ = ↘⟦T⟧ ; T≈T′ = T≈T′ }
              | record { ↘⟦T⟧ = ↘⟦T⟧′ ; T≈T′ = T≈T′₁ }
              | R
            rewrite ⟦⟧-det ↘⟦T⟧′ ↘⟦T⟧ = ®-one-sided T≈T′ T≈T′₁ R

®-L-𝕌 :  {i j k} 
  (kA : A  A′  𝕌 k) 
  (iA : Li j k A  Li j k A′  𝕌 i) 
  (GluL i j k Γ T (_⊢_®[ k ] kA)) 
  Γ  T ®[ i ] iA
®-L-𝕌 {j = j} {k = k} kA (L i≡j+k kA′ _ _) 
  rewrite 𝕌-wf-gen k (Li≤ i≡j+k)
        | Glu-wf-gen k (Li≤ i≡j+k) = record
  { UT = UT
  ; ⊢UT = ⊢UT
  ; T≈ = T≈
  ; krip = λ ⊢σ  ®-≡ kA kA′ (krip ⊢σ) refl
  }
  where open GluL 

®El-𝕌-𝕌 :   {j}
  (jA : A  A′  𝕌 j) 
  (iA : U j ∈′ 𝕌 (1 + j)) 
  (GluU j (1 + j) Γ t T a (𝕌-wellfounded j)  a∈  Γ  t ®[ j ] a∈)) 
  Γ  t  T ®[ 1 + j ] a ∈El iA
®El-𝕌-𝕌 jA (U 1+j≡1+j _) record { t∶T = t∶T ; T≈ = T≈ ; A∈𝕌 = A∈𝕌 ; rel = rel }
    rewrite Glu-wellfounded-≡ (≤-reflexive (sym 1+j≡1+j)) = record
  { t∶T = t∶T
  ; T≈ = T≈
  ; A∈𝕌 = A∈𝕌
  ; rel = rel
  }

®El-Π-𝕌 :  {i j k} 
  (i≡maxjk : i  max j k) 
  (jA : A  A′  𝕌 j) 
  (RT :  {a a′} 
    a  a′  El j jA 
    ΠRT S (ρ  a) S′ (ρ′  a′) (𝕌 k)) 
  (iA : Π j A (S  k) ρ  Π j A′ (S′  k) ρ′  𝕌 i) 
  GluΛ i j k Γ t T a _ _ jA RT (_⊢_®[ j ] jA) (_⊢_∶_®[ j ]_∈El jA)  a∈  _⊢_∶_®[ k ]_∈El (ΠRT.T≈T′ (RT a∈))) 
  Γ  t  T ®[ i ] a ∈El iA
®El-Π-𝕌 {j = j} {k = k} refl jA RT (Π i≡maxjk jA′ RT′ _ _) 
  rewrite 𝕌-wf-gen j (ΠI≤ i≡maxjk)
        | 𝕌-wf-gen k (ΠO≤ i≡maxjk)
        | Glu-wf-gen j (ΠI≤ i≡maxjk)
        | Glu-wf-gen k (ΠO≤ i≡maxjk) = record
    { t∶T = t∶T
    ; a∈El = El-Π-𝕌 i≡maxjk jA′ RT′ (𝕌-irrel (proj₁ Π-bund) (Π-𝕌 jA′ RT′ i≡maxjk) (proj₂ Π-bund))
    ; IT = _
    ; OT = _
    ; ⊢IT = ⊢IT
    ; ⊢OT = ⊢OT
    ; T≈ = T≈
    ; krip = λ ⊢τ  let open ΛRel (krip ⊢τ) in record
      { IT-rel = ®-≡ jA jA′ IT-rel refl
      ; ap-rel = λ  b∈  helper b∈  ap-rel
      }
    }
  where
    open GluΛ 
    Π-bund = Π-bundle jA  a≈a′  RT a≈a′ , a∈El a≈a′) refl
    helper : (b∈′ : b ∈′ El j jA′) 
             Δ  s  sub IT σ ®[ j ] b ∈El jA′ 
             (∀ {s b}  Δ  s  sub IT σ ®[ j ] b ∈El jA 
               (b∈ : b ∈′ El j jA) 
               ΛKripke Δ (sub t σ $ s) (sub OT (σ , s  IT  j)) a b (_⊢_∶_®[ k ]_∈El ΠRT.T≈T′ (RT b∈))) 
             -----------------------------------------------------------------------------------------
             ΛKripke Δ (sub t σ $ s) (sub OT (σ , s  IT  j)) a b (_⊢_∶_®[ k ]_∈El ΠRT.T≈T′ (RT′ b∈′))
    helper b∈′ s®′ ap-rel with
      𝕌-irrel jA′ jA b∈′ | ®El-≡ jA′ jA s®′ refl
    ... | b∈ | 
      with ap-rel  b∈
    ... | record { fa = fa ; ↘fa = ↘fa ; ®fa = ®fa }
        with RT′ b∈′ | RT b∈
    ... | 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 ↘⟦T′⟧₁ ↘⟦T′⟧ | ⟦⟧-det ↘⟦T⟧₁ ↘⟦T⟧ = record
        { fa = _
        ; ↘fa = ↘fa
        ; ®fa = ®El-≡ _ _ ®fa refl
        }

®El-Li-𝕌 :  {i j k}
    (i≡j+k : i  j + k) 
    (kA : A  A′  𝕌 k) 
    (iA : Li j k A  Li j k A′  𝕌 i) 
    (Glul i j _ Γ t T a (𝕌-wellfounded k) kA (_⊢_∶_®[ k ]_∈El kA)) 
    Γ  t  T ®[ i ] a ∈El iA
®El-Li-𝕌 {j = j} {k = k} refl kA iA 
  with iA
... | L i≡j+k kA′ _ _
  rewrite 𝕌-wf-gen k (Li≤ i≡j+k)
        | Glu-wf-gen k (Li≤ i≡j+k) = record
    { t∶T = t∶T
    ; UT = UT
    ; ⊢UT = ⊢UT
    ; a∈El = El-L-𝕌 kA′ i≡j+k (𝕌-irrel (proj₁ L-bund) (L-𝕌 kA′ i≡j+k) (proj₂ L-bund))
    ; T≈ = T≈
    ; krip = λ ⊢τ  let module lkrip = lKripke (krip ⊢τ) in record
        { ua = lkrip.ua
        ; ↘ua = lkrip.↘ua
        ; ®ua = ®El-≡ kA kA′ lkrip.®ua refl
        }
    }
  where
    open Glul 
    L-bund = L-bundle {j = j} kA a∈El refl