```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
}
```