open import Data.List using (List)

open import CBPV.Structure
open import CBPV.Type

module CBPV.Frex.Comp
  {A : RawAlgebra} (Aᴹ : IsModel A)
  (Θ : List ValType) (Ψ : List CompType) (T : CompType)
  where

open import Function.Base using (_∘_; _$_)
open import Function.Nary.NonDependent using (congₙ)
open import Relation.Binary.PropositionalEquality.Core

open ≡-Reasoning

open import CBPV.Context
open import CBPV.Family

private
  variable
    Γ Δ Π : Context
    x y : Name
    A′ A′′ : ValType
    B : CompType

  module A where
    open RawAlgebra A public
    open IsModel Aᴹ public

  ⟦T⟧ : ValType
  ⟦T⟧ = U (Θ ⟶⋆ Ψ ⟶′⋆ T)

  𝔐 : Context
  𝔐 = [< 𝔪 :- ⟦T⟧ ]

-- Cast and Expand substitutions

cast : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ → Γ ~[ A.Val ]↝ Δ ++ 𝔐
cast σ = σ ⨾ λ ◌ → ◌

expand : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ → Γ :< (𝔪 :- ⟦T⟧) ~[ A.Val ]↝ Δ :< (𝔪 :- ⟦T⟧)
expand σ = cast σ :< 𝔪 ↦ A.var (%% 𝔪)

cast-comm :
  (σ : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ) (f : ∀ {A} → δᵛ 𝔐 A.Val A Δ → δᵛ 𝔐 A.Val A Π) →
  cast σ ⨾ f ≡ cast (σ ⨾ f)
cast-comm σ f = begin
  cast σ ⨾ f   ≡⟨ ⨾-assoc σ (λ ◌ → ◌) f ⟩
  σ ⨾ f        ≡˘⟨ ⨾-assoc σ f (λ ◌ → ◌) ⟩
  cast (σ ⨾ f) ∎

lookup-cast : (σ : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ) (i : VarPos x A′ Γ) → lookup (cast σ) i ≡ lookup σ i
lookup-cast σ i = lookup-⨾ σ (λ ◌ → ◌) i

＠-cast : (σ : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ) (i : Var A′ Γ) → cast σ ＠ i ≡ σ ＠ i
＠-cast σ i = ＠-⨾ σ (λ ◌ → ◌) i

expand-wkn : expand (id {Γ = Γ} ⨾ (A.var ∘ ThereVar)) ≡ (id ⨾ A.var)
expand-wkn = cong (_:< 𝔪 ↦ A.var (%% 𝔪)) $ begin
  cast (id ⨾ (A.var ∘ ThereVar)) ≡⟨ ⨾-assoc id (A.var ∘ ThereVar) (λ ◌ → ◌) ⟩
  id ⨾ (A.var ∘ ThereVar)        ≡˘⟨ ⨾-assoc {W = Var} id ThereVar A.var ⟩
  id ⨾ ThereVar ⨾ A.var          ≡⟨ cong (_⨾ A.var) (tabulate-⨾ (λ ◌ → ◌) ThereVar) ⟩
  tabulate ThereVar ⨾ A.var      ∎

-- Monoid Structure

open RawMonoid

frexMonoid : RawMonoid
frexMonoid .Val = δᵛ 𝔐 A.Val
frexMonoid .Comp = δᶜ 𝔐 A.Comp
frexMonoid .var i = A.var (ThereVar i)
frexMonoid .subᵛ v σ = A.subᵛ v (expand σ)
frexMonoid .subᶜ c σ = A.subᶜ c (expand σ)

open IsMonoid

frexIsMonoid : IsMonoid frexMonoid
frexIsMonoid .subᵛ-var i σ = begin
  A.subᵛ (A.var $ ThereVar i) (expand σ) ≡⟨ A.subᵛ-var (ThereVar i) (expand σ) ⟩
  expand σ ＠ ThereVar i                 ≡⟨⟩
  cast σ ＠ i                            ≡⟨ ＠-cast σ i ⟩
  σ ＠ i                                 ∎
frexIsMonoid .renᵛ-id v = begin
  A.subᵛ v (expand (id ⨾ λ ◌ → A.var $ ThereVar ◌)) ≡⟨ cong (A.subᵛ v) expand-wkn ⟩
  A.renᵛ v id                                       ≡⟨ A.renᵛ-id v ⟩
  v                                                 ∎
