```module DS.Bind where

-- Proof that bind of DS decodes to bind of Fam

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

open import DS.IR

-- Maps left to right

leftFst0 : {D E E' : Set1} -> (c : DS D E) -> (g : E -> DS D E') ->
{Z : Fam D} ->
⟦ c DS->>= g ⟧₀ Z -> ⟦ c ⟧₀ Z
leftFst0 (ι e) g x = _
leftFst0 (σ A f) g (a , x) = a , leftFst0 (f a) g x
leftFst0 (δ A F) g (h , x) = h , leftFst0 (F _) g x

leftSnd0 : {D E E' : Set1} -> (c : DS D E) -> (g : E -> DS D E') ->
{Z : Fam D} ->
(x : ⟦ c DS->>= g ⟧₀ Z) -> ⟦ g (⟦ c ⟧₁ Z (leftFst0 c g x)) ⟧₀ Z
leftSnd0 (ι e) g x = x
leftSnd0 (σ A f) g (a , x) = leftSnd0 (f a) g x
leftSnd0 (δ A F) g (h , x) = leftSnd0 (F _) g x

left0 : {D E E' : Set1} -> (c : DS D E) -> (g : E -> DS D E') ->
{Z : Fam D} ->
⟦ c DS->>= g ⟧₀ Z -> Σ[ x ∈ (⟦ c ⟧₀ Z) ] ⟦ g (⟦ c ⟧₁ Z x) ⟧₀ Z
left0 c g = < leftFst0 c g , leftSnd0 c g >

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

-- Maps right to left

right0 : {D E E' : Set1} -> (c : DS D E) -> (g : E -> DS D E') ->
{Z : Fam D} ->
Σ[ x ∈ (⟦ c ⟧₀ Z) ] ⟦ g (⟦ c ⟧₁ Z x) ⟧₀ Z -> ⟦ c DS->>= g ⟧₀ Z
right0 (ι e) g (_ , y) = y
right0 (σ A f) g ((a , x) , y) = a , right0 (f a) g (x , y)
right0 (δ A F) g ((h , x) , y) = h , right0 (F _) g (x , y)

right1 : {D E E' : Set1} -> (c : DS D E) -> (g : E -> DS D E') ->
{Z : Fam D} -> (y : Σ[ x ∈ (⟦ c ⟧₀ Z) ] ⟦ g (⟦ c ⟧₁ Z x) ⟧₀ Z) ->
⟦ g (⟦ c ⟧₁ Z (proj₁ y)) ⟧₁ Z (proj₂ y)
≡ ⟦ c DS->>= g ⟧₁ Z (right0 c g y)
right1 (ι e) g y = refl
right1 (σ A f) g ((a , x) , y) = right1 (f a) g (x , y)
right1 (δ A F) g ((h , x) , y) = right1 (F _) g (x , y)

-- Roundtrips

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

leftrightSnd0 : {D E E' : Set1} -> (c : DS D E) -> (g : E -> DS D E') ->
{Z : Fam D} -> (x : ⟦ c ⟧₀ Z)(y : ⟦ g (⟦ c ⟧₁ Z x) ⟧₀ Z) ->
subst (λ z → ⟦ g (⟦ c ⟧₁ Z z) ⟧₀ Z) (leftrightFst0 c g x y) y
≡  (leftSnd0 c g (right0 c g (x , y)))
leftrightSnd0 (ι e) g x y = refl
leftrightSnd0 (σ A f) g {Z} (a , x) y
= trans (sym (subst-cong (leftrightFst0 (f a) g x y)))
(leftrightSnd0 (f a) g x y)
leftrightSnd0 (δ A F) g {Z} (h , x) y
= trans (sym (subst-cong (leftrightFst0 (F _) g x y)))
(leftrightSnd0 (F _) g x y)

leftright0 : {D E E' : Set1} -> (c : DS D E) -> (g : E -> DS D E') ->
{Z : Fam D} -> (w : Σ[ x ∈ (⟦ c ⟧₀ Z) ] ⟦ g (⟦ c ⟧₁ Z x) ⟧₀ Z) ->
w ≡ left0 c g (right0 c g w)
leftright0 c g (x , h) = Σ-≡ (leftrightFst0 c g x h) (leftrightSnd0 c g x h)

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

leftright1 : {D E E' : Set1} -> (c : DS D E) -> (g : E -> DS D E') ->
{Z : Fam D} -> (w : Σ[ x ∈ (⟦ c ⟧₀ Z) ] ⟦ g (⟦ c ⟧₁ Z x) ⟧₀ Z) ->
trans (right1 c g w) (left1 c g (right0 c g w))
≡ cong (λ z → ⟦ g (⟦ c ⟧₁ Z (proj₁ z)) ⟧₁ Z (proj₂ z)) (leftright0 c g w)
leftright1 (ι e) g y = refl
leftright1 (σ A f) g {Z} ((a , x) , y)
= trans
(leftright1 (f a) g (x , y))
(trans
(cong-cong (Σ-≡ (leftrightFst0 (f a) g x y) (leftrightSnd0 (f a) g x y)))
(cong (cong _) (Σ-≡-cong-sym (λ v → a , v) (leftrightFst0 (f a) g x y)
(leftrightSnd0 (f a) g x y))))
leftright1 (δ A F) g ((h , x) , y)
= trans
(leftright1 (F _) g (x , y))
(trans
((cong-cong (Σ-≡ (leftrightFst0 (F _) g x y) (leftrightSnd0 (F _) g x y))))
(cong (cong _) (Σ-≡-cong-sym (λ v → h , v) (leftrightFst0 (F _) g x y)
(leftrightSnd0 (F _) g x y))))

rightleft1 : {D E E' : Set1} -> (c : DS D E) -> (g : E -> DS D E') ->
{Z : Fam D} -> (w : ⟦ c DS->>= g ⟧₀ Z) ->
trans (left1 c g w) (right1 c g (left0 c g w))
≡ cong (⟦ c DS->>= g ⟧₁ Z) (rightleft0 c g w)
rightleft1 (ι e) g y = refl
rightleft1 (σ A f) g (a , x) = trans (rightleft1 (f a) g x)
(cong-cong (rightleft0 (f a) g x))
rightleft1 (δ A F) g (h , x) = trans (rightleft1 (F _) g x)
(cong-cong (rightleft0 (F _) g x))

-- Summing up:

DSBindEquiv : {D E E' : Set1} -> (c : DS D E) -> (g : E -> DS D E') ->
{Z : Fam D} ->
⟦ c DS->>= g ⟧ Z ≃ (⟦ c ⟧ Z Fam->>= (λ e → ⟦ g e ⟧ Z))
DSBindEquiv c g = record { left = (left0 c g , left1 c g)
; right = (right0 c g , right1 c g)
; leftright = comp-is-id-ext (left0 c g , left1 c g)
(right0 c g , right1 c g)
(leftright0 c g)
(leftright1 c g)
; rightleft = comp-is-id-ext (right0 c g , right1 c g)
(left0 c g , left1 c g)
(rightleft0 c g)
(rightleft1 c g) }
```