module CBPV.Structure where

open import CBPV.Context hiding (map)
open import CBPV.Family
open import CBPV.Type

open import Data.List using (List)
open import Data.List.Relation.Unary.All using (All; map)

open import Function.Base using (_∘_; _$_)

open import Relation.Binary.PropositionalEquality.Core
open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning)

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

-- Raw Bundles ----------------------------------------------------------------

record RawMonoid : Set₁ where
  field
    Val  : ValFamily
    Comp : CompFamily
    var  : Var ⇾ᵗ Val
    subᵛ : Val ⇾ᵗ Val ^ᵗ Val
    subᶜ : Comp ⇾ᵗ Comp ^ᵗ Val

  renᵛ : Val ⇾ᵗ □ᵗ Val
  renᵛ v ρ = subᵛ v (ρ ⨾ var)

  renᶜ : Comp ⇾ᵗ □ᵗ Comp
  renᶜ c ρ = subᶜ c (ρ ⨾ var)

  lift : (Θ : Context) (σ : Γ ~[ Val ]↝ Δ) → Γ ++ Θ ~[ Val ]↝ Δ ++ Θ
  lift Θ σ = σ ⨾ (λ ◌ → renᵛ ◌ (weakl Θ)) ∥ weakr ⨾ var

  lift-weakl :
    (Θ : Context) (σ : Γ ~[ Val ]↝ Δ) →
    weakl Θ ⨾′ lift Θ σ ≈ σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ)
  lift-weakl Θ σ = copair-weakl {X = Val} {Δ = Θ} (σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ)) (weakr ⨾ var)

record RawAlgebra : Set₁ where
  infixr 1 have_be_ drop_then_ split_then_ bind_to_ push_then_
  infixr 1 have_be[_]_ split_then[_,_]_ bind_to[_]_
  infix 1 case_of_or_
  infix 1 case_of[_]_or[_]_
  field
    monoid : RawMonoid

  open RawMonoid monoid public

  field
    have_be_ : Val A ⇾ δᵗ [< x :- A ] Comp B ⇒ Comp B
    thunk : Comp B ⇾ Val (U B)
    force : Val (U B) ⇾ Comp B
    point : Val 𝟙 Γ
    drop_then_ : Val 𝟙 ⇾ Comp B ⇒ Comp B
    ⟨_,_⟩ : Val A ⇾ Val A′ ⇒ Val (A × A′)
    split_then_ : Val (A × A′) ⇾ δᵗ [< x :- A , y :- A′ ] Comp B ⇒ Comp B
    inl : Val A ⇾ Val (A + A′)
    inr : Val A′ ⇾ Val (A + A′)
    case_of_or_ : Val (A + A′) ⇾ δᵗ [< x :- A ] Comp B ⇒ δᵗ [< y :- A′ ] Comp B ⇒ Comp B
    ret : Val A ⇾ Comp (F A)
    bind_to_ : Comp (F A) ⇾ δᵗ [< x :- A ] Comp B ⇒ Comp B
    ⟪_,_⟫ : Comp B ⇾ Comp B′ ⇒ Comp (B × B′)
    fst : Comp (B × B′) ⇾ Comp B
    snd : Comp (B × B′) ⇾ Comp B′
    pop : δᵗ [< x :- A ] Comp B ⇾ Comp (A ⟶ B)
    push_then_ : Val A ⇾ Comp (A ⟶ B) ⇒ Comp B

  have_be[_]_ : Val A Γ → (x : Name) → δᵗ [< x :- A ] Comp B Γ → Comp B Γ
  have v be[ x ] c = have v be c

  split_then[_,_]_ : Val (A × A′) Γ → (x y : Name) → δᵗ [< x :- A , y :- A′ ] Comp B Γ → Comp B Γ
  split v then[ x , y ] c = split v then c

  case_of[_]_or[_]_ :
    Val (A + A′) Γ →
    (x : Name) → δᵗ [< x :- A ] Comp B Γ →
    (y : Name) → δᵗ [< y :- A′ ] Comp B Γ →
    Comp B Γ
  case v of[ x ] c or[ y ] d = case v of c or d

  bind_to[_]_ : Comp (F A) Γ → (x : Name) → δᵗ [< x :- A ] Comp B Γ → Comp B Γ
  bind c to[ x ] d = bind c to d

  pop[_] : (x : Name) → δᵗ [< x :- A ] Comp B ⇾ Comp (A ⟶ B)
  pop[ x ] c = pop c

open RawAlgebra

record RawCompExtension
  (A : RawAlgebra)
  (Θ : List ValType) (Ψ : List CompType) (T : CompType) : Set₁
  where
  field
    X : RawAlgebra
    staᵛ : A .Val ⇾ᵗ X .Val
    staᶜ : A .Comp ⇾ᵗ X .Comp
    dyn  : All (λ A → X .Val A Γ) Θ → All (λ B → X .Comp B Γ) Ψ → X .Comp T Γ

record RawValExtension
  (A : RawAlgebra)
  (Θ : List ValType) (Ψ : List CompType) (T : ValType) : Set₁
  where
  field
    X : RawAlgebra
    staᵛ : A .Val ⇾ᵗ X .Val
    staᶜ : A .Comp ⇾ᵗ X .Comp
    dyn  : All (λ A → X .Val A Γ) Θ → All (λ B → X .Comp B Γ) Ψ → X .Val T Γ

