module Generic.Fusion where

open import Size
open import Data.Sum
open import Data.List hiding ([_] ; zip ; lookup)
open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])

open import indexed
open import rel
open import var hiding (_<$>_)
open import varlike
open import environment

open import Generic.Syntax
open import Generic.Semantics
open import Generic.Zip
open import Generic.Simulation using (reify^R ; vl^VarTm)
open import Generic.Identity

module _  {I : Set} {π“₯₁ π“₯β‚‚ π“₯₃ 𝓒₁ 𝓒₂ 𝓒₃ : I β†’ List I β†’ Set}
          (𝓑^E : {Ξ“ Ξ” Θ : List I} β†’ (Ξ“ ─Env) π“₯₁ Ξ” β†’ (Ξ” ─Env) π“₯β‚‚ Θ β†’ (Ξ“ ─Env) π“₯₃ Θ β†’ Set)
          (𝓑^π“₯  : Rel π“₯β‚‚ π“₯₃)
          (𝓑^𝓒   : Rel 𝓒₂ 𝓒₃)
          where

 record Fus (d : Desc I) (𝓒₁ : Sem d π“₯₁ 𝓒₁) (𝓒₂ : Sem d π“₯β‚‚ 𝓒₂) (𝓒₃ : Sem d π“₯₃ 𝓒₃) : Set where
   field

     quote₁  :  (i : I) β†’ [ 𝓒₁ i ⟢ Tm d ∞ i ]

     vl^π“₯₁   :  VarLike π“₯₁

     th^R    :  {Ξ“ Ξ” Θ Ξ : List I} {ρ₁ : (Ξ“ ─Env) π“₯₁ Ξ”} {ρ₂ : (Ξ” ─Env) π“₯β‚‚ Θ} {ρ₃ : (Ξ“ ─Env) π“₯₃ Θ} β†’ (Οƒ : Thinning Θ Ξ) β†’ 𝓑^E ρ₁ ρ₂ ρ₃ β†’
                𝓑^E ρ₁ (th^Env (Sem.th^π“₯ 𝓒₂) ρ₂ Οƒ) (th^Env (Sem.th^π“₯ 𝓒₃) ρ₃ Οƒ)

     >>^R    :  {Ξ“ Ξ” Θ Ξ : List I} {ρ₁ : (Ξ“ ─Env) π“₯₁ Ξ”} {ρ₂ : (Ξ” ─Env) π“₯β‚‚ Θ} {ρ₃ : (Ξ“ ─Env) π“₯₃ Θ} {ρ₄ : (Ξ ─Env) π“₯β‚‚ Θ} {ρ₅ : (Ξ ─Env) π“₯₃ Θ} β†’ 𝓑^E ρ₁ ρ₂ ρ₃ β†’ βˆ€[ 𝓑^π“₯ ] ρ₄ ρ₅ β†’
                𝓑^E (freshΛ‘ vl^π“₯₁ Ξ” {Ξ} >> th^Env (Sem.th^π“₯ 𝓒₁) ρ₁ (freshΚ³ vl^Var Ξ)) (ρ₄ >> ρ₂) (ρ₅ >> ρ₃)

     var^R   :  {Ξ“ Ξ” Θ : List I} {i : I} {ρ₁ : (Ξ“ ─Env) π“₯₁ Ξ”} {ρ₂ : (Ξ” ─Env) π“₯β‚‚ Θ} {ρ₃ : (Ξ“ ─Env) π“₯₃ Θ} β†’ 𝓑^E ρ₁ ρ₂ ρ₃ β†’ (v : Var i Ξ“) β†’
                rel 𝓑^𝓒  (Sem.sem 𝓒₂ ρ₂ (quote₁ i (Sem.var 𝓒₁ (lookup ρ₁ v))))
                           (Sem.var 𝓒₃ (lookup ρ₃ v))

     alg^R   :  {Ξ“ Ξ” Θ : List I} {s : Size} {i : I} {ρ₁ : (Ξ“ ─Env) π“₯₁ Ξ”} {ρ₂ : (Ξ” ─Env) π“₯β‚‚ Θ} {ρ₃ : (Ξ“ ─Env) π“₯₃ Θ} β†’ (b : ⟦ d ⟧ (Scope (Tm d s)) i Ξ“) β†’ 𝓑^E ρ₁ ρ₂ ρ₃ β†’
                let  v₁ = fmap d (Sem.body 𝓒₁ ρ₁) b
                     v₃ = fmap d (Sem.body 𝓒₃ ρ₃) b
                in Zip d (Kripke^R 𝓑^π“₯ 𝓑^𝓒)
                    (fmap d (Ξ» Ξ” i β†’ Sem.body 𝓒₂ ρ₂ Ξ” i ∘ quote₁ i ∘ reify vl^π“₯₁ Ξ” i) v₁)
                    v₃ β†’
                rel 𝓑^𝓒 (Sem.sem 𝓒₂ ρ₂ (quote₁ i (Sem.alg 𝓒₁ v₁))) (Sem.alg 𝓒₃ v₃)



   fus  :  {s : Size} {i : I} {Ξ“ Ξ” Θ : List I} {ρ₁ : (Ξ“ ─Env) π“₯₁ Ξ”} {ρ₂ : (Ξ” ─Env) π“₯β‚‚ Θ} {ρ₃ : (Ξ“ ─Env) π“₯₃ Θ} β†’ 𝓑^E ρ₁ ρ₂ ρ₃ β†’ (t : Tm d s i Ξ“) β†’ rel 𝓑^𝓒  (Sem.sem 𝓒₂ ρ₂ (quote₁ i (Sem.sem 𝓒₁ ρ₁ t)))
                                                                                                                                                           (Sem.sem 𝓒₃ ρ₃ t)
   body :  {s : Size} {Ξ“ Θ Ξ : List I} {ρ₁ : (Ξ“ ─Env) π“₯₁ Θ} {ρ₂ : (Θ ─Env) π“₯β‚‚ Ξ} {ρ₃ : (Ξ“ ─Env) π“₯₃ Ξ} β†’ 𝓑^E ρ₁ ρ₂ ρ₃ β†’ (Ξ” : List I) (i : I) (b : Scope (Tm d s) Ξ” i Ξ“) β†’
           Kripke^R 𝓑^π“₯ 𝓑^𝓒 Ξ” i   (Sem.body 𝓒₂ ρ₂ Ξ” i (quote₁ i (reify vl^π“₯₁ Ξ” i (Sem.body 𝓒₁ ρ₁ Ξ” i b))))
                                  (Sem.body 𝓒₃ ρ₃ Ξ” i b)


   fus ρ^R (`var v) = var^R ρ^R v
   fus ρ^R (`con t) = alg^R t ρ^R (rew (zip d (body ρ^R) t)) where

     eq  = fmapΒ² d (Sem.body 𝓒₁ _) (Ξ» Ξ” i t β†’ Sem.body 𝓒₂ _ Ξ” i (quote₁ i (reify vl^π“₯₁ Ξ” i t))) t
     rew = subst (Ξ» v β†’ Zip d (Kripke^R 𝓑^π“₯ 𝓑^𝓒) v _) (sym eq)

   body ρ^R []       i b = fus ρ^R b
   body ρ^R (Οƒ ∷ Ξ”)  i b = Ξ» ren vs^R β†’ fus (>>^R (th^R ren ρ^R) vs^R) b

