{-# OPTIONS --allow-unsolved-metas #-}
module Uniform.Coproduct.Maps {D : Set₁} where

open import Prelude.Basic
open import Prelude.Equality
open import Prelude.Container
open import Prelude.Fam

open import Prelude.Equivalences
open _≃_

open import Data.Nat.Properties.Simple using (+-right-identity; +-suc)

open import Uniform.IR
open import Uniform.Coproduct {D}

-- for ease of chaining equivalences together, we define the decoding
-- of ranked containerised codes

mutual
  ⟦_⟧UniR : {n : ℕ} -> (G : UniR n)-> Fam D -> Set
  ⟦ ιR ⟧UniR Z = ⊤
  ⟦ δσR G H ⟧UniR Z@(U , T)
    = Σ[ x ∈ (⟦ G ⟧UniR Z) ] (cont (H (⟦ G ⟧InfoR Z x)) U)

  ⟦_⟧InfoR : {n : ℕ} -> (G : UniR n)(UT : Fam D) -> ⟦ G ⟧UniR UT -> InfoR G
  ⟦ ιR ⟧InfoR UT _ = lift tt
  ⟦ δσR G H ⟧InfoR Z@(U , T) (x , p)
    = (⟦ G ⟧InfoR Z x , cont-map (H _) T p)

⟦_⟧R : {E : Set1}{n : ℕ} ->  UFR E n -> Fam D -> Fam E
⟦_⟧R (c , α) Z = ⟦ c ⟧UniR Z , α ∘ ⟦ c ⟧InfoR Z


-- containerise equivalence

module ContaineriseEq {Z : Fam D} where

  mutual
    left0 : (c : Uni D) -> ⟦ containerise c ⟧UniR Z -> ⟦ c ⟧Uni Z
    left0 ι x = x
    left0 (σ G A) (x , a , _) = left0 G x , subst A (left1 G x) a
    left0 (δ G A) (x , _ , g)
      = left0 G x , (λ a → g (subst A (sym (left1 G x)) a))

    left1 : (c : Uni D) -> (x : ⟦ containerise c ⟧UniR Z) ->
               containeriseInfo c (⟦ containerise c ⟧InfoR Z x)
               ≡ ⟦ c ⟧Info Z (left0 c x)
    left1 ι _ = refl
    left1 (σ G A) (x , a , _) = Σ-≡ (left1 G x) refl
    left1 (δ G A) (x , _ , g)
      = Σ-≡ (left1 G x) (subst-dom (left1 G x))

  mutual
    right0 : (c : Uni D) -> ⟦ c ⟧Uni Z -> ⟦ containerise c ⟧UniR Z
    right0 ι x = x
    right0 (σ G A) (x , a)
      = right0 G x , subst A (right1 G x) a , ⊥-elim
    right0 (δ G A) (x , g)
      = right0 G x , _ , (λ a → g (subst A (sym (right1 G x)) a))

    right1 : (c : Uni D) -> (x : ⟦ c ⟧Uni Z) ->
             ⟦ c ⟧Info Z x
               ≡ containeriseInfo c (⟦ containerise c ⟧InfoR Z (right0 c x))
    right1 ι _ = refl
    right1 (σ G A) (x , a) = Σ-≡ (right1 G x) refl
    right1 (δ G A) (x , g)
      = Σ-≡ (right1 G x) (subst-dom (right1 G x))

  mutual
    leftright0 : (c : Uni D) ->
                 (x : ⟦ c ⟧Uni Z) -> x ≡ left0 c (right0 c x)
    leftright0 ι x = refl
    leftright0 (σ G A) (x , a)
      = Σ-≡ (leftright0 G x)
            (trans
              (subst-cong {B = A} (leftright0 G x))
              (trans
                (congSubst (leftright1 G x))
                (subst-trans (right1 G x) (left1 G (right0 G x)))))
    leftright0 (δ G A) (x , g)
      = Σ-≡ (leftright0 G x)
            (trans
              (subst-dom (leftright0 G x))
              (ext (λ a → cong g
                               (trans
                                 (subst-cong {B = A}
                                             (sym (leftright0 G x)))
                                 (trans
                                   (congSubst (leftright1-sym G x))
                                   (subst-trans
                                     (sym (left1 G (right0 G x)))
                                     (sym (right1 G x))))))))

    leftright1 : (c : Uni D) -> (x : ⟦ c ⟧Uni Z) ->
                   cong (⟦ c ⟧Info Z) (leftright0 c x)
                     ≡ trans (right1 c x) (left1 c (right0 c x))
    leftright1 c x = UIP _ _ --TODO: for now

    leftright1-sym : (c : Uni D) -> (x : ⟦ c ⟧Uni Z) ->
                       cong (⟦ c ⟧Info Z) (sym (leftright0 c x))
                         ≡ trans (sym (left1 c (right0 c x)))
                                 (sym (right1 c x))
    leftright1-sym c x
      = trans
         (sym-cong (leftright0 c x))
         (trans
           (cong sym (leftright1 c x))
           (trans-sym
             {x = containeriseInfo c
                    (⟦ containerise c ⟧InfoR Z (right0 c x))}
             {y = ⟦ c ⟧Info Z x}
             (right1 c x)
             (left1 c (right0 c x))))

  mutual
    rightleft0 : (c : Uni D) -> (x : ⟦ containerise c ⟧UniR Z) ->
                    x ≡ right0 c (left0 c x)
    rightleft0 ι x = refl
    rightleft0 (σ G A) (x , a , _)
      = Σ-≡ (rightleft0 G x)
            (Σ-≡ (trans
                   (sym (subst-natural proj₁ (rightleft0 G x)))
                   (trans
                     (subst-cong {B = A} (rightleft0 G x))
                     (trans
                       (congSubst (rightleft1 G x))
                       (subst-trans (left1 G x)
                                    (right1 G (left0 G x))))))
                 (ext (λ ())))
    rightleft0 (δ G A) (x , _ , g)
      = Σ-≡ (rightleft0 G x)
            (Σ-≡ refl
                 (trans
                   (sym (subst-natural proj₂ (rightleft0 G x)))
                   (trans
                     (subst-dom (rightleft0 G x))
                     (ext (λ a → cong g
                                      (trans
                                        (subst-cong
                                          (sym (rightleft0 G x)))
                                        (trans
                                          (congSubst {B = A}
                                            (rightleft1-sym G x))
                                          (subst-trans
                                            (sym (right1 G (left0 G x)))
                                            (sym (left1 G x))))))))))

    rightleft1 : (c : Uni D) -> (x : ⟦ containerise c ⟧UniR Z) ->
                   cong (containeriseInfo c ∘ (⟦ containerise c ⟧InfoR Z))
                        (rightleft0 c x)
                      ≡ trans (left1 c x) (right1 c (left0 c x))
    rightleft1 c x =  UIP _ _ --TODO: for now

    rightleft1-sym : (c : Uni D) -> (x : ⟦ containerise c ⟧UniR Z) ->
                   cong (containeriseInfo c ∘ (⟦ containerise c ⟧InfoR Z))
                        (sym (rightleft0 c x))
                      ≡ trans (sym (right1 c (left0 c x)))
                              (sym (left1 c x))
    rightleft1-sym c x = trans
                           (sym-cong (rightleft0 c x))
                           (trans
                             (cong sym (rightleft1 c x))
                             (trans-sym
                               {x = containeriseInfo c
                                      (⟦ containerise c ⟧InfoR Z x)}
                               {y = ⟦ c ⟧Info Z (left0 c x)}
                               (left1 c x)
                               (right1 c (left0 c x))))



containeriseEq :
  ∀ {E} -> (R : UF D E) -> {Z : Fam D} ->
 ⟦ containeriseUF R ⟧R Z ≃ ⟦ R ⟧ Z
left (containeriseEq (c , α))
 = (ContaineriseEq.left0 c , (cong α ∘ (ContaineriseEq.left1 c)))
right (containeriseEq (c , α))
 = (ContaineriseEq.right0 c , (cong α ∘ (ContaineriseEq.right1 c)))
leftright (containeriseEq R@(c , α))
 = comp-is-id-ext
    (left (containeriseEq R))
    (right (containeriseEq R))
    (ContaineriseEq.leftright0 c)
    (λ x → trans
            (trans-cong
              (ContaineriseEq.right1 c x)
              (ContaineriseEq.left1 c (ContaineriseEq.right0 c x)))
            (trans
              (cong (cong α) (sym (ContaineriseEq.leftright1 c x)))
              (sym (cong-cong (ContaineriseEq.leftright0 c x)))))
rightleft (containeriseEq R@(c , α))
 = comp-is-id-ext
    (right (containeriseEq R))
    (left (containeriseEq R))
    (ContaineriseEq.rightleft0 c)
    (λ x → trans
            (trans-cong
              (ContaineriseEq.left1 c x)
              (ContaineriseEq.right1 c (ContaineriseEq.left0 c x)))
            (trans
              (cong (cong α) (sym (ContaineriseEq.rightleft1 c x)))
              (sym (cong-cong (ContaineriseEq.rightleft0 c x)))))


-- forget equivalence
module ForgetEq {Z : Fam D} where

  subst-cont : ∀ {a b c d} → {A : Set a}{Z : Set b} -> (H : A -> Cont {c} {d}) ->
             {x y : A} -> (p : x ≡ y) -> {u : cont (H x) Z}{v : cont (H y) Z} ->
             (q : subst (proj₁ ∘ H) p (proj₁ u) ≡ proj₁ v) ->
             (∀ z → proj₂ u (subst (λ z → proj₂ (H (proj₁ z)) (proj₂ z)) (sym (Σ-≡ p q)) z) ≡ proj₂ v z) ->
             subst (λ z → cont (H z) Z) p u ≡ v
  subst-cont H refl refl q = Σ-≡ refl (ext (λ z → q z))


  mutual
    left0 : {n : ℕ} -> (c : UniR n) -> ⟦ forget c ⟧Uni Z -> ⟦ c ⟧UniR Z
    left0 ιR x = x
    left0 (δσR G H) ((x , a) , g)
      = (left0 G x ,
--         subst (λ z → proj₁ (H z)) (left1 G x) a , (λ p → g (subst (λ z → proj₂ (H (proj₁ z)) (proj₂ z)) (sym (Σ-≡ (left1 G x) refl)) p)))
         subst (λ z → cont (H z) (ind Z)) (left1 G x) (a , g))

    left1 : {n : ℕ} -> (c : UniR n) -> (x : ⟦ forget c ⟧Uni Z) ->
            forgetInfo c (⟦ forget c ⟧Info Z x) ≡ ⟦ c ⟧InfoR Z (left0 c x)
    left1 ιR x = refl
    left1 (δσR G A) ((x , a) , g) rewrite left1 G x = refl -- TODO: do this properly

  mutual
    right0 : {n : ℕ} -> (c : UniR n) -> ⟦ c ⟧UniR Z -> ⟦ forget c ⟧Uni Z
    right0 ιR x = x
    right0 (δσR G H) (x , a , g)
      = (right0 G x , subst (proj₁ ∘ H) (right1 G x) a) , (λ p → g (subst (λ z → proj₂ (H (proj₁ z)) (proj₂ z)) (sym (Σ-≡ (right1 G x) refl)) p))

    right1 : {n : ℕ} -> (c : UniR n) -> (x : ⟦ c ⟧UniR Z) ->
             ⟦ c ⟧InfoR Z x ≡ forgetInfo c (⟦ forget c ⟧Info Z (right0 c x))
    right1 ιR x = refl
    right1 (δσR G H) (x , a , g) rewrite right1 G x = refl -- TODO: do properly

  mutual
    leftright0 : {n : ℕ} -> (c : UniR n) -> (x : ⟦ c ⟧UniR Z) ->
                 x ≡ left0 c (right0 c x)
    leftright0 ιR x = refl
    leftright0 (δσR G H) (x , a , g)
     =  Σ-≡ (leftright0 G x)
            {!!}
{-
            (subst-cont
              (H ∘ ⟦ G ⟧InfoR Z)
              (leftright0 G x)
              p
              (λ z → snd-part z))
     where
       p = (trans
              (trans
                (subst-cong  {B = proj₁ ∘ H} (leftright0 G x))
                (trans
                  (congSubst (leftright1 G x))
                  (subst-trans (right1 G x) (left1 G (right0 G x)))))
              (subst-natural {P = proj₁ ∘ H} proj₁ (left1 G (right0 G x))))
       snd-part : ∀ z →
                  g (subst (λ z → proj₂ (H (⟦ G ⟧InfoR Z (proj₁ z))) (proj₂ z))
                           (sym (Σ-≡ (leftright0 G x) p)) z)
                    ≡ proj₂
                        (subst (λ z → (cont (H z) (ind Z)))
                               (left1 G (right0 G x))
                               (subst (proj₁ ∘ H) (right1 G x) a ,
                                (λ p → g (subst (λ z → proj₂ (H (proj₁ z)) (proj₂ z)) (sym (Σ-≡ (right1 G x) refl)) p)))) z
       snd-part z = {!(subst-proj₂ {C = λ z s → proj₂ (H z) s -> ind Z} (left1 G (right0 G x))))!}
