{-# OPTIONS --allow-unsolved-metas #-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Univalence using (ua)
open import Cubical.Data.Equality.Conversion using (eqToPath)
open import Cubical.Data.Nat

module Calf.Computation.CList2 where

open import Calf.Core.Cost
open import Calf.Value
open import Calf.Value.List
open import Calf.Value.Nat
import Calf.Value.Closed as ●
import Calf.Value.Open as ◯
open import Calf.Computation
open import Calf.Computation.Free as F
open import Calf.Computation.Copower
open import Calf.Computation.Open as ◯ᶜ
open import Calf.Computation.Closed as ●ᶜ
open import Calf.Computation.Glue
open import Calf.Computation.Abstraction
open import Calf.Computation.Potential
open import Calf.Computation.Credit

-- binom2 : ℕ → ℕ
-- binom2 zero = zero
-- binom2 (suc n) = n + binom2 n

-- clist₂-potential : ℂ → ℂ → ℕ → ℂ
-- clist₂-potential c-linear c-quadratic n =
--   (n ⊙ c-linear) +ℂ (binom2 n ⊙ c-quadratic)

-- module _ where
--   clist₂-potential-suc
--     : ∀ n c-linear c-quadratic
--     → clist₂-potential c-linear c-quadratic (suc n)
--       ≡ c-linear +ℂ clist₂-potential (c-quadratic +ℂ c-linear) c-quadratic n
--   clist₂-potential-suc n c-linear c-quadratic =
--       clist₂-potential c-linear c-quadratic (suc n)
--     ≡⟨ refl ⟩
--       (c-linear +ℂ (n ⊙ c-linear))
--         +ℂ ((n + binom2 n) ⊙ c-quadratic)
--     ≡⟨ cong
--         ((c-linear +ℂ (n ⊙ c-linear)) +ℂ_)
--         (⊙-+-left n (binom2 n) c-quadratic) ⟩
--       (c-linear +ℂ (n ⊙ c-linear))
--         +ℂ ((n ⊙ c-quadratic) +ℂ (binom2 n ⊙ c-quadratic))
--     ≡⟨ +ℂ-assoc c-linear (n ⊙ c-linear)
--         ((n ⊙ c-quadratic) +ℂ (binom2 n ⊙ c-quadratic)) ⟩
--       c-linear +ℂ
--         ((n ⊙ c-linear)
--           +ℂ ((n ⊙ c-quadratic) +ℂ (binom2 n ⊙ c-quadratic)))
--     ≡⟨ cong (c-linear +ℂ_)
--         (sym (+ℂ-assoc (n ⊙ c-linear) (n ⊙ c-quadratic) (binom2 n ⊙ c-quadratic))) ⟩
--       c-linear +ℂ
--         (((n ⊙ c-linear) +ℂ (n ⊙ c-quadratic))
--           +ℂ (binom2 n ⊙ c-quadratic))
--     ≡⟨ cong
--         (λ c → c-linear +ℂ (c +ℂ (binom2 n ⊙ c-quadratic)))
--         (+ℂ-comm (n ⊙ c-linear) (n ⊙ c-quadratic)) ⟩
--       c-linear +ℂ
--         (((n ⊙ c-quadratic) +ℂ (n ⊙ c-linear))
--           +ℂ (binom2 n ⊙ c-quadratic))
--     ≡⟨ cong (c-linear +ℂ_)
--         (cong (_+ℂ (binom2 n ⊙ c-quadratic))
--           (sym (⊙-+ n c-quadratic c-linear))) ⟩
--       c-linear +ℂ clist₂-potential (c-quadratic +ℂ c-linear) c-quadratic n
--     ∎

opaque
  CList₂ : ℂ → ℂ → 𝒱 → 𝒞
  CList₂ c-linear c-quadratic X = ?
    -- Potential {List X} (clist₂-potential c-linear c-quadratic ∘ length)

  cnil₂ : ∀ {c-lin c-quad} → U (CList₂ c-lin c-quad X)
  cnil₂ {X} {c-lin} {c-quad} = ?
    -- triangleᶜ'
    --   (ret [])
    --   (ret [])
    --   $
    --     bind' (λ l → F _ .charge (clist₂-potential c-lin c-quad (length l)) (ret l)) .U (ret [])
    --   ≡⟨ bind'/β ⟩
    --     F _ .charge (0ℂ +ℂ 0ℂ) (ret [])
    --   ≡⟨ cong (λ c → F _ .charge c (ret [])) (+ℂ-identityˡ 0ℂ) ⟩
    --     F _ .charge 0ℂ (ret [])
    --   ≡⟨ F _ .charge/0 ⟩
    --     ret []
    --   ∎

  ccons₂ : ∀ {c-lin c-quad} → X → ▷[ c-lin ] (CList₂ (c-quad +ℂ c-lin) c-quad X) ⊸ CList₂ c-lin c-quad X
  ccons₂ {X} {c-lin} {c-quad} x = ?
    -- subst (_⊸ CList₂ c-lin c-quad X)
    --   ( Abstractionᶜ (F (List X)) (F (List X))
    --       (CHARGE c-lin ⨾ᶜ bind' (λ l → F _ .charge (clist₂-potential (c-quad +ℂ c-lin) c-quad (length l)) (ret l)))
    --   ≡⟨ cong (Abstractionᶜ _ _) (CHARGE-commute _ _) ⟩
    --     Abstractionᶜ (F (List X)) (F (List X))
    --       (bind' (λ l → F _ .charge (clist₂-potential (c-quad +ℂ c-lin) c-quad (length l)) (ret l)) ⨾ᶜ CHARGE c-lin)
    --   ≡⟨ sym Abstractionᶜ-Abstractionᶜ ⟩
    --     Abstractionᶜ
    --       (CList₂ (c-quad +ℂ c-lin) c-quad X)
    --       (CList₂ (c-quad +ℂ c-lin) c-quad X)
    --       (squareᶜ'
    --         (CHARGE c-lin)
    --         (CHARGE c-lin)
    --         (λ e → bind' (λ l → F _ .charge (clist₂-potential (c-quad +ℂ c-lin) c-quad (length l)) (ret l)) .charge c-lin e))
    --   ≡⟨ cong (Abstractionᶜ _ _) (squareᶜ'-charge _) ⟩
    --     ▷[ c-lin ] (CList₂ (c-quad +ℂ c-lin) c-quad X)
    --   ∎) $
    -- squareᶜ'
    --   (F.map (x ∷_))
    --   (F.map (x ∷_))
    --   λ e →
    --     bind' (λ l → F (List X) .charge (clist₂-potential c-lin c-quad (length l)) (ret l)) .U (F.map (x ∷_) .U e)
    --   ≡⟨ refl ⟩
    --     bind' (λ l → F (List X) .charge (clist₂-potential c-lin c-quad (length l)) (ret l)) .U (bind' (ret ∘ (x ∷_)) .U e)
    --   ≡⟨ bind'-assoc _ _ _ ⟩
    --     bind' (λ l →
    --       bind' (λ l →
    --         F (List X) .charge (clist₂-potential c-lin c-quad (length l)) (ret l))
    --       .U (ret (x ∷ l)))
    --     .U e
    --   ≡⟨ cong (λ h → bind' {A = F (List X)} h .U e) (funExt λ _ → bind'/β) ⟩
    --     bind' (λ l →
    --       F (List X) .charge (clist₂-potential c-lin c-quad (length (x ∷ l))) (ret (x ∷ l)))
    --     .U e
    --   ≡⟨ cong (λ h → bind' {A = F (List X)} h .U e)
    --         (funExt λ l →
    --           cong (λ c → F (List X) .charge c (ret (x ∷ l)))
    --             (clist₂-potential-suc (length l) c-lin c-quad)) ⟩
    --     bind' (λ l →
    --       F (List X) .charge
    --         (c-lin +ℂ clist₂-potential (c-quad +ℂ c-lin) c-quad (length l))
    --         (ret (x ∷ l)))
    --     .U e
    --   ≡⟨ cong (λ h → bind' {A = F (List X)} h .U e) (funExt λ l → F (List X) .charge/+) ⟩
    --     bind' (λ l →
    --       F (List X) .charge c-lin
    --         (F (List X) .charge
    --           (clist₂-potential (c-quad +ℂ c-lin) c-quad (length l))
    --           (ret (x ∷ l))))
    --     .U e
    --   ≡⟨ bind'-charge _ _ _ ⟩
    --     bind' (λ l →
    --       F (List X) .charge
    --         (clist₂-potential (c-quad +ℂ c-lin) c-quad (length l))
    --         (ret (x ∷ l)))
    --     .U (F (List X) .charge c-lin e)
    --   ≡⟨ sym
    --         (cong (λ h → bind' {A = F (List X)} h .U (F (List X) .charge c-lin e))
    --           (funExt λ l →
    --             cong (F (List X) .charge (clist₂-potential (c-quad +ℂ c-lin) c-quad (length l))) bind'/β)) ⟩
    --     bind' (λ l →
    --       F (List X) .charge
    --         (clist₂-potential (c-quad +ℂ c-lin) c-quad (length l))
    --         (F.map (x ∷_) .U (ret l)))
    --     .U (F (List X) .charge c-lin e)
    --   ≡⟨ sym
    --         (cong (λ h → bind' {A = F (List X)} h .U (F (List X) .charge c-lin e))
    --           (funExt λ l →
    --             F.map (x ∷_) .charge (clist₂-potential (c-quad +ℂ c-lin) c-quad (length l)) (ret l))) ⟩
    --     bind' (λ l →
    --       F.map (x ∷_) .U
    --         (F (List X) .charge (clist₂-potential (c-quad +ℂ c-lin) c-quad (length l)) (ret l)))
    --     .U (F (List X) .charge c-lin e)
    --   ≡⟨ sym (bind'-assoc _ _ _) ⟩
    --     F.map (x ∷_) .U
    --       (bind' (λ l →
    --         F (List X) .charge (clist₂-potential (c-quad +ℂ c-lin) c-quad (length l)) (ret l))
    --       .U (F (List X) .charge c-lin e))
    --   ∎

  cfoldr₂ : ∀ {c-lin c-quad} (A : ℂ → 𝒞)
    → (∀ c-lin → U (A c-lin))
    → (∀ c-lin → X → (▷[ c-lin ] (A (c-quad +ℂ c-lin))) ⊸ A c-lin)
    → CList₂ c-lin c-quad X ⊸ A c-lin
  cfoldr₂ {X = X} {c-lin = c-lin} {c-quad = c-quad} A e-nil e-cons = ?
    -- subst (CList₂ c-lin c-quad X ⊸_) (𝒞-glue-fracture-retract (A c-lin)) $
    -- squareᶜ (go• c-lin) (go◦ c-lin) go-•⊸◦
    -- where
    --   costᶜ-at : ℂ → F (List X) ⊸ F (List X)
    --   costᶜ-at c =
    --     bind' {A = F _} λ l →
    --     CHARGE {A = F _} (clist₂-potential c c-quad (length l)) .U (ret l)

    --   costᶜ : F (List X) ⊸ F (List X)
    --   costᶜ = costᶜ-at c-lin

    --   fold• : (List X) → (c : ℂ) → U (●ᶜ (A c))
    --   fold• =
    --     foldr
    --       (λ x rec c →
    --         ●.map (e-cons c x .U)
    --           (transport
    --             (cong U (sym (▷-●ᶜ c (A (c-quad +ℂ c)))))
    --             (rec (c-quad +ℂ c))))
    --       (λ c → η• (e-nil c))

    --   go• : (c : ℂ) → ●ᶜ (F (List X)) ⊸ ●ᶜ (A c)
    --   go• c =
    --     ●ᶜ.bind $
    --     bind' (λ l → fold• l c)

    --   open-econs : (c : ℂ) → X → ◯ᶜ (A (c-quad +ℂ c)) ⊸ ◯ᶜ (A c)
    --   open-econs c x .U a◦ =
    --     ◯.map (e-cons c x .U)
    --       (transport (cong U (sym (▷-◯ᶜ c (A (c-quad +ℂ c))))) a◦)
    --   open-econs c x .charge d a◦ = funExt λ abs →
    --       e-cons c x .U
    --         (transport (cong U (sym (▷-◯ᶜ c (A (c-quad +ℂ c)))))
    --           (◯ᶜ (A (c-quad +ℂ c)) .charge d a◦)
    --           abs)
    --     ≡⟨ cong (λ q → e-cons c x .U (q abs))
    --           (transport-charge (sym (▷-◯ᶜ c (A (c-quad +ℂ c)))) d a◦) ⟩
    --       e-cons c x .U
    --         ((◯ᶜ (▷[ c ] (A (c-quad +ℂ c))) .charge d
    --           (transport (cong U (sym (▷-◯ᶜ c (A (c-quad +ℂ c))))) a◦)) abs)
    --     ≡⟨ e-cons c x .charge d
    --           (transport (cong U (sym (▷-◯ᶜ c (A (c-quad +ℂ c))))) a◦ abs) ⟩
    --       A c .charge d
    --         (e-cons c x .U
    --           (transport (cong U (sym (▷-◯ᶜ c (A (c-quad +ℂ c))))) a◦ abs))
    --     ∎

    --   fold◦ : (List X) → (c : ℂ) → U (◯ᶜ (A c))
    --   fold◦ =
    --     foldr
    --       (λ x rec c → open-econs c x .U (rec (c-quad +ℂ c)))
    --       (λ c → η◦ (e-nil c))

    --   go◦ : (c : ℂ) → ◯ᶜ (F (List X)) ⊸ ◯ᶜ (A c)
    --   go◦ c =
    --     ◯ᶜ.bind {A = F _} {B = A c} $
    --     bind' (λ l → fold◦ l c)

    --   fold•ᶜ : (c : ℂ) → F (List X) ⊸ ●ᶜ (A c)
    --   fold•ᶜ c = bind' (λ l → fold• l c)

    --   go-•⊸◦ :
    --     go• c-lin ⨾ᶜ ●ᶜ.map η◦ᶜ ≡ ●ᶜ.map (costᶜ ⨾ᶜ η◦ᶜ) ⨾ᶜ ●ᶜ.map (go◦ c-lin)
    --   go-•⊸◦ =
    --       go• c-lin ⨾ᶜ ●ᶜ.map η◦ᶜ
    --     ≡⟨ refl ⟩
    --       ●ᶜ.bind (fold•ᶜ c-lin) ⨾ᶜ ●ᶜ.map η◦ᶜ
    --     ≡⟨ ●ᶜ.bind-map _ _ ⟩
    --       ●ᶜ.bind (fold•ᶜ c-lin ⨾ᶜ ●ᶜ.map η◦ᶜ)
    --     ≡⟨ cong ●ᶜ.bind (bind'-path _ _ (funExt (fold•-coherence c-lin))) ⟩
    --       ●ᶜ.bind (costᶜ ⨾ᶜ η◦ᶜ ⨾ᶜ go◦ c-lin ⨾ᶜ η•ᶜ)
    --     ≡⟨ ●ᶜ.bind-η• _ ⟩
    --       ●ᶜ.map (costᶜ ⨾ᶜ η◦ᶜ ⨾ᶜ go◦ c-lin)
    --     ≡⟨ sym (●ᶜ.map-∘ _ _) ⟩
    --       ●ᶜ.map (costᶜ ⨾ᶜ η◦ᶜ) ⨾ᶜ ●ᶜ.map (go◦ c-lin)
    --     ∎
    --     where
    --       cost-nil : ∀ c → costᶜ-at c .U (ret []) ≡ ret []
    --       cost-nil c =
    --           costᶜ-at c .U (ret [])
    --         ≡⟨ bind'/β ⟩
    --           F (List X) .charge (0ℂ +ℂ 0ℂ) (ret [])
    --         ≡⟨ cong (λ c → F (List X) .charge c (ret [])) (+ℂ-identityˡ 0ℂ) ⟩
    --           F (List X) .charge 0ℂ (ret [])
    --         ≡⟨ F (List X) .charge/0 ⟩
    --           ret []
    --         ∎

    --       cost-cons : ∀ c x l →
    --         CHARGE {A = F _} c .U
    --           (F.map (x ∷_) .U (costᶜ-at (c-quad +ℂ c) .U (ret l)))
    --         ≡ costᶜ-at c .U (ret (x ∷ l))
    --       cost-cons c x l =
    --           CHARGE {A = F _} c .U
    --             (F.map (x ∷_) .U (costᶜ-at (c-quad +ℂ c) .U (ret l)))
    --         ≡⟨ cong (λ e → CHARGE {A = F _} c .U (F.map (x ∷_) .U e)) bind'/β ⟩
    --           CHARGE {A = F _} c .U
    --             (F.map (x ∷_) .U
    --               (CHARGE {A = F _} (clist₂-potential (c-quad +ℂ c) c-quad (length l)) .U (ret l)))
    --         ≡⟨ cong (CHARGE {A = F _} c .U)
    --               (cong ((_$ ret l) ∘ U)
    --                 (CHARGE-commute
    --                   (clist₂-potential (c-quad +ℂ c) c-quad (length l))
    --                   (F.map (x ∷_)))) ⟩
    --           CHARGE {A = F _} c .U
    --             (CHARGE {A = F _} (clist₂-potential (c-quad +ℂ c) c-quad (length l)) .U
    --               (F.map (x ∷_) .U (ret l)))
    --         ≡⟨ cong (λ e → CHARGE {A = F _} c .U
    --               (CHARGE {A = F _} (clist₂-potential (c-quad +ℂ c) c-quad (length l)) .U e))
    --               bind'/β ⟩
    --           CHARGE {A = F _} c .U
    --             (CHARGE {A = F _} (clist₂-potential (c-quad +ℂ c) c-quad (length l)) .U
    --               (ret (x ∷ l)))
    --         ≡⟨ sym (cong ((_$ ret (x ∷ l)) ∘ U)
    --               (CHARGE-+ {A = F _} c (clist₂-potential (c-quad +ℂ c) c-quad (length l)))) ⟩
    --           CHARGE {A = F _}
    --             (c +ℂ clist₂-potential (c-quad +ℂ c) c-quad (length l)) .U
    --             (ret (x ∷ l))
    --         ≡⟨ cong (λ c → CHARGE {A = F _} c .U (ret (x ∷ l)))
    --               (sym (clist₂-potential-suc (length l) c c-quad)) ⟩
    --           CHARGE {A = F _}
    --             (clist₂-potential c c-quad (length (x ∷ l))) .U
    --             (ret (x ∷ l))
    --         ≡⟨ sym bind'/β ⟩
    --           costᶜ-at c .U (ret (x ∷ l))
    --         ∎

    --       go◦-cons : ∀ c x (e : U (F (List X))) →
    --         go◦ c .U (η◦ᶜ {A = F _} .U (F.map (x ∷_) .U e))
    --         ≡ open-econs c x .U (go◦ (c-quad +ℂ c) .U (η◦ᶜ {A = F _} .U e))
    --       go◦-cons c x e =
    --           go◦ c .U (η◦ᶜ {A = F _} .U (F.map (x ∷_) .U e))
    --         ≡⟨ refl ⟩
    --           bind' (λ l → fold◦ l c) .U (F.map (x ∷_) .U e)
    --         ≡⟨ bind'-assoc _ _ _ ⟩
    --           bind' (λ l →
    --             bind' (λ l → fold◦ l c) .U (ret (x ∷ l)))
    --           .U e
    --         ≡⟨ cong (λ h → bind' {A = ◯ᶜ (A c)} h .U e) (funExt λ l → bind'/β) ⟩
    --           bind' (λ l →
    --             open-econs c x .U (fold◦ l (c-quad +ℂ c)))
    --           .U e
    --         ≡⟨ sym (bind'-map (open-econs c x) _ _) ⟩
    --           open-econs c x .U (bind' (λ l → fold◦ l (c-quad +ℂ c)) .U e)
    --         ≡⟨ refl ⟩
    --           open-econs c x .U (go◦ (c-quad +ℂ c) .U (η◦ᶜ {A = F _} .U e))
    --         ∎

    --       open-cons-charge : ∀ c x l →
    --         ◯.map (e-cons c x .U)
    --           (transport (cong U (sym (▷-◯ᶜ c (A (c-quad +ℂ c)))))
    --             (CHARGE {A = ◯ᶜ (A (c-quad +ℂ c))} c .U
    --               ((costᶜ-at (c-quad +ℂ c) ⨾ᶜ η◦ᶜ ⨾ᶜ go◦ (c-quad +ℂ c)) .U (ret l))))
    --         ≡ (costᶜ-at c ⨾ᶜ η◦ᶜ ⨾ᶜ go◦ c) .U (ret (x ∷ l))
    --       open-cons-charge c x l =
    --         let
    --           e = costᶜ-at (c-quad +ℂ c) .U (ret l)
    --           s = go◦ (c-quad +ℂ c) .U (η◦ᶜ {A = F _} .U e)
    --         in
    --           open-econs c x .U (CHARGE {A = ◯ᶜ (A (c-quad +ℂ c))} c .U s)
    --         ≡⟨ cong ((_$ s) ∘ U) (CHARGE-commute c (open-econs c x)) ⟩
    --           CHARGE {A = ◯ᶜ (A c)} c .U (open-econs c x .U s)
    --         ≡⟨ cong (CHARGE {A = ◯ᶜ (A c)} c .U)
    --               (sym (go◦-cons c x e)) ⟩
    --           CHARGE {A = ◯ᶜ (A c)} c .U
    --             (go◦ c .U (η◦ᶜ {A = F _} .U (F.map (x ∷_) .U e)))
    --         ≡⟨ sym (cong ((_$ η◦ᶜ {A = F _} .U (F.map (x ∷_) .U e)) ∘ U)
    --               (CHARGE-commute c (go◦ c))) ⟩
    --           go◦ c .U
    --             (η◦ᶜ {A = F _} .U
    --               (CHARGE {A = F _} c .U (F.map (x ∷_) .U e)))
    --         ≡⟨ cong (λ e → go◦ c .U (η◦ᶜ {A = F _} .U e)) (cost-cons c x l) ⟩
    --           go◦ c .U (η◦ᶜ {A = F _} .U (costᶜ-at c .U (ret (x ∷ l))))
    --         ∎

    --       fold•-coherence : ∀ c l →
    --         (fold•ᶜ c ⨾ᶜ ●ᶜ.map η◦ᶜ) .U (ret l)
    --         ≡ (costᶜ-at c ⨾ᶜ η◦ᶜ ⨾ᶜ go◦ c ⨾ᶜ η•ᶜ) .U (ret l)
    --       fold•-coherence c [] =
    --           (fold•ᶜ c ⨾ᶜ ●ᶜ.map η◦ᶜ) .U (ret [])
    --         ≡⟨ cong (●.map (η◦ᶜ {A = A c} .U)) bind'/β ⟩
    --           η•ᶜ {A = ◯ᶜ (A c)} .U (η◦ᶜ {A = A c} .U (e-nil c))
    --         ≡⟨ cong (η•ᶜ {A = ◯ᶜ (A c)} .U) (sym bind'/β) ⟩
    --           η•ᶜ {A = ◯ᶜ (A c)} .U
    --             (bind' (λ l → fold◦ l c) .U (ret []))
    --         ≡⟨ refl ⟩
    --           η•ᶜ {A = ◯ᶜ (A c)} .U
    --             (go◦ c .U (η◦ᶜ {A = F _} .U (ret [])))
    --         ≡⟨ cong
    --               (λ e → η•ᶜ {A = ◯ᶜ (A c)} .U
    --                 (go◦ c .U (η◦ᶜ {A = F _} .U e)))
    --               (sym (cost-nil c)) ⟩
    --           η•ᶜ {A = ◯ᶜ (A c)} .U
    --             (go◦ c .U (η◦ᶜ {A = F _} .U
    --               (costᶜ-at c .U (ret []))))
    --         ≡⟨ refl ⟩
    --           (costᶜ-at c ⨾ᶜ η◦ᶜ ⨾ᶜ go◦ c ⨾ᶜ η•ᶜ) .U (ret [])
    --         ∎
    --       fold•-coherence c (x ∷ l) =
    --           (fold•ᶜ c ⨾ᶜ ●ᶜ.map η◦ᶜ) .U (ret (x ∷ l))
    --         ≡⟨ cong (●.map (η◦ᶜ {A = A c} .U)) bind'/β ⟩
    --           ●.map (η◦ᶜ {A = A c} .U)
    --             (●.map (e-cons c x .U)
    --               (transport (cong U (sym (▷-●ᶜ c (A (c-quad +ℂ c)))))
    --                 (fold• l (c-quad +ℂ c))))
    --         ≡⟨ cong
    --             (λ q → ●.map (η◦ᶜ {A = A c} .U)
    --               (●.map (e-cons c x .U)
    --                 (transport (cong U (sym (▷-●ᶜ c (A (c-quad +ℂ c))))) q)))
    --             (sym bind'/β) ⟩
    --           ●.map (η◦ᶜ {A = A c} .U)
    --             (●.map (e-cons c x .U)
    --               (transport (cong U (sym (▷-●ᶜ c (A (c-quad +ℂ c)))))
    --                 (fold•ᶜ (c-quad +ℂ c) .U (ret l))))
    --         ≡⟨ (
    --           let
    --               q▷• =
    --                 transport
    --                   (cong U (sym (▷-●ᶜ c (A (c-quad +ℂ c)))))
    --                   (fold•ᶜ (c-quad +ℂ c) .U (ret l))
    --               q▷◦ =
    --                 transport
    --                   (cong U (sym (▷-◯ᶜ c (A (c-quad +ℂ c)))))
    --                   (CHARGE {A = ◯ᶜ (A (c-quad +ℂ c))} c .U
    --                     ((costᶜ-at (c-quad +ℂ c) ⨾ᶜ η◦ᶜ ⨾ᶜ go◦ (c-quad +ℂ c)) .U (ret l)))
    --               tr▷◦ =
    --                 transport
    --                   (cong (λ C → U (●ᶜ C)) (sym (▷-◯ᶜ c (A (c-quad +ℂ c)))))

    --               q▷-coh : ●ᶜ.map (η◦ᶜ {A = ▷[ c ] (A (c-quad +ℂ c))}) .U q▷• ≡ η• q▷◦
    --               q▷-coh =
    --                   ●ᶜ.map (η◦ᶜ {A = ▷[ c ] (A (c-quad +ℂ c))}) .U q▷•
    --                 ≡⟨ ? ⟩  -- transport-▷ c (A (c-quad +ℂ c)) (fold•ᶜ (c-quad +ℂ c) .U (ret l)) ⟩
    --                   tr▷◦
    --                     ((▷-FRAC c (A (c-quad +ℂ c)) .𝒞-FRACTURE.α•) .U
    --                       (fold•ᶜ (c-quad +ℂ c) .U (ret l)))
    --                 ≡⟨ cong tr▷◦
    --                     (sym (●.map-∘
    --                       (η◦ᶜ {A = A (c-quad +ℂ c)} .U)
    --                       (◯ᶜ (A (c-quad +ℂ c)) .charge c)
    --                       (fold•ᶜ (c-quad +ℂ c) .U (ret l)))) ⟩
    --                   tr▷◦
    --                     (●.map (CHARGE {A = ◯ᶜ (A (c-quad +ℂ c))} c .U)
    --                       ((fold•ᶜ (c-quad +ℂ c) ⨾ᶜ ●ᶜ.map η◦ᶜ) .U (ret l)))
    --                 ≡⟨ cong tr▷◦
    --                     (cong (●.map (CHARGE {A = ◯ᶜ (A (c-quad +ℂ c))} c .U))
    --                       (fold•-coherence (c-quad +ℂ c) l)) ⟩
    --                   η• q▷◦
    --                 ∎
    --             in
    --             fracture-map-coh (e-cons c x) q▷• q▷◦ q▷-coh
    --         ) ⟩
    --           η•ᶜ {A = ◯ᶜ (A c)} .U
    --             (◯.map (e-cons c x .U)
    --               (transport (cong U (sym (▷-◯ᶜ c (A (c-quad +ℂ c)))))
    --                 (CHARGE {A = ◯ᶜ (A (c-quad +ℂ c))} c .U
    --                   ((costᶜ-at (c-quad +ℂ c) ⨾ᶜ η◦ᶜ ⨾ᶜ go◦ (c-quad +ℂ c)) .U (ret l)))))
    --         ≡⟨ cong (η•ᶜ {A = ◯ᶜ (A c)} .U) (open-cons-charge c x l) ⟩
    --           (costᶜ-at c ⨾ᶜ η◦ᶜ ⨾ᶜ go◦ c ⨾ᶜ η•ᶜ) .U (ret (x ∷ l))
    --         ∎