frexIsMonoid .subᵛ-assoc v σ ς =
  begin
    A.subᵛ (A.subᵛ v (expand σ)) (expand ς)
  ≡⟨ A.subᵛ-assoc v (expand σ) (expand ς) ⟩
    A.subᵛ v (expand σ ⨾ λ ◌ → A.subᵛ ◌ (expand ς))
  ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → A.subᵛ v (◌ᵃ :< 𝔪 ↦ ◌ᵇ))
       (cast-comm σ (λ ◌ → A.subᵛ ◌ (expand ς)))
       (A.subᵛ-var (%% 𝔪) (expand ς)) ⟩
    A.subᵛ v (expand (σ ⨾ λ ◌ → A.subᵛ ◌ (expand ς)))
  ∎
frexIsMonoid .renᶜ-id c = begin
  A.subᶜ c (expand (id ⨾ λ ◌ → A.var $ ThereVar ◌)) ≡⟨ cong (A.subᶜ c) expand-wkn ⟩
  A.renᶜ c id                                       ≡⟨ A.renᶜ-id c ⟩
  c                                                 ∎
frexIsMonoid .subᶜ-assoc c σ ς =
  begin
    A.subᶜ (A.subᶜ c (expand σ)) (expand ς)
  ≡⟨ A.subᶜ-assoc c (expand σ) (expand ς) ⟩
    A.subᶜ c ((cast σ ⨾ λ ◌ → A.subᵛ ◌ (expand ς)) :< 𝔪 ↦ A.subᵛ (A.var $ %% 𝔪) (expand ς))
  ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → A.subᶜ c (◌ᵃ :< 𝔪 ↦ ◌ᵇ))
       (cast-comm σ (λ ◌ → A.subᵛ ◌ (expand ς)))
       (A.subᵛ-var (%% 𝔪) (expand ς)) ⟩
    A.subᶜ c (expand (σ ⨾ λ ◌ → A.subᵛ ◌ (expand ς)))
  ∎

open RawAlgebra
  renaming
    ( have_be_ to [_]have_be_
    ; drop_then_ to [_]drop_then_
    ; ⟨_,_⟩ to [_]⟨_,_⟩
    ; split_then_ to [_]split_then_
    ; case_of_or_ to [_]case_of_or_
    ; bind_to_ to [_]bind_to_
    ; ⟪_,_⟫ to [_]⟪_,_⟫
    ; push_then_ to [_]push_then_
    )

frexAlgebra : RawAlgebra
frexAlgebra .monoid = frexMonoid
[ frexAlgebra ]have v be c = A.have v be A.renᶜ c (pull [< _ :- _ ] 𝔐)
frexAlgebra .thunk c = A.thunk c
frexAlgebra .force v = A.force v
frexAlgebra .point = A.point
[ frexAlgebra ]drop v then c = A.drop v then c
[ frexAlgebra ]⟨ v , w ⟩ = A.⟨ v , w ⟩
[ frexAlgebra ]split v then c = A.split v then A.renᶜ c (pull [< _ :- _ , _ :- _ ] 𝔐)
frexAlgebra .inl v = A.inl v
frexAlgebra .inr v = A.inr v
[ frexAlgebra ]case v of c or d =
  A.case v
  of A.renᶜ c (pull [< _ :- _ ] 𝔐)
  or A.renᶜ d (pull [< _ :- _ ] 𝔐)
frexAlgebra .ret v = A.ret v
[ frexAlgebra ]bind c to d = A.bind c to A.renᶜ d (pull [< _ :- _ ] 𝔐)
[ frexAlgebra ]⟪ c , d ⟫ = A.⟪ c , d ⟫
frexAlgebra .fst c = A.fst c
frexAlgebra .snd c = A.snd c
frexAlgebra .pop c = A.pop (A.renᶜ c (pull [< _ :- _ ] 𝔐))
[ frexAlgebra ]push v then c = A.push v then c

private module X = RawAlgebra frexAlgebra

open IsAlgebra