-}

    leftright1 : {n : ℕ} -> (c : UniR n) -> (x : ⟦ c ⟧UniR Z) ->
                   cong (⟦ c ⟧InfoR Z)
                        (leftright0 c x)
                      ≡ trans (right1 c x) (left1 c (right0 c x))
    leftright1 ιR x = refl
    leftright1 (δσR G H) (x , a , g) = UIP _ _ -- TODO as usual



  mutual
    rightleft0 : {n : ℕ} -> (c : UniR n) -> (x : ⟦ forget c ⟧Uni Z) ->
                 x ≡ right0 c (left0 c x)
    rightleft0 ιR x = refl
    rightleft0 (δσR G H) ((x , a) , g)
     = Σ-≡ (Σ-≡ (rightleft0 G x)
                (trans
                  (subst-cong {B = proj₁ ∘ H} (rightleft0 G x))
                  (trans
                    (congSubst (rightleft1 G x))
                    (trans
                      (subst-trans (left1 G x) (right1 G (left0 G x)))
                      (cong (subst (proj₁ ∘ H) (right1 G (left0 G x)))
                            (subst-natural proj₁ (left1 G x)))))))
                {!!}
-- (trans (subst-dom (Σ-≡ (rightleft0 G x)       (trans (subst-cong (rightleft0 G x))        (trans (congSubst (rightleft1 G x))         (trans (subst-trans (left1 G x) (right1 G (left0 G x)))          (cong (subst (proj₁ ∘ H) (right1 G (left0 G x)))           (subst-natural proj₁ (left1 G x)))))))) (ext (λ a → {!congd proj₂!})))

    rightleft1 : {n : ℕ} -> (c : UniR n) -> (x : ⟦ forget c ⟧Uni Z) ->
                   cong (forgetInfo c ∘ (⟦ forget c ⟧Info Z))
                        (rightleft0 c x)
                      ≡ trans (left1 c x) (right1 c (left0 c x))
    rightleft1 ιR x = refl
    rightleft1 (δσR G H) ((x , a) , g) = UIP _ _