record RawFreeCompExtension
  (A : RawAlgebra)
  (Θ : List ValType) (Ψ : List CompType) (T : CompType) : Set₁
  where
  field
    extension : RawCompExtension A Θ Ψ T

  open RawCompExtension

  field
    evalᵛ : (ext : RawCompExtension A Θ Ψ T) → extension .X .Val ⇾ᵗ ext .X .Val
    evalᶜ : (ext : RawCompExtension A Θ Ψ T) → extension .X .Comp ⇾ᵗ ext .X .Comp

record RawFreeValExtension
  (A : RawAlgebra)
  (Θ : List ValType) (Ψ : List CompType) (T : ValType) : Set₁
  where
  field
    extension : RawValExtension A Θ Ψ T

  open RawValExtension

  field
    evalᵛ : (ext : RawValExtension A Θ Ψ T) → extension .X .Val ⇾ᵗ ext .X .Val
    evalᶜ : (ext : RawValExtension A Θ Ψ T) → extension .X .Comp ⇾ᵗ ext .X .Comp

-- Structures -----------------------------------------------------------------

record IsMonoid (M : RawMonoid) : Set where
  private module M = RawMonoid M
  field
    subᵛ-cong : (v : M.Val A Γ) → {σ ς : Γ ~[ M.Val ]↝ Δ} → σ ≈ ς → M.subᵛ v σ ≡ M.subᵛ v ς
    subᶜ-cong : (c : M.Comp B Γ) → {σ ς : Γ ~[ M.Val ]↝ Δ} → σ ≈ ς → M.subᶜ c σ ≡ M.subᶜ c ς
    subᵛ-var : (i : Var A Γ) (σ : Γ ~[ M.Val ]↝ Δ) → M.subᵛ (M.var i) σ ≡ σ ＠ i
    renᵛ-id : (v : M.Val A Γ) → M.renᵛ v id ≡ v
    subᵛ-assoc :
      (v : M.Val A Γ) (σ : Γ ~[ M.Val ]↝ Δ) (ς : Δ ~[ M.Val ]↝ Θ) →
      M.subᵛ (M.subᵛ v σ) ς ≡ M.subᵛ v (σ ⨾ λ ◌ → M.subᵛ ◌ ς)
    renᶜ-id : (c : M.Comp B Γ) → M.renᶜ c id ≡ c
    subᶜ-assoc :
      (c : M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) (ς : Δ ~[ M.Val ]↝ Θ) →
      M.subᶜ (M.subᶜ c σ) ς ≡ M.subᶜ c (σ ⨾ λ ◌ → M.subᵛ ◌ ς)

  open ≡-Reasoning

  renᵛ-cong : (v : M.Val A Γ) → {ρ ϱ : Γ ↝ Δ} → ρ ≈ ϱ → M.renᵛ v ρ ≡ M.renᵛ v ϱ
  renᵛ-cong v ρ≈ϱ = subᵛ-cong v (tabulate≈ $ cong M.var ∘ (ρ≈ϱ ＠_))

  renᶜ-cong : (c : M.Comp B Γ) → {ρ ϱ : Γ ↝ Δ} → ρ ≈ ϱ → M.renᶜ c ρ ≡ M.renᶜ c ϱ
  renᶜ-cong c ρ≈ϱ = subᶜ-cong c (tabulate≈ $ cong M.var ∘ (ρ≈ϱ ＠_))

  renᵛ-var : (i : Var A Γ) (ρ : Γ ↝ Δ) → M.renᵛ (M.var i) ρ ≡ M.var (ρ ＠ i)
  renᵛ-var i ρ = begin
    M.renᵛ (M.var i) ρ ≡⟨ subᵛ-var i (ρ ⨾ M.var) ⟩
    M.var (ρ ＠ i)     ∎

  subᵛ-renᵛ :
    (v : M.Val A Γ) (ρ : Γ ↝ Δ) (σ : Δ ~[ M.Val ]↝ Θ) →
    M.subᵛ (M.renᵛ v ρ) σ ≡ M.subᵛ v (ρ ⨾′ σ)
  subᵛ-renᵛ v ρ σ = begin
    M.subᵛ (M.renᵛ v ρ) σ                   ≡⟨ subᵛ-assoc v (ρ ⨾ M.var) σ ⟩
    M.subᵛ v (ρ ⨾ λ ◌ → M.subᵛ (M.var ◌) σ) ≡⟨ subᵛ-cong v (tabulate≈ $ λ i → subᵛ-var (ρ ＠ i) σ) ⟩
    M.subᵛ v (ρ ⨾′ σ)                       ∎

  subᶜ-renᶜ :
    (c : M.Comp B Γ) (ρ : Γ ↝ Δ) (σ : Δ ~[ M.Val ]↝ Θ) →
    M.subᶜ (M.renᶜ c ρ) σ ≡ M.subᶜ c (ρ ⨾′ σ)
  subᶜ-renᶜ c ρ σ = begin
    M.subᶜ (M.renᶜ c ρ) σ                   ≡⟨ subᶜ-assoc c (ρ ⨾ M.var) σ ⟩
    M.subᶜ c (ρ ⨾ λ ◌ → M.subᵛ (M.var ◌) σ) ≡⟨ subᶜ-cong c (tabulate≈ $ λ i → subᵛ-var (ρ ＠ i) σ) ⟩
    M.subᶜ c (ρ ⨾′ σ)                       ∎

  renᵛ-assoc :
    (v : M.Val A Γ) (ρ : Γ ↝ Δ) (ϱ : Δ ↝ Θ) →
    M.renᵛ (M.renᵛ v ρ) ϱ ≡ M.renᵛ v (ρ ⨾′ ϱ)
  renᵛ-assoc v ρ ϱ = begin
    M.renᵛ (M.renᵛ v ρ) ϱ                   ≡⟨ subᵛ-assoc v (ρ ⨾ M.var) (ϱ ⨾ M.var) ⟩
    M.subᵛ v (ρ ⨾ λ ◌ → M.renᵛ (M.var ◌) ϱ) ≡⟨ subᵛ-cong v (tabulate≈ $ λ i → renᵛ-var (ρ ＠ i) ϱ) ⟩
    M.renᵛ v (ρ ⨾′ ϱ)                       ∎

  renᶜ-assoc :
    (c : M.Comp B Γ) (ρ : Γ ↝ Δ) (ϱ : Δ ↝ Θ) →
    M.renᶜ (M.renᶜ c ρ) ϱ ≡ M.renᶜ c (ρ ⨾′ ϱ)
  renᶜ-assoc c ρ ϱ = begin
    M.renᶜ (M.renᶜ c ρ) ϱ                   ≡⟨ subᶜ-assoc c (ρ ⨾ M.var) (ϱ ⨾ M.var) ⟩
    M.subᶜ c (ρ ⨾ λ ◌ → M.renᵛ (M.var ◌) ϱ) ≡⟨ subᶜ-cong c (tabulate≈ $ λ i → renᵛ-var (ρ ＠ i) ϱ) ⟩
    M.renᶜ c (ρ ⨾′ ϱ)                       ∎

  lift-ren :
    (Θ : Context) (ρ : Γ ↝ Δ) →
    M.lift Θ (ρ ⨾ M.var) ≈ lift′ Θ ρ ⨾ M.var
  lift-ren Θ ρ =
    copair-unique {X = M.Val} _ _ _
      (tabulate≈ $ λ i → begin
        M.var ((ρ ⨾ weaklF Θ ∥ weakr) ＠ weakl Θ ＠ i) ≡⟨ cong M.var (copair-weakl {Δ = Θ} (ρ ⨾ weaklF Θ) weakr ＠ i) ⟩
        M.var (weaklF Θ $ ρ ＠ i)                      ≡˘⟨ renᵛ-var (ρ ＠ i) (weakl Θ) ⟩
        M.renᵛ (M.var $ ρ ＠ i) (weakl Θ)              ∎)
      (tabulate≈ $ λ i → cong M.var (copair-weakr (ρ ⨾ weaklF Θ) weakr ＠ i))