lemma₀ : (v : X.Val A′ Γ) (ρ : Γ ↝ Δ) → X.renᵛ v ρ ≡ A.renᵛ v (ρ ⨾ ThereVar :< 𝔪 ↦ %% 𝔪)
lemma₀ {A′ = A′} v ρ = begin
  X.renᵛ v ρ                                                   ≡⟨⟩
  X.subᵛ v (ρ ⨾ X.var)                                         ≡⟨⟩
  A.subᵛ v (expand (ρ ⨾ X.var))                                ≡⟨⟩
  A.subᵛ v (cast (ρ ⨾ X.var) :< 𝔪 ↦ A.var (%% 𝔪))              ≡⟨⟩
  A.subᵛ v (cast (ρ ⨾ (A.var ∘ ThereVar)) :< 𝔪 ↦ A.var (%% 𝔪)) ≡⟨ cong (λ ◌ → A.subᵛ v (◌ :< 𝔪 ↦ A.var (toVar Here))) (⨾-assoc ρ (A.var ∘ ThereVar) (λ ◌ → ◌)) ⟩
  A.subᵛ v (ρ ⨾ (A.var ∘ ThereVar) :< 𝔪 ↦ A.var (%% 𝔪))        ≡˘⟨ cong (λ ◌ → A.subᵛ v (◌ :< 𝔪 ↦ A.var (toVar Here))) (⨾-assoc ρ ThereVar A.var) ⟩
  A.subᵛ v (ρ ⨾ ThereVar ⨾ A.var :< 𝔪 ↦ A.var (%% 𝔪))          ≡⟨⟩
  A.subᵛ v ((ρ ⨾ ThereVar :< 𝔪 ↦ %% 𝔪) ⨾ A.var)                ≡⟨⟩
  A.renᵛ v (ρ ⨾ ThereVar {y = 𝔪} :< 𝔪 ↦ %% 𝔪)                  ∎

lemma₁ :
  (c : δᶜ [< x :- A′ ] X.Comp B Γ) (σ : Γ ~[ X.Val ]↝ Δ) →
  A.subᶜ (A.renᶜ c (pull [< x :- A′ ] 𝔐)) (A.lift [< x :- A′ ] (expand σ)) ≡
  A.renᶜ (X.subᶜ c (X.lift [< x :- A′ ] σ)) (pull [< x :- A′ ] 𝔐)