forgetEq :
  ∀ {E}{n} -> (R : UFR E n) -> {Z : Fam D} ->
 ⟦ forgetUFR R ⟧ Z ≃ ⟦ R ⟧R Z
left (forgetEq (c , α))  = (ForgetEq.left0 c , cong α ∘ ForgetEq.left1 c)
right (forgetEq (c , α)) = (ForgetEq.right0 c , cong α ∘ ForgetEq.right1 c)
leftright (forgetEq R@(c , α) {Z})
 = comp-is-id-ext
    (left (forgetEq R))
    (right (forgetEq R))
    (ForgetEq.leftright0 c)
    (λ x → trans
            (trans-cong
              (ForgetEq.right1 c x)
              (ForgetEq.left1 c (ForgetEq.right0 c x)))
            (trans
              (cong (cong α) (sym (ForgetEq.leftright1 c x)))
              (sym (cong-cong {f = α} {g = ⟦ c ⟧InfoR Z} (ForgetEq.leftright0 c x)))))
rightleft (forgetEq R@(c , α) {Z})
 = comp-is-id-ext
    (right (forgetEq R))
    (left (forgetEq R))
    (ForgetEq.rightleft0 c)
    (λ x → trans
            (trans-cong
              (ForgetEq.left1 c x)
              (ForgetEq.right1 c (ForgetEq.left0 c x)))
            (trans
              (cong (cong α) (sym (ForgetEq.rightleft1 c x)))
              (sym (cong-cong {f = α} {g = forgetInfo c ∘ (⟦ forget c ⟧Info Z)} (ForgetEq.rightleft0 c x)))))



