```module Polynomial.EmbeddingFromDS where

open import Prelude.Basic
open import Prelude.Equality
open import Prelude.Fam
open import Prelude.Equivalences

open import Polynomial.IR
open import DS.IR renaming (⟦_⟧ to ⟦_⟧DS; ⟦_⟧₀ to ⟦_⟧DS₀; ⟦_⟧₁ to ⟦_⟧DS₁)

-- Embedding Dybjer-Setzer into Polynomial

DStoPoly : {D E : Set1} -> DS D E -> Poly D
DStoPoly (ι e) = con ⊤
DStoPoly (σ A f) = sigma (con A) (λ a → DStoPoly (f (lower a)))
DStoPoly (δ A F) = sigma (pi A (λ _ → idPN)) (λ g → DStoPoly (F g))

DStoInfoMap : {D E : Set1} -> (c : DS D E) -> Info (DStoPoly c) -> E
DStoInfoMap (ι e) _ = e
DStoInfoMap (σ A f) (a , x) = DStoInfoMap (f (lower a)) x
DStoInfoMap (δ A F) (g , x) = DStoInfoMap (F g) x

DStoPolyIR : {D E : Set1} -> DS D E -> IR D E
DStoPolyIR c = DStoPoly c , DStoInfoMap c

-- maps back and forth

-- right
right0 : {D E : Set1} -> (c : DS D E) -> {Z : Fam D} ->
Node (DStoPoly c) Z -> ⟦ c ⟧DS₀ Z
right0 (ι e)   = id
right0 (σ A f) = map id (right0 (f _))
right0 (δ A F) = map id (right0 (F _))

right1 : {D E : Set1} -> (c : DS D E) -> {Z : Fam D} ->
(x : ⟦ DStoPolyIR c ⟧₀ Z) ->
⟦ DStoPolyIR c ⟧₁ Z x ≡ ⟦ c ⟧DS₁ Z (right0 c x)
right1 (ι e)   _       = refl
right1 (σ A f) (a , x) = right1 (f a) x
right1 (δ A F) (g , x) = right1 (F _) x

-- left
left0 : {D E : Set1} -> (c : DS D E) -> {Z : Fam D} ->
⟦ c ⟧DS₀ Z -> Node (DStoPoly c) Z
left0 (ι e)   = id
left0 (σ A f) = map id (left0 (f _))
left0 (δ A F) = map id (left0 (F _))

left1 : {D E : Set1} -> (c : DS D E) -> {Z : Fam D} ->
(x : ⟦ c ⟧DS₀ Z) ->
⟦ c ⟧DS₁ Z x ≡ ⟦ DStoPolyIR c ⟧₁ Z (left0 c x)
left1 (ι e)   _       = refl
left1 (σ A f) (a , x) = left1 (f a) x
left1 (δ A F) (g , x) = left1 (F _) x

leftright0 : {D E : Set1} -> (c : DS D E) -> {Z : Fam D} ->
(x : Node (DStoPoly c) Z) -> x ≡ left0 c (right0 c x)
leftright0 (ι e) x = refl
leftright0 (σ A f) (a , x) = cong (λ z → a , z) (leftright0 (f a) x)
leftright0 (δ A F) (g , x) = cong (λ z → g , z) (leftright0 (F _) x)

rightleft0 : {D E : Set1} -> (c : DS D E) -> {Z : Fam D} ->
(x : ⟦ c ⟧DS₀ Z) -> x ≡ right0 c (left0 c x)
rightleft0 (ι e) x = refl
rightleft0 (σ A f) (a , x) = cong (λ z → a , z) (rightleft0 (f a) x)
rightleft0 (δ A F) (g , x) = cong (λ z → g , z) (rightleft0 (F _) x)

embedEquiv : {D E : Set1} -> (c : DS D E) -> {Z : Fam D} ->
⟦ c ⟧DS Z ≃ ⟦ DStoPolyIR c ⟧ Z
embedEquiv c = record { left = left0 c , left1 c
; right = right0 c , right1 c
; leftright = comp-is-id-ext (left0 c , left1 c)
(right0 c , right1 c)
(leftright0 c)
(λ y → UIP _ _) -- TODO
; rightleft = comp-is-id-ext (right0 c , right1 c)
(left0 c , left1 c)
(rightleft0 c)
(λ y → UIP _ _) -- TODO
}

{----- Naturality -------------------------------}

-- the translation is also natural in E
naturality0 : {D E E' : Set1} -> (h : E -> E') ->
(c : DS D E) -> DStoPoly (DS-map h c) ≡ DStoPoly c
naturality0 h (ι e) = refl
naturality0 h (σ A f) = cong (sigma (con A))
(ext (λ a → naturality0 h (f (lower a))))
naturality0 h (δ A F) = cong (sigma (pi A (λ _ → idPN)))
(ext (λ g → naturality0 h (F g)))

naturality1 : {D E E' : Set1} -> (h : E -> E') -> (c : DS D E) ->
(x : Info (DStoPoly (DS-map h c))) ->
DStoInfoMap (DS-map h c) x
≡ h (DStoInfoMap c (subst Info (naturality0 h c) x))
naturality1 h (ι e) x = refl
naturality1 h (σ A f) (a , x)
= let p = naturality0 h ∘ f ∘ lower
lemma : (a , subst Info (p a) x)
≡ subst Info (cong (sigma (con A)) (ext p)) (a , x)
lemma = trans
(trans
(cong (_,_ a)
(trans
(sym (congSubst (ext-β p a)))
(sym (subst-cong {B = Info} (ext p)))))
(sym (subst-Σ-const-first (ext p))))
(subst-cong (ext p))
in
trans (naturality1 h (f (lower a)) x)
(cong (λ z → h (DStoInfoMap (f (lower (proj₁ z))) (proj₂ z)))
lemma)
naturality1 h (δ A F) (g , x)
= let p = naturality0 h ∘ F
lemma : (g , subst Info (p g) x)
≡ subst Info (cong (sigma (pi A (λ _ → idPN))) (ext p)) (g , x)
lemma = trans
(trans
(cong (_,_ g)
(trans
(sym (congSubst (ext-β p g)))
(sym (subst-cong {B = Info} (ext p)))))
(sym (subst-Σ-const-first (ext p))))
(subst-cong (ext p))
in
trans (naturality1 h (F g) x)
(cong (λ z → h (DStoInfoMap (F (proj₁ z)) (proj₂ z))) lemma)

naturality : {D E E' : Set1} -> (h : E -> E') ->
(c : DS D E) ->
DStoPolyIR (DS-map h c) ≡ IR-map h (DStoPolyIR c)
naturality h c
= Σ-≡ (naturality0 h c)
(trans
(subst-dom (naturality0 h c))
(ext (λ x →
trans
(naturality1 h c (subst Info (sym (naturality0 h c)) x))
(cong (h ∘ DStoInfoMap c)
(subst-sym-subst (naturality0 h c))))))
```