record IsMonoidArrow
  (M N : RawMonoid)
  (fᵛ : RawMonoid.Val M ⇾ᵗ RawMonoid.Val N)
  (fᶜ : RawMonoid.Comp M ⇾ᵗ RawMonoid.Comp N) : Set
  where
  private
    module M = RawMonoid M
    module N = RawMonoid N
  field
    ⟨var⟩ : (i : Var A Γ) → fᵛ (M.var i) ≡ N.var i
    ⟨subᵛ⟩ :
      (v : M.Val A Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      fᵛ (M.subᵛ v σ) ≡ N.subᵛ (fᵛ v) (σ ⨾ fᵛ)
    ⟨subᶜ⟩ :
      (c : M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      fᶜ (M.subᶜ c σ) ≡ N.subᶜ (fᶜ c) (σ ⨾ fᵛ)

module MonArrow
  {M N}
  {fᵛ : RawMonoid.Val M ⇾ᵗ RawMonoid.Val N}
  {fᶜ : RawMonoid.Comp M ⇾ᵗ RawMonoid.Comp N}
  (arr : IsMonoidArrow M N fᵛ fᶜ)
  (Nᵐ : IsMonoid N)
  where

  private
    module M = RawMonoid M
    module N where
      open RawMonoid N public
      open IsMonoid Nᵐ public

  open IsMonoidArrow arr
  open ≡-Reasoning

  ⟨renᵛ⟩ : (v : M.Val A Γ) (ρ : Γ ↝ Δ) → fᵛ (M.renᵛ v ρ) ≡ N.renᵛ (fᵛ v) ρ
  ⟨renᵛ⟩ v ρ = begin
    fᵛ (M.renᵛ v ρ)                        ≡⟨ ⟨subᵛ⟩ v (ρ ⨾ M.var) ⟩
    N.subᵛ (fᵛ v) (ρ ⨾ λ ◌ → fᵛ (M.var ◌)) ≡⟨ N.subᵛ-cong (fᵛ v) (tabulate≈ $ λ i → ⟨var⟩ (ρ ＠ i)) ⟩
    N.renᵛ (fᵛ v) ρ                        ∎

  ⟨renᶜ⟩ : (c : M.Comp B Γ) (ρ : Γ ↝ Δ) → fᶜ (M.renᶜ c ρ) ≡ N.renᶜ (fᶜ c) ρ
  ⟨renᶜ⟩ c ρ = begin
    fᶜ (M.renᶜ c ρ)                        ≡⟨ ⟨subᶜ⟩ c (ρ ⨾ M.var) ⟩
    N.subᶜ (fᶜ c) (ρ ⨾ λ ◌ → fᵛ (M.var ◌)) ≡⟨ N.subᶜ-cong (fᶜ c) (tabulate≈ $ λ i → ⟨var⟩ (ρ ＠ i)) ⟩
    N.renᶜ (fᶜ c) ρ                        ∎

record IsAlgebra (M : RawAlgebra) : Set where
  private module M = RawAlgebra M
  field
    isMonoid : IsMonoid M.monoid

  open IsMonoid isMonoid public

  field
    sub-have :
      (v : M.Val A Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᶜ (M.have v be c) σ ≡ (M.have M.subᵛ v σ be M.subᶜ c (M.lift [< x :- A ] σ))
    sub-thunk :
      (c : M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᵛ (M.thunk c) σ ≡ M.thunk (M.subᶜ c σ)
    sub-force :
      (v : M.Val (U B) Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᶜ (M.force v) σ ≡ M.force (M.subᵛ v σ)
    sub-point : (σ : Γ ~[ M.Val ]↝ Δ) → M.subᵛ M.point σ ≡ M.point
    sub-drop :
      (v : M.Val 𝟙 Γ) (c : M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᶜ (M.drop v then c) σ ≡ (M.drop M.subᵛ v σ then M.subᶜ c σ)
    sub-pair :
      (v : M.Val A Γ) (w : M.Val A′ Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᵛ M.⟨ v , w ⟩ σ ≡ M.⟨ M.subᵛ v σ , M.subᵛ w σ ⟩
    sub-split :
      (v : M.Val (A × A′) Γ) (c : δᵗ [< x :- A , y :- A′ ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᶜ (M.split v then c) σ ≡
        (M.split M.subᵛ v σ then M.subᶜ c (M.lift [< x :- A , y :- A′ ] σ))
    sub-inl :
      (v : M.Val A Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᵛ (M.inl {A′ = A′} v) σ ≡ M.inl (M.subᵛ v σ)
    sub-inr :
      (v : M.Val A′ Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᵛ (M.inr {A = A} v) σ ≡ M.inr (M.subᵛ v σ)
    sub-case :
      (v : M.Val (A + A′) Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) (d : δᵗ [< y :- A′ ] M.Comp B Γ) →
      (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᶜ (M.case v of c or d) σ ≡
        (M.case M.subᵛ v σ of M.subᶜ c (M.lift [< x :- A ] σ) or M.subᶜ d (M.lift [< y :- A′ ] σ))
    sub-ret :
      (v : M.Val A Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᶜ (M.ret v) σ ≡ M.ret (M.subᵛ v σ)
    sub-bind :
      (c : M.Comp (F A) Γ) (d : δᵗ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᶜ (M.bind c to d) σ ≡ (M.bind M.subᶜ c σ to M.subᶜ d (M.lift [< x :- A ] σ))
    sub-bundle :
      (c : M.Comp B Γ) (d : M.Comp B′ Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᶜ M.⟪ c , d ⟫ σ ≡ M.⟪ M.subᶜ c σ , M.subᶜ d σ ⟫
    sub-fst :
      (c : M.Comp (B × B′) Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᶜ (M.fst c) σ ≡ M.fst (M.subᶜ c σ)
    sub-snd :
      (c : M.Comp (B × B′) Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᶜ (M.snd c) σ ≡ M.snd (M.subᶜ c σ)
    sub-pop :
      (c : δᵗ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᶜ (M.pop c) σ ≡ M.pop (M.subᶜ c (M.lift [< x :- A ] σ))
    sub-push :
      (v : M.Val A Γ) (c : M.Comp (A ⟶ B) Γ) (σ : Γ ~[ M.Val ]↝ Δ) →
      M.subᶜ (M.push v then c) σ ≡ (M.push M.subᵛ v σ then M.subᶜ c σ)

  open ≡-Reasoning

  ren-have :
    (v : M.Val A Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) →
    M.renᶜ (M.have v be c) ρ ≡ (M.have M.renᵛ v ρ be[ x ] M.renᶜ c (lift′ [< x :- A ] ρ))
  ren-have {x = x} v c ρ =
    begin
      M.renᶜ (M.have v be c) ρ
    ≡⟨ sub-have v c (ρ ⨾ M.var) ⟩
      (M.have M.renᵛ v ρ be M.subᶜ c (M.lift [< x :- _ ] (ρ ⨾ M.var)))
    ≡⟨ cong (λ ◌ → M.have M.renᵛ v ρ be ◌) (subᶜ-cong c $ lift-ren [< x :- _ ] ρ) ⟩
      (M.have M.renᵛ v ρ be[ x ] M.renᶜ c (lift′ [< x :- _ ] ρ))
    ∎

  ren-thunk :
    (c : M.Comp B Γ) (ρ : Γ ↝ Δ) →
    M.renᵛ (M.thunk c) ρ ≡ M.thunk (M.renᶜ c ρ)
  ren-thunk c ρ = sub-thunk c (ρ ⨾ M.var)

  ren-force :
    (v : M.Val (U B) Γ) (ρ : Γ ↝ Δ) →
    M.renᶜ (M.force v) ρ ≡ M.force (M.renᵛ v ρ)
  ren-force c ρ = sub-force c (ρ ⨾ M.var)

  ren-point : (ρ : Γ ↝ Δ) → M.renᵛ M.point ρ ≡ M.point
  ren-point ρ = sub-point (ρ ⨾ M.var)

  ren-drop :
    (v : M.Val 𝟙 Γ) (c : M.Comp B Γ) (ρ : Γ ↝ Δ) →
    M.renᶜ (M.drop v then c) ρ ≡ (M.drop M.renᵛ v ρ then M.renᶜ c ρ)
  ren-drop v c ρ = sub-drop v c (ρ ⨾ M.var)

  ren-pair :
    (v : M.Val A Γ) (w : M.Val A′ Γ) (ρ : Γ ↝ Δ) →
    M.renᵛ M.⟨ v , w ⟩ ρ ≡ M.⟨ M.renᵛ v ρ , M.renᵛ w ρ ⟩
  ren-pair v w ρ = sub-pair v w (ρ ⨾ M.var)

  ren-split :
    (v : M.Val (A × A′) Γ) (c : δᵗ [< x :- A , y :- A′ ] M.Comp B Γ) (ρ : Γ ↝ Δ) →
    M.renᶜ (M.split v then c) ρ ≡
    (M.split M.renᵛ v ρ then[ x , y ] M.renᶜ c (lift′ [< x :- _ , y :- _ ] ρ))
  ren-split {x = x} {y = y} v c ρ =
    begin
      M.renᶜ (M.split v then c) ρ
    ≡⟨ sub-split v c (ρ ⨾ M.var) ⟩
      (M.split M.subᵛ v (ρ ⨾ M.var) then M.subᶜ c (M.lift [< x :- _ , y :- _ ] (ρ ⨾ M.var)))
    ≡⟨ cong (λ ◌ → M.split M.subᵛ v (ρ ⨾ M.var) then ◌) (subᶜ-cong c $ lift-ren [< x :- _ , y :- _ ] ρ) ⟩
      (M.split M.renᵛ v ρ then[ x , y ] M.renᶜ c (lift′ [< x :- _ , y :- _ ] ρ))
    ∎

  ren-inl :
    (v : M.Val A Γ) (ρ : Γ ↝ Δ) →
    M.renᵛ (M.inl {A′ = A′} v) ρ ≡ M.inl (M.renᵛ v ρ)
  ren-inl v ρ = sub-inl v (ρ ⨾ M.var)

  ren-inr :
    (v : M.Val A′ Γ) (ρ : Γ ↝ Δ) →
    M.renᵛ (M.inr {A = A} v) ρ ≡ M.inr (M.renᵛ v ρ)
  ren-inr v ρ = sub-inr v (ρ ⨾ M.var)

  ren-case :
    (v : M.Val (A + A′) Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) (d : δᵗ [< y :- A′ ] M.Comp B Γ) →
    (ρ : Γ ↝ Δ) →
    M.renᶜ (M.case v of c or d) ρ ≡
    ( M.case M.renᵛ v ρ
    of[ x ] M.renᶜ c (lift′ [< x :- A ] ρ)
    or[ y ] M.renᶜ d (lift′ [< y :- A′ ] ρ))
  ren-case {x = x} {y = y} v c d ρ =
    begin
      M.renᶜ (M.case v of c or d) ρ
    ≡⟨ sub-case v c d (ρ ⨾ M.var) ⟩
      ( M.case M.subᵛ v (ρ ⨾ M.var)
      of M.subᶜ c (M.lift [< x :- _ ] (ρ ⨾ M.var))
      or M.subᶜ d (M.lift [< y :- _ ] (ρ ⨾ M.var)))
    ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → M.case M.subᵛ v (ρ ⨾ M.var) of ◌ᵃ or ◌ᵇ)
         (subᶜ-cong c $ lift-ren [< x :- _ ] ρ)
         (subᶜ-cong d $ lift-ren [< y :- _ ] ρ) ⟩
      ( M.case M.subᵛ v (ρ ⨾ M.var)
      of[ x ] M.renᶜ c (lift′ [< x :- _ ] ρ)
      or[ y ] M.renᶜ d (lift′ [< y :- _ ] ρ))
    ∎

  ren-ret :
    (v : M.Val A Γ) (ρ : Γ ↝ Δ) →
    M.renᶜ (M.ret v) ρ ≡ M.ret (M.renᵛ v ρ)
  ren-ret v ρ = sub-ret v (ρ ⨾ M.var)

  ren-bind :
    (c : M.Comp (F A) Γ) (d : δᵗ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) →
    M.renᶜ (M.bind c to d) ρ ≡ (M.bind M.renᶜ c ρ to[ x ] M.renᶜ d (lift′ [< x :- A ] ρ))
  ren-bind {x = x} c d ρ =
    begin
      M.renᶜ (M.bind c to d) ρ
    ≡⟨ sub-bind c d (ρ ⨾ M.var) ⟩
      (M.bind M.renᶜ c ρ to M.subᶜ d (M.lift [< x :- _ ] (ρ ⨾ M.var)))
    ≡⟨ cong (λ ◌ → M.bind M.renᶜ c ρ to ◌) (subᶜ-cong d $ lift-ren [< x :- _ ] ρ) ⟩
      (M.bind M.renᶜ c ρ to[ x ] M.renᶜ d (lift′ [< x :- _ ] ρ))
    ∎

  ren-bundle :
    (c : M.Comp B Γ) (d : M.Comp B′ Γ) (ρ : Γ ↝ Δ) →
    M.renᶜ M.⟪ c , d ⟫ ρ ≡ M.⟪ M.renᶜ c ρ , M.renᶜ d ρ ⟫
  ren-bundle c d ρ = sub-bundle c d (ρ ⨾ M.var)

  ren-fst :
    (c : M.Comp (B × B′) Γ) (ρ : Γ ↝ Δ) →
    M.renᶜ (M.fst c) ρ ≡ M.fst (M.renᶜ c ρ)
  ren-fst c ρ = sub-fst c (ρ ⨾ M.var)

  ren-snd :
    (c : M.Comp (B × B′) Γ) (ρ : Γ ↝ Δ) →
    M.renᶜ (M.snd c) ρ ≡ M.snd (M.renᶜ c ρ)
  ren-snd c ρ = sub-snd c (ρ ⨾ M.var)

  ren-pop :
    (c : δᵗ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) →
    M.renᶜ (M.pop c) ρ ≡ M.pop[ x ] (M.renᶜ c (lift′ [< x :- A ] ρ))
  ren-pop {x = x} c ρ =
    begin
      M.renᶜ (M.pop c) ρ
    ≡⟨ sub-pop c (ρ ⨾ M.var) ⟩
      M.pop (M.subᶜ c (M.lift [< x :- _ ] (ρ ⨾ M.var)))
    ≡⟨ cong M.pop (subᶜ-cong c $ lift-ren [< x :- _ ] ρ) ⟩
      M.pop[ x ] (M.renᶜ c (lift′ [< x :- _ ] ρ))
    ∎

  ren-push :
    (v : M.Val A Γ) (c : M.Comp (A ⟶ B) Γ) (ρ : Γ ↝ Δ) →
    M.renᶜ (M.push v then c) ρ ≡ (M.push M.renᵛ v ρ then M.renᶜ c ρ)
  ren-push v c ρ = sub-push v c (ρ ⨾ M.var)

record IsModel (M : RawAlgebra) : Set where
  private module M = RawAlgebra M
  field
    isAlgebra : IsAlgebra M

  open IsAlgebra isAlgebra public

  field
    have-beta :
      (v : M.Val A Γ) (c : δᵗ _ M.Comp B Γ) →
      (M.have v be c) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v)
    force-beta : (c : M.Comp B Γ) → M.force (M.thunk c) ≡ c
    thunk-eta : (v : M.Val (U B) Γ) → M.thunk (M.force v) ≡ v
    point-beta : (c : M.Comp B Γ) → (M.drop M.point then c) ≡ c
    drop-eta :
      (v : M.Val 𝟙 Γ) (c : δᵗ _ M.Comp B Γ) →
      (M.drop v then M.subᶜ c (id ⨾ M.var :< x ↦ M.point)) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v)
    pair-beta :
      (v : M.Val A Γ) (w : M.Val A′ Γ) (c : δᵗ _ M.Comp B Γ) →
      (M.split M.⟨ v , w ⟩ then c) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v :< y ↦ w)
    pair-eta :
      (v : M.Val (A × A′) Γ) (c : δᵗ _ M.Comp B Γ) →
        (M.split v then
          M.subᶜ c
            (  weakl [< y :- A , z :- A′ ] ⨾ M.var
            :< x ↦ M.⟨ M.var (%% y) , M.var (%% z) ⟩
            ))
      ≡
        M.subᶜ c (id ⨾ M.var :< x ↦ v)
    inl-beta :
      (v : M.Val A Γ) (c : δᵗ _ M.Comp B Γ) (d : δᵗ [< y :- A′ ] M.Comp B Γ) →
      (M.case (M.inl v) of c or d) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v)
    inr-beta :
      (v : M.Val A′ Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) (d : δᵗ _ M.Comp B Γ) →
      (M.case (M.inr v) of c or d) ≡ M.subᶜ d (id ⨾ M.var :< y ↦ v)
    case-eta :
      (v : M.Val (A + A′) Γ) (c : δᵗ _ M.Comp B Γ) →
        ( M.case v
          of M.subᶜ c (weakl [< y :- A ]  ⨾ M.var :< x ↦ M.inl (M.var $ %% y))
          or M.subᶜ c (weakl [< z :- A′ ] ⨾ M.var :< x ↦ M.inr (M.var $ %% z)))
      ≡
        M.subᶜ c (id ⨾ M.var :< x ↦ v)
    ret-beta :
      (v : M.Val A Γ) (c : δᵗ _ M.Comp B Γ) →
      (M.bind M.ret v to c) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v)
    bind-bind-comm :
      (c : M.Comp (F A) Γ) (d : δᵗ [< x :- A ] M.Comp (F A′) Γ) (e : δᵗ [< y :- A′ ] M.Comp B Γ) →
        (M.bind (M.bind c to d) to e)
      ≡
        (M.bind c to M.bind d to M.subᶜ e (weakl [< x :- _ , y :- _ ] ⨾ M.var :< y ↦ M.var (%% y)))
    bind-fst-comm :
      (c : M.Comp (F A) Γ) (d : δᵗ [< x :- A ] M.Comp (B × B′) Γ) →
      (M.bind c to M.fst d) ≡ M.fst (M.bind c to d)
    bind-snd-comm :
      (c : M.Comp (F A) Γ) (d : δᵗ [< x :- A ] M.Comp (B × B′) Γ) →
      (M.bind c to M.snd d) ≡ M.snd (M.bind c to d)
    bind-push-comm :
      (v : M.Val A Γ) (c : M.Comp (F A′) Γ) (d : δᵗ [< x :- A′ ] M.Comp (A ⟶ B) Γ) →
      (M.push v then M.bind c to d) ≡ (M.bind c to M.push M.subᵛ v (weakl _ ⨾ M.var) then d)
    fst-beta : (c : M.Comp B Γ) (d : M.Comp B′ Γ) → M.fst M.⟪ c , d ⟫ ≡ c
    snd-beta : (c : M.Comp B Γ) (d : M.Comp B′ Γ) → M.snd M.⟪ c , d ⟫ ≡ d
    bundle-eta : (c : M.Comp (B × B′) Γ) → M.⟪ M.fst c , M.snd c ⟫ ≡ c
    push-beta :
      (v : M.Val A Γ) (c : δᵗ _ M.Comp B Γ) →
      (M.push v then M.pop c) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v)
    push-eta :
      (c : M.Comp (A ⟶ B) Γ) →
      M.pop (M.push (M.var $ %% x) then M.subᶜ c (weakl [< x :- _ ] ⨾ M.var)) ≡ c

record IsAlgebraArrow
  (M N : RawAlgebra)
  (fᵛ : M .Val ⇾ᵗ N .Val) (fᶜ : M .Comp ⇾ᵗ N .Comp) : Set
  where
  private
    module M = RawAlgebra M
    module N = RawAlgebra N
  field
    isMonoidArrow : IsMonoidArrow M.monoid N.monoid fᵛ fᶜ
    ⟨have⟩ : (v : M.Val A Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) → fᶜ (M.have v be c) ≡ (N.have fᵛ v be fᶜ c)
    ⟨thunk⟩ : (c : M.Comp B Γ) → fᵛ (M.thunk c) ≡ N.thunk (fᶜ c)
    ⟨force⟩ : (v : M.Val (U B) Γ) → fᶜ (M.force v) ≡ N.force (fᵛ v)
    ⟨point⟩ : fᵛ M.point ≡ N.point {Γ = Γ}
    ⟨drop⟩ : (v : M.Val 𝟙 Γ) (c : M.Comp B Γ) → fᶜ (M.drop v then c) ≡ (N.drop fᵛ v then fᶜ c)
    ⟨pair⟩ : (v : M.Val A Γ) (w : M.Val A′ Γ) → fᵛ M.⟨ v , w ⟩ ≡ N.⟨ fᵛ v , fᵛ w ⟩
    ⟨split⟩ :
      (v : M.Val (A × A′) Γ) (c : δᵗ [< x :- A , y :- A′ ] M.Comp B Γ) →
      fᶜ (M.split v then c) ≡ (N.split fᵛ v then fᶜ c)
    ⟨inl⟩ : (v : M.Val A  Γ) → fᵛ {A + A′} (M.inl v) ≡ N.inl (fᵛ v)
    ⟨inr⟩ : (v : M.Val A′ Γ) → fᵛ {A + A′} (M.inr v) ≡ N.inr (fᵛ v)
    ⟨case⟩ :
      (v : M.Val (A + A′) Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) (d : δᵗ [< y :- A′ ] M.Comp B Γ) →
      fᶜ (M.case v of c or d) ≡ (N.case fᵛ v of fᶜ c or fᶜ d)
    ⟨ret⟩ : (v : M.Val A Γ) → fᶜ (M.ret v) ≡ N.ret (fᵛ v)
    ⟨bind⟩ : (c : M.Comp (F A) Γ) (d : δᵗ [< x :- A ] M.Comp B Γ) → fᶜ (M.bind c to d) ≡ (N.bind fᶜ c to fᶜ d)
    ⟨bundle⟩ : (c : M.Comp B Γ) (d : M.Comp B′ Γ) → fᶜ M.⟪ c , d ⟫ ≡ N.⟪ fᶜ c , fᶜ d ⟫
    ⟨fst⟩ : (c : M.Comp (B × B′) Γ) → fᶜ (M.fst c) ≡ N.fst (fᶜ c)
    ⟨snd⟩ : (c : M.Comp (B × B′) Γ) → fᶜ (M.snd c) ≡ N.snd (fᶜ c)
    ⟨pop⟩ : (c : δᵗ [< x :- A ] M.Comp B Γ) → fᶜ (M.pop c) ≡ N.pop (fᶜ c)
    ⟨push⟩ : (v : M.Val A Γ) (c : M.Comp (A ⟶ B) Γ) → fᶜ (M.push v then c) ≡ (N.push fᵛ v then fᶜ c)

record IsCompExtension {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawCompExtension A Θ Ψ T) : Set where
  open RawCompExtension M
  field
    isModel : IsModel X
    sta-arrow : IsAlgebraArrow A X staᵛ staᶜ
    dyn-sub :
      (vs : All (λ A → X .Val A Γ) Θ) (cs : All (λ A → X .Comp A Γ) Ψ) (σ : Γ ~[ X .Val ]↝ Δ) →
      X .subᶜ (dyn vs cs) σ ≡ dyn (map (λ ◌ → X .subᵛ ◌ σ) vs) (map (λ ◌ → X .subᶜ ◌ σ) cs)

record IsValExtension {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawValExtension A Θ Ψ T) : Set where
  open RawValExtension M
  field
    isModel : IsModel X
    sta-arrow : IsAlgebraArrow A X staᵛ staᶜ
    dyn-sub :
      (vs : All (λ A → X .Val A Γ) Θ) (cs : All (λ A → X .Comp A Γ) Ψ) (σ : Γ ~[ X .Val ]↝ Δ) →
      X .subᵛ (dyn vs cs) σ ≡ dyn (map (λ ◌ → X .subᵛ ◌ σ) vs) (map (λ ◌ → X .subᶜ ◌ σ) cs)

record IsCompExtArrow {A Θ Ψ T} (M N : RawCompExtension A Θ Ψ T)
  (fᵛ : RawCompExtension.X M .Val ⇾ᵗ RawCompExtension.X N .Val)
  (fᶜ : RawCompExtension.X M .Comp ⇾ᵗ RawCompExtension.X N .Comp) : Set
  where
  private
    module M = RawCompExtension M
    module N = RawCompExtension N
  field
    isAlgebraArrow : IsAlgebraArrow M.X N.X fᵛ fᶜ
    ⟨staᵛ⟩ : (v : A .Val A′ Γ) → fᵛ (M.staᵛ v) ≡ N.staᵛ v
    ⟨staᶜ⟩ : (c : A .Comp B Γ) → fᶜ (M.staᶜ c) ≡ N.staᶜ c
    ⟨dyn⟩ :
      (vs : All (λ A → M.X .Val A Γ) Θ) (cs : All (λ A → M.X .Comp A Γ) Ψ) →
      fᶜ (M.dyn vs cs) ≡ N.dyn (map fᵛ vs) (map fᶜ cs)

record IsValExtArrow {A Θ Ψ T} (M N : RawValExtension A Θ Ψ T)
  (fᵛ : RawValExtension.X M .Val ⇾ᵗ RawValExtension.X N .Val)
  (fᶜ : RawValExtension.X M .Comp ⇾ᵗ RawValExtension.X N .Comp) : Set
  where
  private
    module M = RawValExtension M
    module N = RawValExtension N
  field
    isAlgebraArrow : IsAlgebraArrow M.X N.X fᵛ fᶜ
    ⟨staᵛ⟩ : (v : A .Val A′ Γ) → fᵛ (M.staᵛ v) ≡ N.staᵛ v
    ⟨staᶜ⟩ : (c : A .Comp B Γ) → fᶜ (M.staᶜ c) ≡ N.staᶜ c
    ⟨dyn⟩ :
      (vs : All (λ A → M.X .Val A Γ) Θ) (cs : All (λ A → M.X .Comp A Γ) Ψ) →
      fᵛ (M.dyn vs cs) ≡ N.dyn (map fᵛ vs) (map fᶜ cs)

record IsFreeCompExt {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawFreeCompExtension A Θ Ψ T) : Set₁ where
  private module M = RawFreeCompExtension M
  open RawCompExtension
  field
    isExtension : IsCompExtension Aᴹ M.extension
    eval-homo :
      (ext : RawCompExtension A Θ Ψ T) →
      IsCompExtArrow M.extension ext (M.evalᵛ ext) (M.evalᶜ ext)
    eval-uniqueᵛ :
      (ext : RawCompExtension A Θ Ψ T) →
      (fᵛ : M.extension .X .Val ⇾ᵗ ext .X .Val) →
      (fᶜ : M.extension .X .Comp ⇾ᵗ ext .X .Comp) →
      IsCompExtArrow M.extension ext fᵛ fᶜ →
      (v : M.extension .X .Val A′ Γ) →
      fᵛ v ≡ M.evalᵛ ext v
    eval-uniqueᶜ :
      (ext : RawCompExtension A Θ Ψ T) →
      (fᵛ : M.extension .X .Val ⇾ᵗ ext .X .Val) →
      (fᶜ : M.extension .X .Comp ⇾ᵗ ext .X .Comp) →
      IsCompExtArrow M.extension ext fᵛ fᶜ →
      (c : M.extension .X .Comp B Γ) →
      fᶜ c ≡ M.evalᶜ ext c

record IsFreeValExt {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawFreeValExtension A Θ Ψ T) : Set₁ where
  private module M = RawFreeValExtension M
  open RawValExtension
  field
    isExtension : IsValExtension Aᴹ M.extension
    eval-homo :
      (ext : RawValExtension A Θ Ψ T) →
      IsValExtArrow M.extension ext (M.evalᵛ ext) (M.evalᶜ ext)
    eval-uniqueᵛ :
      (ext : RawValExtension A Θ Ψ T) →
      (fᵛ : M.extension .X .Val ⇾ᵗ ext .X .Val) →
      (fᶜ : M.extension .X .Comp ⇾ᵗ ext .X .Comp) →
      IsValExtArrow M.extension ext fᵛ fᶜ →
      (v : M.extension .X .Val A′ Γ) →
      fᵛ v ≡ M.evalᵛ ext v
    eval-uniqueᶜ :
      (ext : RawValExtension A Θ Ψ T) →
      (fᵛ : M.extension .X .Val ⇾ᵗ ext .X .Val) →
      (fᶜ : M.extension .X .Comp ⇾ᵗ ext .X .Comp) →
      IsValExtArrow M.extension ext fᵛ fᶜ →
      (c : M.extension .X .Comp B Γ) →
      fᶜ c ≡ M.evalᶜ ext c