-- padding equivalence

module PadEq {Z : Fam D} where

  left0 : ∀ {n} m (c : UniR n) -> ⟦ c ⟧UniR Z -> ⟦ pad m c ⟧UniR Z
  left0 {n} zero c x rewrite +-right-identity n = x , _ , ⊥-elim
  left0 {n} (suc m) c x rewrite +-suc n m = left0 m c x , _ , ⊥-elim

  left1 : ∀ {n} m (c : UniR n) -> (x : ⟦ c ⟧UniR Z) ->
          ⟦ c ⟧InfoR Z x ≡ padInfo m c (⟦ pad m c ⟧InfoR Z (left0 m c x))
  left1 {n} zero c x rewrite +-right-identity n = refl
  left1 {n} (suc m) c x rewrite +-suc n m = left1 m c x

  right0 : ∀ {n} m (c : UniR n) -> ⟦ pad m c ⟧UniR Z -> ⟦ c ⟧UniR Z
  right0 {n} zero c x rewrite +-right-identity n = proj₁ x
  right0 {n} (suc m) c x rewrite +-suc n m = right0 m c (proj₁ x)

  right1 : ∀ {n} m (c : UniR n) -> (x : ⟦ pad m c ⟧UniR Z) ->
             padInfo m c (⟦ pad m c ⟧InfoR Z x) ≡ ⟦ c ⟧InfoR Z (right0 m c x)
  right1 {n} zero c x rewrite +-right-identity n = refl
  right1 {n} (suc m) c x rewrite +-suc n m = right1 m c (proj₁ x)

  leftright0 : ∀ {n} m (c : UniR n) -> (x : ⟦ pad m c ⟧UniR Z) ->
               x ≡ left0 m c (right0 m c x)
  leftright0 {n} zero c x rewrite +-right-identity n
    = Σ-≡ refl (Σ-≡ refl (ext (λ ())))
  leftright0 {n} (suc m) c x rewrite +-suc n m
    = Σ-≡ (leftright0 m c (proj₁ x)) (Σ-≡ refl (ext (λ ())))

  rightleft0 : ∀ {n} m (c : UniR n) -> (x : ⟦ c ⟧UniR Z) ->
               x ≡ right0 m c (left0 m c x)
  rightleft0 {n} zero c x rewrite +-right-identity n = refl
  rightleft0 {n} (suc m) c x rewrite +-suc n m = rightleft0 m c x

