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))))))