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