padEq :
  ∀ {E}{n} m -> (R : UFR E n) -> {Z : Fam D} ->
  ⟦ R ⟧R Z ≃ ⟦ padUFR m R ⟧R Z
left (padEq m R@(c , α) {Z}) = (PadEq.left0 m c , cong α ∘ PadEq.left1 m c)
right (padEq m R@(c , α) {Z}) = (PadEq.right0 m c , cong α ∘ PadEq.right1 m c)
leftright (padEq m R@(c , α) {Z})
   = comp-is-id
      (left (padEq m R {Z}))
      (right (padEq m R {Z}))
      (ext (PadEq.leftright0 m c))
      (λ y → UIP _ _) -- TODO
rightleft (padEq m R@(c , α) {Z})
   = comp-is-id
      (right (padEq m R {Z}))
      (left (padEq m R {Z}))
      (ext (PadEq.rightleft0 m c))
      (λ y → UIP _ _) -- TODO



-- padEqual interaction with coproducts equivalence

module PadEqualEq {Z : Fam D} where

  left0 : ∀ {n m} -> (c : UniR n)(d : UniR m) ->
          let (_ , c' , d') = padEqual c d in
          ⟦ c' ⟧UniR Z ⊎ ⟦ d' ⟧UniR Z -> ⟦ c ⟧UniR Z ⊎ ⟦ d ⟧UniR Z
  left0 {m} {n} c d with compare n m
  ... | less .n k    = ⊎-map id (PadEq.right0 k d)
  ... | equal .m     = id
  ... | greater .m k = ⊎-map (PadEq.right0 k c) id

  left1 : ∀ {n m} -> (c : UniR n)(d : UniR m) ->
          let (_ , c' , d') = padEqual c d in
          (x : ⟦ c'  ⟧UniR Z ⊎ ⟦ d'  ⟧UniR Z) ->
          ⊎-map (padEqualInfo₁ c d ∘ ⟦ c' ⟧InfoR Z)
                (padEqualInfo₂ c d ∘ ⟦ d' ⟧InfoR Z) x
             ≡ (⊎-map (⟦ c ⟧InfoR Z) (⟦ d ⟧InfoR Z) (left0 c d x))
  left1 {m} {n} c d x with compare n m
  left1 c d (inj₁ x) | less n k = refl
  left1 c d (inj₂ x) | less n k = cong inj₂ (PadEq.right1 k d x)
  left1 c d x | equal m = refl
  left1 c d (inj₁ x) | greater m k = cong inj₁ (PadEq.right1 k c x)
  left1 c d (inj₂ x) | greater m k = refl

  right0 : ∀ {n m} -> (c : UniR n)(d : UniR m) ->
           let (_ , c' , d') = padEqual c d in
           ⟦ c ⟧UniR Z ⊎ ⟦ d ⟧UniR Z -> ⟦ c' ⟧UniR Z ⊎ ⟦ d' ⟧UniR Z
  right0 {m} {n} c d with compare n m
  ... | less .n k    = ⊎-map id (PadEq.left0 k d)
  ... | equal .m     = id
  ... | greater .m k = ⊎-map (PadEq.left0 k c) id

  right1 : ∀ {n m} -> (c : UniR n)(d : UniR m) ->
          let (_ , c' , d') = padEqual c d in
          (x : ⟦ c ⟧UniR Z ⊎ ⟦ d ⟧UniR Z) ->
          ⊎-map (⟦ c ⟧InfoR Z) (⟦ d ⟧InfoR Z) x
            ≡ ⊎-map (padEqualInfo₁ c d ∘ ⟦ c' ⟧InfoR Z)
                    (padEqualInfo₂ c d ∘ ⟦ d' ⟧InfoR Z) (right0 c d x)
  right1 {m} {n} c d x with compare n m
  right1 c d (inj₁ x) | less n k = refl
  right1 c d (inj₂ x) | less n k = cong inj₂ (PadEq.left1 k d x)
  right1 c d x | equal m = refl
  right1 c d (inj₁ x) | greater m k = cong inj₁ (PadEq.left1 k c x)
  right1 c d (inj₂ x) | greater m k = refl

  leftright0 : ∀ {n m} -> (c : UniR n)(d : UniR m) ->
               let (_ , c' , d') = padEqual c d in
               (x : ⟦ c ⟧UniR Z ⊎ ⟦ d ⟧UniR Z) ->
               x ≡ left0 c d (right0 c d x)
  leftright0 {m} {n} c d x with compare n m
  leftright0 c d (inj₁ x) | less n k = refl
  leftright0 c d (inj₂ x) | less n k = cong inj₂ (PadEq.rightleft0 k d x)
  leftright0 c d x | equal m = refl
  leftright0 c d (inj₁ x) | greater m k = cong inj₁ (PadEq.rightleft0 k c x)
  leftright0 c d (inj₂ x) | greater m k = refl


  rightleft0 : ∀ {n m} -> (c : UniR n)(d : UniR m) ->
               let (_ , c' , d') = padEqual c d in
               (x : ⟦ c'  ⟧UniR Z ⊎ ⟦ d' ⟧UniR Z) ->
               x ≡ right0 c d (left0 c d x)
  rightleft0 {m} {n} c d x with compare n m
  rightleft0 c d (inj₁ x) | less n k = refl
  rightleft0 c d (inj₂ x) | less n k = cong inj₂ (PadEq.leftright0 k d x)
  rightleft0 c d x | equal m = refl
  rightleft0 c d (inj₁ x) | greater m k = cong inj₁ (PadEq.leftright0 k c x)
  rightleft0 c d (inj₂ x) | greater m k = refl


map-fuse : ∀ {a b c d e} →
           {A  : Set a}{B : Set b}{C : Set c}{D : Set d}{E : Set e}
           {f : A -> C}{g : B -> D}(f' : C -> E)(g' : D -> E) ->
           (x : A ⊎ B) ->
           [ (f' ∘ f) , g' ∘ g ]′ x ≡ [ f' , g' ] (⊎-map f g x)
map-fuse f' g' (inj₁ x) = refl
map-fuse f' g' (inj₂ y) = refl

padEqualEq :
  ∀ {E}{n m} -> (R : UFR E n)(R' : UFR E m) -> {Z : Fam D} ->
  (⟦ pe₁ R R' ⟧R Z Fam+ ⟦ pe₂ R R' ⟧R Z) ≃ (⟦ R ⟧R Z Fam+ ⟦ R' ⟧R Z)
left (padEqualEq R@(c , α) R'@(c' , α') {Z})
  = PadEqualEq.left0 c c' ,
    (λ x → trans (map-fuse α α' x)
                 (trans (cong [ α , α' ] (PadEqualEq.left1 c c' x))
                        (sym (map-fuse α α' (PadEqualEq.left0 c c' x)))))
right (padEqualEq R@(c , α) R'@(c' , α') {Z})
  = PadEqualEq.right0 c c' ,
    (λ x → trans (map-fuse α α' x)
                 (trans (cong [ α , α' ] (PadEqualEq.right1 c c' x))
                        (sym (map-fuse α α' (PadEqualEq.right0 c c' x)))))
leftright (padEqualEq R@(c , α) R'@(c' , α') {Z})
   = comp-is-id
      (left (padEqualEq R R' {Z}))
      (right (padEqualEq R R' {Z}))
      (ext (PadEqualEq.leftright0 c c'))
      (λ y → UIP _ _) -- TODO
rightleft (padEqualEq R@(c , α) R'@(c' , α') {Z})
   = comp-is-id
      (right (padEqualEq R R' {Z}))
      (left (padEqualEq R R' {Z}))
      (ext (PadEqualEq.rightleft0 c c'))
      (λ y → UIP _ _) -- TODO




-- choice equivalence

module ChoiceEq {Z : Fam D} where

  mutual

    left0 : {n : ℕ} -> (c c' : UniR n) ->
            ⟦ choice c c' ⟧UniR Z -> ⟦ c ⟧UniR Z ⊎ ⟦ c' ⟧UniR Z
    left0 ιR ιR (_ , true , _) = inj₁ tt
    left0 ιR ιR (_ , false , _) = inj₂ tt
    left0 (δσR c A) (δσR c' A') (x , a)
     with left0 c c' x | choiceInfo c c' (⟦ choice c c' ⟧InfoR Z x) | left1 c c' x
    ... | inj₁ y | inj₁ γ | refl = inj₁ (y , a)
    ... | inj₁ y | inj₂ γ | ()
    ... | inj₂ y | inj₁ γ | ()
    ... | inj₂ y | inj₂ γ | refl = inj₂ (y , a)

    left1 : {n : ℕ} -> (c c' : UniR n) ->
            (x : ⟦ choice c c' ⟧UniR Z) ->
            (choiceInfo c c' (⟦ choice c c' ⟧InfoR Z x))
              ≡ ⊎-map (⟦ c ⟧InfoR Z) (⟦ c' ⟧InfoR Z) (left0 c c' x)
    left1 ιR ιR (_ , true , _) = refl
    left1 ιR ιR (_ , false , _) = refl
    left1 (δσR c A) (δσR c' A') (x , a)
     with left0 c c' x | choiceInfo c c' (⟦ choice c c' ⟧InfoR Z x) | left1 c c' x
    ... | inj₁ y | inj₁ γ | refl = refl
    ... | inj₁ y | inj₂ γ | ()
    ... | inj₂ y | inj₁ γ | ()
    ... | inj₂ y | inj₂ γ | refl = refl

    right0 : {n : ℕ} -> (c c' : UniR n) ->
            ⟦ c ⟧UniR Z ⊎ ⟦ c' ⟧UniR Z -> ⟦ choice c c' ⟧UniR Z
    right0 ιR ιR (inj₁ tt) = (_ , true , ⊥-elim)
    right0 ιR ιR (inj₂ tt) = (_ , false , ⊥-elim)
    right0 (δσR c A) (δσR c' A') (inj₁ (x , a))
     = right0 c c' (inj₁ x) , subst (λ z → cont ([ A , A' ]′ z) (ind Z)) (right1 c c' (inj₁ x)) a
    right0 (δσR c A) (δσR c' A') (inj₂ (x , a))
     = right0 c c' (inj₂ x) , subst (λ z → cont ([ A , A' ]′ z) (ind Z)) (right1 c c' (inj₂ x)) a

    right1 : {n : ℕ} -> (c c' : UniR n) ->
             (x : ⟦ c ⟧UniR Z ⊎ ⟦ c' ⟧UniR Z) ->
             ⊎-map (⟦ c ⟧InfoR Z) (⟦ c' ⟧InfoR Z) x
               ≡ choiceInfo c c' (⟦ choice c c' ⟧InfoR Z (right0 c c' x))
    right1 ιR ιR (inj₁ tt) = refl
    right1 ιR ιR (inj₂ tt) = refl
    right1 (δσR c A) (δσR c' A') (inj₁ (x , a))
      with choiceInfo c c' (⟦ choice c c' ⟧InfoR Z (right0 c c' (inj₁ x))) | right1 c c' (inj₁ x)
    ... | inj₁ q | refl = refl
    ... | inj₂ q | ()
    right1 (δσR c A) (δσR c' A') (inj₂ (x , a))
      with choiceInfo c c' (⟦ choice c c' ⟧InfoR Z (right0 c c' (inj₂ x))) | right1 c c' (inj₂ x)
    ... | inj₁ q | ()
    ... | inj₂ q | refl = refl

    leftright0 : {n : ℕ} -> (c c' : UniR n) ->
                 (x : ⟦ c ⟧UniR Z ⊎ ⟦ c' ⟧UniR Z) ->
                 x ≡ left0 c c' (right0 c c' x)
    leftright0 ιR ιR (inj₁ tt) = refl
    leftright0 ιR ιR (inj₂ tt) = refl
    leftright0 (δσR c A) (δσR c' A') (inj₁ (x , a))
     = {!!}
    leftright0 (δσR c A) (δσR c' A') (inj₂ (x , a))
     = {!!}


    rightleft0 : {n : ℕ} -> (c c' : UniR n) ->
                 (x : ⟦ choice c c' ⟧UniR Z) ->
                 x ≡ right0 c c' (left0 c c' x)
    rightleft0 ιR ιR (_ , true , _) = Σ-≡ refl (Σ-≡ refl (ext (λ ())))
    rightleft0 ιR ιR (_ , false , _) = Σ-≡ refl (Σ-≡ refl (ext (λ ())))
    rightleft0 (δσR c A) (δσR c' A') (x , a) = {!!}

choiceEq :
  ∀ {E}{n} -> (R R' : UFR E n) -> {Z : Fam D} ->
  ⟦ choiceUFR R R' ⟧R Z ≃ (⟦ R ⟧R Z Fam+ ⟦ R' ⟧R Z)
left (choiceEq R@(c , α) R'@(c' , α') {Z})
 = ChoiceEq.left0 c c' ,
    (λ x → (trans (cong [ α , α' ] (ChoiceEq.left1 c c' x))
                  (sym (map-fuse α α' (ChoiceEq.left0 c c' x)))))
right (choiceEq R@(c , α) R'@(c' , α') {Z})
 = ChoiceEq.right0 c c' ,
    (λ x → trans (map-fuse α α' x)
                 (cong [ α , α' ] (ChoiceEq.right1 c c' x)))
leftright (choiceEq R@(c , α) R'@(c' , α') {Z})
   = comp-is-id
      (left (choiceEq R R' {Z}))
      (right (choiceEq R R' {Z}))
      (ext (ChoiceEq.leftright0 c c'))
      (λ y → UIP _ _) -- TODO
rightleft (choiceEq R@(c , α) R'@(c' , α') {Z})
   = comp-is-id
      (right (choiceEq R R' {Z}))
      (left (choiceEq R R' {Z}))
      (ext (ChoiceEq.rightleft0 c c'))
      (λ y → UIP _ _) -- TODO


-- Finally:

coprodEq : ∀ {E} -> (R R' : UF D E) -> {Z : Fam D} ->
           ⟦ R UF-+ R' ⟧ Z ≃ (⟦ R ⟧ Z Fam+ ⟦ R' ⟧ Z)
coprodEq R@(c , α) R'@(d , β) =
  let (n , c' , d') = padEqual (containerise c) (containerise d)
  in transEq
       (transEq
         (transEq
           (forgetEq (choiceUFR (pe₁ (containeriseUF R)
                                     (containeriseUF R'))
                                (pe₂ (containeriseUF R)
                                     (containeriseUF R'))))
           (choiceEq (pe₁ (containeriseUF R) (containeriseUF R'))
                     (pe₂ (containeriseUF R) (containeriseUF R'))))
         (padEqualEq (containeriseUF R) (containeriseUF R')))
       (+-≃ (containeriseEq R) (containeriseEq R'))