lemma₁ {x = x} c σ =
  begin
    A.subᶜ (A.renᶜ c (pull [< x :- _ ] 𝔐)) (A.lift [< x :- _ ] (expand σ))
  ≡⟨ A.subᶜ-renᶜ c (pull [< x :- _ ] 𝔐) (A.lift [< x :- _ ] (expand σ)) ⟩
    A.subᶜ c (pull [< x :- _ ] 𝔐 ⨾ (A.lift [< x :- _ ] (expand σ) ＠_))
  ≡⟨ congₙ 3 (λ ◌ᵃ ◌ᵇ ◌ᶜ → A.subᶜ c (◌ᵃ :< x ↦ ◌ᵇ :< 𝔪 ↦ ◌ᶜ))
       (begin
          weakl 𝔐 ⨾ (weakl [< x :- _ ] ＠_) ⨾ (A.lift [< x :- _ ] (expand σ) ＠_)
        ≡⟨ cong (_⨾ (A.lift [< x :- _ ] (expand σ) ＠_)) (⨾-cong (weakl 𝔐) (＠-tabulate Var ThereVar)) ⟩
          weakl 𝔐 ⨾ ThereVar ⨾ (A.lift [< x :- _ ] (expand σ) ＠_)
        ≡⟨ ⨾-assoc (weakl 𝔐) ThereVar (A.lift [< x :- _ ] (expand σ) ＠_) ⟩
          weakl 𝔐 ⨾ (λ ◌ → A.lift [< x :- _ ] (expand σ) ＠ ThereVar ◌)
        ≡⟨ ⨾-cong (weakl 𝔐) (＠-⨾ (expand σ) (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))) ⟩
          weakl 𝔐 ⨾ (λ ◌ → A.renᵛ (expand σ ＠ ◌) (weakl [< x :- _ ]))
        ≡˘⟨ ⨾-assoc (weakl 𝔐) (expand σ ＠_) (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ])) ⟩
          ([ A.Val ] (weakl 𝔐 ⨾ (expand σ ＠_)) ⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ])))
        ≡⟨ cong (_⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))) (tabulate-⨾ (weaklF 𝔐) (expand σ ＠_)) ⟩
          tabulate (cast σ ＠_) ⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))
        ≡⟨ cong (_⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))) (tabulate-＠ (cast σ)) ⟩
          cast σ ⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))
        ≡⟨ ⨾-assoc σ (λ ◌ → ◌) (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ])) ⟩
          σ ⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))
        ≡⟨ ⨾-cong σ (λ v → cong (λ ◌ → A.renᵛ v (◌ :< 𝔪 ↦ %% 𝔪)) $
             begin
               tabulate (ThereVar ∘ ThereVar)                              ≡˘⟨ tabulate-cong Var (λ i → pull-left [< x :- _ ] 𝔐 (i .pos)) ⟩
               (tabulate ((pull [< x :- _ ] 𝔐 ＠_) ∘ ThereVar ∘ ThereVar)) ≡˘⟨ tabulate-⨾ {V = Var} ThereVar ((pull [< x :- _ ] 𝔐 ＠_) ∘ ThereVar) ⟩
               (tabulate ThereVar ⨾ ((pull [< x :- _ ] 𝔐 ＠_) ∘ ThereVar)) ≡˘⟨ ⨾-assoc (tabulate ThereVar) ThereVar (pull [< x :- _ ] 𝔐 ＠_) ⟩
               (tabulate ThereVar ⨾ ThereVar ⨾ (pull [< x :- _ ] 𝔐 ＠_))   ∎) ⟩
          σ ⨾ (λ ◌ → A.renᵛ ◌ ((weakl [< x :- _ ] ⨾ ThereVar :< 𝔪 ↦ %% 𝔪) ⨾ (pull [< x :- _ ] 𝔐 ＠_)))
        ≡˘⟨ ⨾-cong σ (λ v → A.renᵛ-assoc v (weakl [< x :- _ ] ⨾ ThereVar :< 𝔪 ↦ %% 𝔪) (pull [< x :- _ ] 𝔐)) ⟩
          σ ⨾ (λ ◌ → A.renᵛ (A.renᵛ ◌ (weakl [< x :- _ ] ⨾ ThereVar :< 𝔪 ↦ %% 𝔪)) (pull [< x :- _ ] 𝔐))
        ≡˘⟨ ⨾-cong σ (λ v → cong (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐)) (lemma₀ v (weakl [< x :- _ ]))) ⟩
          σ ⨾ (λ ◌ → A.renᵛ (X.renᵛ ◌ (weakl [< x :- _ ])) (pull [< x :- _ ] 𝔐))
        ≡˘⟨ ⨾-assoc σ (λ ◌ → X.renᵛ ◌ (weakl [< x :- _ ])) (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐)) ⟩
          σ ⨾ (λ ◌ → X.renᵛ ◌ (weakl [< x :- _ ])) ⨾ (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐))
        ≡˘⟨ ⨾-assoc (σ ⨾ (λ ◌ → X.renᵛ ◌ (weakl [< x :- _ ]))) (λ ◌ → ◌) (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐)) ⟩
          σ ⨾ (λ ◌ → X.renᵛ ◌ (weakl [< x :- _ ])) ⨾ (λ ◌ → ◌) ⨾ (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐))
        ∎)
       (begin
         A.var (%% x)                                 ≡˘⟨ A.renᵛ-var (%% x) (pull [< x :- _ ] 𝔐) ⟩
         A.renᵛ (A.var (%% x)) (pull [< x :- _ ] 𝔐) ∎)
       {!!} ⟩
    A.subᶜ c (expand (X.lift [< x :- _ ] σ) ⨾ λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐))
  ≡˘⟨ A.subᶜ-assoc c (expand $ X.lift [< x :- _ ] σ) (pull [< x :- _ ] 𝔐 ⨾ A.var) ⟩
    A.renᶜ (A.subᶜ c (expand $ X.lift [< x :- _ ] σ)) (pull [< x :- _ ] 𝔐)
  ≡⟨⟩
    A.renᶜ (X.subᶜ c (X.lift [< x :- _ ] σ)) (pull [< x :- _ ] 𝔐)
  ∎