module _ {I : Set} (d : Desc I) where

 open ≑-Reasoning

 RenΒ² : Fus (Ξ» ρ₁ β†’ βˆ€[ Eq^R ] ∘ (select ρ₁)) Eq^R Eq^R d Renaming Renaming Renaming
 Fus.quote₁ RenΒ² = Ξ» _ t β†’ t
 Fus.vl^π“₯₁ RenΒ² = vl^Var
 Fus.th^R RenΒ² = Ξ» Οƒ ρ^R β†’ pack^R (Ξ» k β†’ cong (lookup Οƒ) (lookup^R ρ^R k))
 Fus.>>^R RenΒ² {Ξ“} {Ξ”} {Θ} {Ξ} {ρ₁} {ρ₂} {ρ₃} {ρ₄} {ρ₅} = Ξ» ρ^R vs^R β†’ pack^R (aux ρ^R vs^R) where

   aux : βˆ€[ Eq^R ] (select ρ₁ ρ₂) ρ₃ β†’ βˆ€[ Eq^R ] ρ₄ ρ₅ β†’ {i : I} (k : Var i (Ξ ++ Ξ“)) β†’
         [ lookup ρ₄ , lookup ρ₂ ]β€² (split Ξ ([ lookup (freshΛ‘ vl^Var Ξ”) , (lookup (freshΚ³ vl^Var Ξ) βˆ˜β€² (lookup ρ₁)) ]β€² (split Ξ k)))
       ≑ [ lookup ρ₅ , lookup ρ₃ ]β€² (split Ξ k)
   aux ρ^R vs^R k with split Ξ k
   ... | inj₁ kΛ‘ =
     begin
       [ lookup ρ₄ , lookup ρ₂ ] (split Ξ (injectΛ‘ Ξ” (lookup (base vl^Var) kΛ‘)))
           β‰‘βŸ¨ cong [ lookup ρ₄ , lookup ρ₂ ]β€² (split-injectΛ‘ Ξ” (lookup (base vl^Var) kΛ‘)) ⟩
       lookup ρ₄ (lookup (base vl^Var) kΛ‘)
           β‰‘βŸ¨ cong (lookup ρ₄) (lookup-base^Var kΛ‘) ⟩
       lookup ρ₄ kΛ‘
           β‰‘βŸ¨ lookup^R vs^R kΛ‘ ⟩
       lookup ρ₅ kΛ‘
     ∎
   ... | injβ‚‚ kΚ³ =
     begin
       [ lookup ρ₄ , lookup ρ₂ ] (split Ξ (injectΚ³ Ξ (lookup (base vl^Var) (lookup ρ₁ kΚ³))))
           β‰‘βŸ¨ cong [ lookup ρ₄ , lookup ρ₂ ]β€² (split-injectΚ³ Ξ (lookup (base vl^Var) (lookup ρ₁ kΚ³))) ⟩
       lookup ρ₂ (lookup (base vl^Var) (lookup ρ₁ kΚ³))
           β‰‘βŸ¨ cong (lookup ρ₂) (lookup-base^Var (lookup ρ₁ kΚ³)) ⟩
       lookup ρ₂ (lookup ρ₁ kΚ³)
           β‰‘βŸ¨ lookup^R ρ^R kΚ³ ⟩
       lookup ρ₃ kΚ³
     ∎

 Fus.var^R RenΒ² = Ξ» ρ^R v β†’ cong `var (lookup^R ρ^R v)
 Fus.alg^R RenΒ² {ρ₁ = ρ₁} {ρ₂} {ρ₃} b ρ^R = Ξ» zipped β†’ cong `con $
   let v₁ = fmap d (Sem.body Renaming ρ₁) b
       v₃ = fmap d (Sem.body Renaming ρ₃) b in
   begin
     fmap d (reify vl^Var) (fmap d (Sem.body Renaming ρ₂) (fmap d (reify vl^Var) v₁))
         β‰‘βŸ¨ cong (fmap d (reify vl^Var)) (fmapΒ² d (reify vl^Var) (Sem.body Renaming ρ₂) v₁) ⟩
     fmap d (reify vl^Var) (fmap d (Ξ» Ξ¦ i β†’ (Sem.body Renaming ρ₂ Ξ¦ i) ∘ (reify vl^Var Ξ¦ i)) v₁)
         β‰‘βŸ¨ zip^reify Eq^R (reify^R Eq^R Eq^R (vl^Refl vl^Var)) d zipped ⟩
     fmap d (reify vl^Var) v₃
   ∎

 renΒ² : {Ξ“ Ξ” Θ : List I} {i : I} β†’ βˆ€ t (ρ₁ : Thinning Ξ“ Ξ”) (ρ₂ : Thinning Ξ” Θ) β†’
        ren ρ₂ {i = i} (ren ρ₁ t) ≑ ren (select ρ₁ ρ₂) t
 renΒ² t ρ₁ ρ₂ = Fus.fus RenΒ² (pack^R (Ξ» _ β†’ refl)) t

 RenSub : Fus (Ξ» ρ₁ β†’ βˆ€[ Eq^R ] ∘ (select ρ₁)) Eq^R Eq^R d Renaming Substitution Substitution
 Fus.quote₁  RenSub = Ξ» _ t β†’ t
 Fus.vl^π“₯₁  RenSub = vl^Var
 Fus.th^R    RenSub = Ξ» Οƒ ρ^R β†’ pack^R (Ξ» k β†’ cong (ren Οƒ) (lookup^R ρ^R k))
 Fus.>>^R   RenSub {Ξ“} {Ξ”} {Θ} {Ξ} {ρ₁} {ρ₂} {ρ₃} {ρ₄} {ρ₅} = Ξ» ρ^R vs^R β†’ pack^R (aux ρ^R vs^R) where

   aux : βˆ€[ Eq^R ] (select ρ₁ ρ₂) ρ₃ β†’ βˆ€[ Eq^R ] ρ₄ ρ₅ β†’ {i : I} (k : Var i (Ξ ++ Ξ“)) β†’
         [ lookup ρ₄ , lookup ρ₂ ]β€² (split Ξ ([ lookup (freshΛ‘ vl^Var Ξ”) , (lookup (freshΚ³ vl^Var Ξ) βˆ˜β€² (lookup ρ₁)) ]β€² (split Ξ k)))
       ≑ [ lookup ρ₅ , lookup ρ₃ ]β€² (split Ξ k)
   aux ρ^R vs^R k with split Ξ k
   ... | inj₁ kΛ‘ =
     begin
       [ lookup ρ₄ , lookup ρ₂ ] (split Ξ (injectΛ‘ Ξ” (lookup (base vl^Var) kΛ‘)))
           β‰‘βŸ¨ cong [ lookup ρ₄ , lookup ρ₂ ]β€² (split-injectΛ‘ Ξ” (lookup (base vl^Var) kΛ‘)) ⟩
       lookup ρ₄ (lookup (base vl^Var) kΛ‘)
           β‰‘βŸ¨ cong (lookup ρ₄) (lookup-base^Var kΛ‘) ⟩
       lookup ρ₄ kΛ‘
           β‰‘βŸ¨ lookup^R vs^R kΛ‘ ⟩
       lookup ρ₅ kΛ‘
     ∎
   ... | injβ‚‚ kΚ³ =
     begin
       [ lookup ρ₄ , lookup ρ₂ ] (split Ξ (injectΚ³ Ξ (lookup (base vl^Var) (lookup ρ₁ kΚ³))))
           β‰‘βŸ¨ cong [ lookup ρ₄ , lookup ρ₂ ]β€² (split-injectΚ³ Ξ (lookup (base vl^Var) (lookup ρ₁ kΚ³))) ⟩
       lookup ρ₂ (lookup (base vl^Var) (lookup ρ₁ kΚ³))
           β‰‘βŸ¨ cong (lookup ρ₂) (lookup-base^Var (lookup ρ₁ kΚ³)) ⟩
       lookup ρ₂ (lookup ρ₁ kΚ³)
           β‰‘βŸ¨ lookup^R ρ^R kΚ³ ⟩
       lookup ρ₃ kΚ³
     ∎

 Fus.var^R   RenSub = Ξ» ρ^R v β†’ lookup^R ρ^R v
 Fus.alg^R   RenSub {ρ₁ = ρ₁} {ρ₂} {ρ₃} b ρ^R = Ξ» zipped β†’ cong `con $
   let v₁ = fmap d (Sem.body Renaming ρ₁) b
       v₃ = fmap d (Sem.body Substitution ρ₃) b in
   begin
     fmap d (reify vl^Tm) (fmap d (Sem.body Substitution ρ₂) (fmap d (reify vl^Var) v₁))
         β‰‘βŸ¨ cong (fmap d (reify vl^Tm)) (fmapΒ² d (reify vl^Var) (Sem.body Substitution ρ₂) v₁) ⟩
     fmap d (reify vl^Tm) (fmap d (Ξ» Ξ¦ i β†’ (Sem.body Substitution ρ₂ Ξ¦ i) ∘ (reify vl^Var Ξ¦ i)) v₁)
         β‰‘βŸ¨ zip^reify Eq^R (reify^R Eq^R Eq^R (vl^Refl vl^Tm)) d zipped ⟩
      fmap d (reify vl^Tm) v₃
   ∎

 rensub :  {Ξ“ Ξ” Θ : List I} {i : I} β†’ βˆ€ t (ρ₁ : Thinning Ξ“ Ξ”) (ρ₂ : (Ξ” ─Env) (Tm d ∞) Θ) β†’
           sub ρ₂ {i = i} (ren ρ₁ t) ≑ sub (select ρ₁ ρ₂) t
 rensub t ρ₁ ρ₂ = Fus.fus RenSub (pack^R (Ξ» _ β†’ refl)) t


 SubRen : Fus (Ξ» ρ₁ ρ₂ β†’ βˆ€[ Eq^R ] (ren ρ₂ <$> ρ₁)) VarTm^R Eq^R d Substitution Renaming Substitution
 Fus.quote₁  SubRen = Ξ» _ β†’ id
 Fus.vl^π“₯₁  SubRen = vl^Tm
 Fus.th^R    SubRen {ρ₁ = ρ₁} {ρ₂} {ρ₃} = Ξ» Οƒ ρ^R β†’ pack^R $ Ξ» k β†’
   begin
     ren (select ρ₂ Οƒ) (lookup ρ₁ k) β‰‘βŸ¨ sym $ renΒ² (lookup ρ₁ k) ρ₂ Οƒ ⟩
     ren Οƒ (ren ρ₂ (lookup ρ₁ k))    β‰‘βŸ¨ cong (ren Οƒ) (lookup^R ρ^R k) ⟩
     ren Οƒ (lookup ρ₃ k)
   ∎
 Fus.>>^R   SubRen {Ξ“} {Ξ”} {Θ} {Ξ} {ρ₁} {ρ₂} {ρ₃} {ρ₄} {ρ₅} = Ξ» ρ^R vs^R β†’ pack^R (aux ρ^R vs^R) where

   aux : βˆ€[ Eq^R ] (ren ρ₂ <$> ρ₁) ρ₃ β†’ βˆ€[ VarTm^R ] ρ₄ ρ₅ β†’ {i : I} (k : Var i (Ξ ++ Ξ“)) β†’
         ren (ρ₄ >> ρ₂) ([ (ren (pack (injectΛ‘ Ξ”)) ∘ (lookup (base vl^Tm)))
                         , (ren (freshΚ³ vl^Var Ξ)  ∘ (lookup ρ₁))
                         ] (split Ξ k))
         ≑ [ lookup ρ₅ , lookup ρ₃ ]β€² (split Ξ k)
   aux ρ^R vs^R k with split Ξ k
   ... | inj₁ kΛ‘ =
     begin
       ren (ρ₄ >> ρ₂) (ren (pack (injectΛ‘ Ξ”)) (lookup (base vl^Tm) kΛ‘))
            β‰‘βŸ¨ Fus.fus RenΒ² (pack^R (injectΛ‘->> ρ₄ ρ₂)) (lookup (base vl^Tm) kΛ‘) ⟩
       ren ρ₄ (lookup (base vl^Tm) kΛ‘)
            β‰‘βŸ¨ cong (ren ρ₄) (lookup-base^Tm kΛ‘) ⟩
       ren ρ₄ (`var kΛ‘)
            β‰‘βŸ¨ lookup^R vs^R kΛ‘ ⟩
       lookup ρ₅ kΛ‘
     ∎
   ... | injβ‚‚ kΚ³ =
     begin
       ren (ρ₄ >> ρ₂) (ren (freshΚ³ vl^Var Ξ) (lookup ρ₁ kΚ³))
            β‰‘βŸ¨ Fus.fus RenΒ² (pack^R (freshΚ³->> Ξ ρ₄ ρ₂)) (lookup ρ₁ kΚ³) ⟩
       ren ρ₂ (lookup ρ₁ kΚ³)
            β‰‘βŸ¨ lookup^R ρ^R kΚ³ ⟩
       lookup ρ₃ kΚ³
     ∎

 Fus.var^R   SubRen = Ξ» ρ^R v β†’ lookup^R ρ^R v
 Fus.alg^R   SubRen {ρ₁ = ρ₁} {ρ₂} {ρ₃} b ρ^R = Ξ» zipped β†’ cong `con $
   let v₁ = fmap d (Sem.body Substitution ρ₁) b
       v₃ = fmap d (Sem.body Substitution ρ₃) b in
   begin
     fmap d (reify vl^Var) (fmap d (Sem.body Renaming ρ₂) (fmap d (reify vl^Tm) v₁))
         β‰‘βŸ¨ cong (fmap d (reify vl^Var)) (fmapΒ² d (reify vl^Tm) (Sem.body Renaming ρ₂) v₁) ⟩
     fmap d (reify vl^Var) (fmap d (Ξ» Ξ¦ i β†’ (Sem.body Renaming ρ₂ Ξ¦ i) ∘ (reify vl^Tm Ξ¦ i)) v₁)
         β‰‘βŸ¨ zip^reify VarTm^R (reify^R VarTm^R Eq^R vl^VarTm) d zipped ⟩
      fmap d (reify vl^Tm) v₃
   ∎

 subren :  {Ξ“ Ξ” Θ : List I} {i : I} β†’ βˆ€ t (ρ₁ : (Ξ“ ─Env) (Tm d ∞) Ξ”) (ρ₂ : Thinning Ξ” Θ) β†’
           ren ρ₂ {i = i} (sub ρ₁ t) ≑ sub (ren ρ₂ <$> ρ₁) t
 subren t ρ₁ ρ₂ = Fus.fus SubRen (pack^R (Ξ» k β†’ refl)) t


 SubΒ² : Fus (Ξ» ρ₁ ρ₂ β†’ βˆ€[ Eq^R ] (sub ρ₂ <$> ρ₁)) Eq^R Eq^R d Substitution Substitution Substitution
 Fus.quote₁ SubΒ² = Ξ» _ t β†’ t
 Fus.vl^π“₯₁ SubΒ² = vl^Tm
 Fus.th^R SubΒ² {ρ₁ = ρ₁} {ρ₂} {ρ₃} = Ξ» Οƒ ρ^R β†’ pack^R $ Ξ» k β†’
   begin
     sub (ren Οƒ <$> ρ₂) (lookup ρ₁ k) β‰‘βŸ¨ sym $ subren (lookup ρ₁ k) ρ₂ Οƒ ⟩
     ren Οƒ (sub ρ₂ (lookup ρ₁ k))     β‰‘βŸ¨ cong (ren Οƒ) (lookup^R ρ^R k)   ⟩
     ren Οƒ (lookup ρ₃ k)
   ∎
 Fus.>>^R SubΒ² {Ξ“} {Ξ”} {Θ} {Ξ} {ρ₁} {ρ₂} {ρ₃} {ρ₄} {ρ₅} = Ξ» ρ^R vs^R β†’ pack^R (aux ρ^R vs^R) where

   aux : βˆ€[ Eq^R ] (sub ρ₂ <$> ρ₁) ρ₃ β†’ βˆ€[ Eq^R ] ρ₄ ρ₅ β†’ {i : I} (k : Var i (Ξ ++ Ξ“)) β†’
         sub (ρ₄ >> ρ₂) ([ lookup (freshΛ‘ vl^Tm Ξ”) , ren (freshΚ³ vl^Var Ξ) ∘ lookup ρ₁ ]β€² (split Ξ k))
         ≑ [ lookup ρ₅ , lookup ρ₃ ]β€² (split Ξ k)
   aux ρ^R vs^R k with split Ξ k
   ... | inj₁ kΛ‘ =
     begin
       sub (ρ₄ >> ρ₂) (ren (pack (injectΛ‘ Ξ”)) (lookup (base vl^Tm) kΛ‘))
            β‰‘βŸ¨ Fus.fus RenSub (pack^R (injectΛ‘->> ρ₄ ρ₂)) (lookup (base vl^Tm) kΛ‘) ⟩
       sub ρ₄ (lookup (base vl^Tm) kΛ‘)
            β‰‘βŸ¨ cong (sub ρ₄) (lookup-base^Tm kΛ‘) ⟩
       sub ρ₄ (`var kΛ‘)
            β‰‘βŸ¨ lookup^R vs^R kΛ‘ ⟩
       lookup ρ₅ kΛ‘
     ∎
   ... | injβ‚‚ kΚ³ =
     begin
       sub (ρ₄ >> ρ₂) (ren (freshΚ³ vl^Var Ξ) (lookup ρ₁ kΚ³))
            β‰‘βŸ¨ Fus.fus RenSub (pack^R (freshΚ³->> Ξ ρ₄ ρ₂)) (lookup ρ₁ kΚ³) ⟩
       sub ρ₂ (lookup ρ₁ kΚ³)
            β‰‘βŸ¨ lookup^R ρ^R kΚ³ ⟩
       lookup ρ₃ kΚ³
     ∎
 Fus.var^R SubΒ² = Ξ» ρ^R v β†’ lookup^R ρ^R v
 Fus.alg^R SubΒ² {ρ₁ = ρ₁} {ρ₂} {ρ₃} b ρ^R = Ξ» zipped β†’ cong `con $
   let v₁ = fmap d (Sem.body Substitution ρ₁) b
       v₃ = fmap d (Sem.body Substitution ρ₃) b in
   begin
     fmap d (reify vl^Tm) (fmap d (Sem.body Substitution ρ₂) (fmap d (reify vl^Tm) v₁))
         β‰‘βŸ¨ cong (fmap d (reify vl^Tm)) (fmapΒ² d (reify vl^Tm) (Sem.body Substitution ρ₂) v₁) ⟩
     fmap d (reify vl^Tm) (fmap d (Ξ» Ξ¦ i β†’ (Sem.body Substitution ρ₂ Ξ¦ i) ∘ (reify vl^Tm Ξ¦ i)) v₁)
         β‰‘βŸ¨ zip^reify Eq^R (reify^R Eq^R Eq^R (vl^Refl vl^Tm)) d zipped ⟩
      fmap d (reify vl^Tm) v₃
   ∎

 subΒ² :  {Ξ“ Ξ” Θ : List I} {i : I} β†’ βˆ€ t (ρ₁ : (Ξ“ ─Env) (Tm d ∞) Ξ”) (ρ₂ : (Ξ” ─Env) (Tm d ∞) Θ) β†’
         sub ρ₂ {i = i} (sub ρ₁ t) ≑ sub (sub ρ₂ <$> ρ₁) t
 subΒ² t ρ₁ ρ₂ = Fus.fus SubΒ² (pack^R (Ξ» k β†’ refl)) t



-- Corollary

 renΞ² : βˆ€ {Ξ“ Ξ” i j} (b : Tm d ∞ j (i ∷ Ξ“)) (u : Tm d ∞ i Ξ“) (ρ : Thinning Ξ“ Ξ”) β†’
        ren ρ (b [ u /0]) ≑ ren (lift vl^Var (i ∷ []) ρ) b [ ren ρ u /0]
 renβ {i = i} b u ρ = begin
     ren ρ (b [ u /0])         β‰‘βŸ¨ subren b (u /0]) ρ ⟩
     sub (ren ρ <$> (u /0])) b β‰‘βŸ¨ sym (Fus.fus RenSub eq^R b) ⟩
     ren ρ′ b [ ren ρ u /0]    ∎ where

     ρ′ = lift vl^Var (i ∷ []) ρ

     eq^R : βˆ€[ Eq^R ] (select ρ′ (ren ρ u /0])) (ren ρ <$> (u /0]))
     lookup^R eq^R z     = refl
     lookup^R eq^R (s k) = begin
       lookup (base vl^Tm) (lookup (base vl^Var) (lookup ρ k)) β‰‘βŸ¨ lookup-base^Tm _ ⟩
       `var (lookup (base vl^Var) (lookup ρ k))                β‰‘βŸ¨ cong `var (lookup-base^Var _) ⟩
       `var (lookup ρ k)                                       β‰‘βŸ¨ sym (cong (ren ρ) (lookup-base^Tm k)) ⟩
       ren ρ (lookup (base vl^Tm) k)                           ∎

 subΞ² : βˆ€ {Ξ“ Ξ” i j} (b : Tm d ∞ j (i ∷ Ξ“)) (u : Tm d ∞ i Ξ“) (ρ : (Ξ“ ─Env) (Tm d ∞) Ξ”) β†’
        sub ρ (b [ u /0]) ≑ sub (lift vl^Tm (i ∷ []) ρ) b [ sub ρ u /0]
 subβ {i = i} b u ρ = begin
   sub ρ (b [ u /0])                  β‰‘βŸ¨ subΒ² b (u /0]) ρ ⟩
   sub (sub ρ <$> (base vl^Tm βˆ™ u)) b β‰‘βŸ¨ sym (Fus.fus SubΒ² eq^Rβ€² b) ⟩
   sub ρ′ b [ sub ρ u /0]             ∎ where

   ρ′ = lift vl^Tm (i ∷ []) ρ
   Οƒ  = freshΚ³ vl^Var (i ∷ [])

   eq^R : βˆ€[ Eq^R ] (select Οƒ (sub ρ u /0])) (base vl^Tm)
   lookup^R eq^R z     = refl
   lookup^R eq^R (s k) = cong (ren extend ∘ lookup (base vl^Tm)) (lookup-base^Var k)

   eq^Rβ€² : βˆ€[ Eq^R ] (sub (sub ρ u /0]) <$> ρ′) (sub ρ <$> (base vl^Tm βˆ™ u))
   lookup^R eq^Rβ€² z     = refl
   lookup^R eq^Rβ€² (s k) = begin
     sub (sub ρ u /0]) (ren Οƒ (lookup ρ k))  β‰‘βŸ¨ Fus.fus RenSub eq^R (lookup ρ k) ⟩
     sub (base vl^Tm) (lookup ρ k)           β‰‘βŸ¨ sub-id (lookup ρ k) ⟩
     lookup ρ k                              β‰‘βŸ¨ cong (sub ρ) (sym $ lookup-base^Tm k) ⟩
     sub ρ (lookup (base vl^Tm) k) ∎