module Uniform.EmbeddingIntoDS where

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

open import Prelude.Equivalences

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

-- Embedding Uniform into Dybjer-Setzer

-- reversing the "list" using an accumulator
UFtoDS' : {D E : Set1} -> (c : Uni D) -> (Info c -> DS D E) -> DS D E
UFtoDS' ι F = F _
UFtoDS' (σ G A) F = UFtoDS' G (λ γ → σ (A γ) (λ a → F (γ , a)))
UFtoDS' (δ G A) F = UFtoDS' G (λ γ → δ (A γ) (λ h → F (γ , h)))

UFtoDS : {D E : Set1} -> (c : UF D E) -> DS D E
UFtoDS (c , α) = UFtoDS' c (ι ∘ α)

-- maps back and forth

-- right
right0 : {D E : Set1} -> (c : Uni D) -> (F : Info c -> DS D E) ->
         {Z : Fam D} -> (x : ⟦ c ⟧Uni Z) ->
         ⟦ F (⟦ c ⟧Info Z x) ⟧DS₀ Z -> (⟦ UFtoDS' c F ⟧DS₀ Z)
right0 ι F x y = y
right0 (σ G A) F (x , a) y = right0 G _ x (a , y)
right0 (δ G A) F (x , h) y = right0 G _ x (h , y)

right1 : {D E : Set1} -> (c : Uni D) -> (F : Info c -> DS D E) ->
           {Z : Fam D} ->
           (x : ⟦ c ⟧Uni Z) -> (y : ⟦ F (⟦ c ⟧Info Z x) ⟧DS₀ Z) ->
           ⟦ F (⟦ c ⟧Info Z x) ⟧DS₁ Z y ≡ ⟦ UFtoDS' c F ⟧DS₁ Z (right0 c F x y)
right1 ι F x y = refl
right1 (σ G A) F (x , a) y = right1 G _ x (a , y)
right1 (δ G A) F (x , h) y = right1 G _ x (h , y)


-- left
left0 : {D E : Set1} -> (c : Uni D) -> (F : Info c -> DS D E) ->
           {Z : Fam D} ->
           ⟦ UFtoDS' c F ⟧DS₀ Z -> Σ[ x ∈ (⟦ c ⟧Uni Z) ] (⟦ F (⟦ c ⟧Info Z x) ⟧DS₀ Z)
left0 ι F x = _ , x
left0 (σ G A) F x
  = let (x' , (a , y)) = left0 G _ x in (x' , a) , y
left0 (δ G A) F x
  = let (x' , (h , y)) = left0 G _ x in (x' , h) , y

left1 : {D E : Set1} -> (c : Uni D) -> (F : Info c -> DS D E) ->
           {Z : Fam D} ->
           (x : ⟦ UFtoDS' c F ⟧DS₀ Z) ->
           ⟦ UFtoDS' c F ⟧DS₁ Z x
             ≡ ⟦ F (⟦ c ⟧Info Z (proj₁ (left0 c F x))) ⟧DS₁ Z
                                                    (proj₂ (left0 c F x))
left1 ι F x = refl
left1 (σ G A) F x = left1 G _ x
left1 (δ G A) F x = left1 G _ x

-- they are inverses

leftright0 : {D E : Set1} -> (c : Uni D) -> (F : Info c -> DS D E) ->
               {Z : Fam D} ->
               (x : ⟦ c ⟧Uni Z) -> (y : ⟦ F (⟦ c ⟧Info Z x) ⟧DS₀ Z) ->
               (x , y) ≡ (left0 c F (right0 c F x y))
leftright0 ι F _ y = refl
leftright0 (σ G A) F (x , a) y
  = cong (λ z → (proj₁ z , proj₁ (proj₂ z)) , proj₂ (proj₂ z))
         (leftright0 G _ x (a , y))
leftright0 (δ G A) F (x , h) y
  = cong (λ z → (proj₁ z , proj₁ (proj₂ z)) , proj₂ (proj₂ z))
         (leftright0 G _ x (h , y))

rightleft0 : {D E : Set1} -> (c : Uni D) -> (F : Info c -> DS D E) ->
               {Z : Fam D} ->
               (x : ⟦ UFtoDS' c F ⟧DS₀ Z) ->
               x ≡ right0 c F (proj₁ (left0 c F x)) (proj₂ (left0 c F x))
rightleft0 ι F x = refl
rightleft0 (σ G A) F x = rightleft0 G _ x
rightleft0 (δ G A) F x = rightleft0 G _ x

embedEquiv : {D E : Set1} -> (R : UF D E) -> {Z : Fam D} ->
             ⟦ UFtoDS R ⟧DS Z ≃ ⟦ R ⟧ Z
embedEquiv R@(c , α)
  = record { left = proj₁ ∘ (left0 c (ι ∘ α)) , left1 c (ι ∘ α)
           ; right = (λ x → right0 c (ι ∘ α) x _) , λ x → right1 c (ι ∘ α) x _
           ; leftright = comp-is-id-ext
                           (proj₁ ∘ (left0 c (ι ∘ α)) , left1 c (ι ∘ α))
                           ((λ x → right0 c (ι ∘ α) x _) ,
                             λ x → right1 c (ι ∘ α) x _)
                           (λ x → cong proj₁ (leftright0 c (ι ∘ α) x _))
                           (λ y → UIP _ _) -- TODO for now
           ; rightleft = comp-is-id-ext
                           ((λ x → right0 c (ι ∘ α) x _) ,
                             λ x → right1 c (ι ∘ α) x _)
                           (proj₁ ∘ (left0 c (ι ∘ α)) , left1 c (ι ∘ α))
                           (rightleft0 c (ι ∘ α))
                           (λ y → UIP _ _) -- TODO for now
           }