-- lemma₁ {x = x} {A′} c σ =
--   begin
--     A.subᶜ (A.subᶜ c (pull [< x :- _ ] 𝔐 ⨾ A.var)) (A.lift [< x :- _ ] (expand σ))
--   ≡⟨ A.subᶜ-assoc c (pull [< x :- _ ] 𝔐 ⨾ A.var) (A.lift [< x :- _ ] (expand σ)) ⟩
--     A.subᶜ c (pull [< x :- _ ] 𝔐 ⨾ A.var ⨾ λ ◌ → A.subᵛ ◌ (A.lift [< x :- _ ] (expand σ)))
--   ≡⟨ cong (A.subᶜ c) (subst-ext _ _ (λ i → helper (i .pos))) ⟩
--     A.subᶜ c (expand (X.lift [< x :- _ ] σ) ⨾ λ ◌ → A.subᵛ ◌ (pull [< x :- _ ] 𝔐 ⨾ A.var))
--   ≡˘⟨ A.subᶜ-assoc c (expand (X.lift [< x :- _ ] σ)) (pull [< x :- _ ] 𝔐 ⨾ A.var) ⟩
--     A.subᶜ (X.subᶜ c (X.lift [< x :- _ ] σ)) (pull [< x :- _ ] 𝔐 ⨾ A.var)
--   ∎
--   where
--   helper :
--     (i : VarPos y A′′ _) →
--       lookup
--         (pull [< x :- A′ ] 𝔐 ⨾ A.var ⨾ λ ◌ → A.subᵛ ◌ (A.lift [< x :- A′ ] (expand σ)))
--         i
--     ≡
--       lookup {V = A.Val}
--         (expand (X.lift [< x :- A′ ] σ) ⨾ λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var))
--         i
--   helper Here = begin
--     A.subᵛ (A.var $ toVar $ There Here) (A.lift [< x :- _ ] (expand σ)) ≡⟨ A.subᵛ-var _ _ ⟩
--     A.subᵛ (A.var $ %% 𝔪) (weakl [< x :- A′ ] ⨾ A.var)                  ≡⟨ A.subᵛ-var _ _ ⟩
--     A.var (%% 𝔪)                                                        ≡˘⟨ A.subᵛ-var _ _ ⟩
--     A.subᵛ (A.var $ %% 𝔪) (pull [< x :- _ ] 𝔐 ⨾ A.var)                  ∎
--   helper (There Here) = begin
--     A.subᵛ (A.var $ %% x) (A.lift [< x :- _ ] (expand σ)) ≡⟨ A.subᵛ-var _ _ ⟩
--     A.var (%% x)                                          ≡˘⟨ A.subᵛ-var _ _ ⟩
--     A.subᵛ (A.var $ %% x) (pull [< x :- _ ] 𝔐 ⨾ A.var)   ∎
--   helper (There (There i)) =
--     begin
--       lookup
--         (pull [< x :- _ ] 𝔐 ⨾ A.var ⨾ λ ◌ → A.subᵛ ◌ (A.lift [< x :- A′ ] (expand σ)))
--         (There $ There i)
--     ≡⟨ lookup-⨾ (pull [< x :- _ ] 𝔐 ⨾ A.var) (λ ◌ → A.subᵛ ◌ (A.lift [< x :- A′ ] (expand σ))) (There $ There i) ⟩
--       A.subᵛ
--         (lookup {V = A.Val}
--           (pull [< x :- _ ] 𝔐 ⨾ A.var)
--           (There $ There i))
--         (A.lift [< x :- A′ ] (expand σ))
--     ≡⟨ cong (λ ◌ → A.subᵛ ◌ (A.lift [< x :- A′ ] (expand σ))) (lookup-⨾ (pull [< x :- _ ] 𝔐) A.var (There $ There i)) ⟩
--       A.subᵛ
--         (A.var $ lookup (pull [< x :- _ ] 𝔐) (There $ There i))
--         (A.lift [< x :- A′ ] (expand σ))
--     ≡⟨ A.subᵛ-var (lookup (pull [< x :- _ ] 𝔐) (There $ There i)) (A.lift [< x :- A′ ] (expand σ)) ⟩
--       A.lift [< x :- A′ ] (expand σ) ＠
--        lookup (pull [< x :- _ ] 𝔐) (There $ There i)
--     ≡⟨ cong (A.lift [< x :- _ ] (expand σ) ＠_) (pull-left [< x :- _ ] 𝔐 i) ⟩
--       lookup (A.lift [< x :- A′ ] (expand σ)) (There $ There i)
--     ≡⟨ A.lift-left [< x :- A′ ] (expand σ) (There i) ⟩
--       A.subᵛ (lookup (cast σ) i) (weakl [< x :- A′ ] ⨾ A.var)
--     ≡⟨ cong (λ ◌ → A.subᵛ ◌ (weakl [< x :- A′ ] ⨾ A.var)) (lookup-cast σ i) ⟩
--       A.subᵛ (lookup σ i) (weakl [< x :- A′ ] ⨾ A.var)
--     ≡⟨ {!!} ⟩
--       A.subᵛ (lookup σ i)
--         (expand (weakl [< x :- A′ ] ⨾ X.var) ⨾ λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var))
--     ≡˘⟨ A.subᵛ-assoc (lookup σ i) (expand (weakl [< x :- A′ ] ⨾ X.var)) (pull [< x :- A′ ] 𝔐 ⨾ A.var) ⟩
--       A.subᵛ
--         (A.subᵛ (lookup σ i) (expand (weakl [< x :- A′ ] ⨾ X.var)))
--         (pull [< x :- A′ ] 𝔐 ⨾ A.var)
--     ≡⟨⟩
--       A.subᵛ
--         (X.subᵛ (lookup σ i) (weakl [< x :- A′ ] ⨾ X.var))
--         (pull [< x :- A′ ] 𝔐 ⨾ A.var)
--     ≡˘⟨ cong (λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var)) (X.lift-left [< x :- A′ ] σ i) ⟩
--       A.subᵛ
--         (lookup (X.lift [< x :- A′ ] σ) (There i))
--         (pull [< x :- A′ ] 𝔐 ⨾ A.var)
--     ≡˘⟨ cong (λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var)) (lookup-cast (X.lift [< x :- A′ ] σ) (There i)) ⟩
--       A.subᵛ
--         (lookup (cast $ X.lift [< x :- A′ ] σ) (There i))
--         (pull [< x :- A′ ] 𝔐 ⨾ A.var)
--     ≡˘⟨ lookup-⨾ (expand (X.lift [< x :- A′ ] σ)) (λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var)) (There $ There i) ⟩
--       lookup {V = A.Val}
--         (expand (X.lift [< x :- A′ ] σ) ⨾ λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var))
--         (There $ There i)
--     ∎

-- frexIsAlgebra : IsAlgebra frexAlgebra
-- frexIsAlgebra .isMonoid = frexIsMonoid
-- frexIsAlgebra .sub-have v c σ =
--   begin
--     A.subᶜ
--       (A.have v be A.subᶜ c (pull [< _ :- _ ] 𝔐 ⨾ A.var))
--       (expand σ)
--   ≡⟨ A.sub-have v (A.subᶜ c (pull [< _ :- _ ] 𝔐 ⨾ A.var)) (expand σ) ⟩
--     (A.have A.subᵛ v (expand σ) be
--       A.subᶜ (A.subᶜ c (pull [< _ :- _ ] 𝔐 ⨾ A.var)) (A.lift [< _ :- _ ] (expand σ)))
--   ≡⟨ cong (λ ◌ → A.have A.subᵛ v (expand σ) be ◌) (lemma₁ c σ) ⟩
--     (A.have A.subᵛ v (expand σ) be
--       A.subᶜ (X.subᶜ c (X.lift [< _ :- _ ] σ)) (pull [< _ :- _ ] 𝔐 ⨾ A.var))
--   ∎
-- frexIsAlgebra .sub-thunk c σ = A.sub-thunk c (expand σ)
-- frexIsAlgebra .sub-force v σ = A.sub-force v (expand σ)
-- frexIsAlgebra .sub-point σ = A.sub-point (expand σ)
-- frexIsAlgebra .sub-drop v c σ = A.sub-drop v c (expand σ)
-- frexIsAlgebra .sub-pair v w σ = A.sub-pair v w (expand σ)
-- frexIsAlgebra .sub-split = {!!}
-- frexIsAlgebra .sub-inl v σ = A.sub-inl v (expand σ)
-- frexIsAlgebra .sub-inr v σ = A.sub-inr v (expand σ)
-- frexIsAlgebra .sub-case = {!!}
-- frexIsAlgebra .sub-ret v σ = A.sub-ret v (expand σ)
-- frexIsAlgebra .sub-bind = {!!}
-- frexIsAlgebra .sub-bundle c d σ = A.sub-bundle c d (expand σ)
-- frexIsAlgebra .sub-fst c σ = A.sub-fst c (expand σ)
-- frexIsAlgebra .sub-snd c σ = A.sub-snd c (expand σ)
-- frexIsAlgebra .sub-pop = {!!}
-- frexIsAlgebra .sub-push v c σ = A.sub-push v c (expand σ)