module Uniform.AppLift.Maps where

open import Prelude.Basic

open import Prelude.Equality
open import Prelude.Fam

open import Uniform.IR

mutual
  _++[_⟶_] : {D : Set1} ->
              (c : Uni D) -> (E : Info c -> Set) -> (d : Uni D) -> Uni D
  c ++[ E ⟶ ι ] = c
  c ++[ E ⟶ σ d A ]
    = σ (c ++[ E ⟶ d ]) (λ γ → (e : E (fst d γ)) -> A (snd d γ e))
  c ++[ E ⟶ δ d A ]
    = δ (c ++[ E ⟶ d ]) (λ γ → Σ[ e ∈ E (fst d γ) ] A (snd d γ e))

  fst : {D : Set1}->
        {c : Uni D}{E : Info c -> Set}(d : Uni D) ->
        Info (c ++[ E ⟶ d ]) -> Info c
  fst d γ = proj₁ (both d γ)

  snd : {D : Set1}->
        {c : Uni D}{E : Info c -> Set}(d : Uni D) ->
        (γ : Info (c ++[ E ⟶ d ])) -> E (fst d γ) -> Info d
  snd d γ = proj₂ (both d γ)

  both : {D : Set1}->
       {c : Uni D}{E : Info c -> Set}(d : Uni D) ->
       (γ : Info (c ++[ E ⟶ d ])) -> Σ[ x ∈ Info c ] (E x -> Info d)
  both ι x = x , (λ _ → lift tt)
  both (σ d A) (x , g) = fst d x , (λ e → snd d x e , g e)
  both (δ d A) (x , g) = fst d x , (λ e → snd d x e , (λ a → g (e , a)))

-- in particular powers by a set

_⟶_ : {D E : Set1} -> (A : Set) -> (d : UF D E) -> UF D (A → E)
A ⟶ (d , α) = (ι ++[ (λ _ → A) ⟶ d ] , (λ γ → α ∘ (snd d γ)))


mutual

  rightFst0 : ∀ {D c E} d → {Z : Fam D} ->
                    ⟦ (c ++[ E ⟶ d ]) ⟧Uni Z -> ⟦ c ⟧Uni Z
  rightFst0 ι x = x
  rightFst0 (σ d A) (x , g) = rightFst0 d x
  rightFst0 (δ d A) (x , g) = rightFst0 d x

  rightSnd0 : ∀ {D c E} d → {Z : Fam D} ->
              (x : ⟦ (c ++[ E ⟶ d ]) ⟧Uni Z) ->
              (e : E (⟦ c ⟧Info Z (rightFst0 d x))) -> ⟦ d ⟧Uni Z
  rightSnd0 ι x  e = _
  rightSnd0 {E = E} (σ d A) (x , g) e
    = (rightSnd0 d x e ,
       subst A (rightSnd1 d x e) (g (subst E (sym (rightFst1 d x)) e)))
  rightSnd0 {E = E} (δ d A) {U , T} (x , g) e
    = (rightSnd0 d x e ,
       (λ a → g (subst E (sym (rightFst1 d x)) e ,
                  subst A (sym (rightSnd1 d x e)) a)))

  rightFst1 : ∀ {D c E} d → {Z : Fam D} ->
              (x : ⟦ (c ++[ E ⟶ d ]) ⟧Uni Z) ->
              fst d (⟦ (c ++[ E ⟶ d ]) ⟧Info Z x) ≡ ⟦ c ⟧Info Z (rightFst0 d x)
  rightFst1 ι x = refl
  rightFst1 (σ d A) (x , g) = rightFst1 d x
  rightFst1 (δ d A) (x , g) = rightFst1 d x

  rightSnd1 : ∀ {D c E} d → {Z : Fam D} ->
              (x : ⟦ (c ++[ E ⟶ d ]) ⟧Uni Z) ->
              (e : E (⟦ c ⟧Info Z (rightFst0 d x))) ->
              snd d (⟦ (c ++[ E ⟶ d ]) ⟧Info Z x)
                    (subst E (sym (rightFst1 d x)) e)
                                                ≡ ⟦ d ⟧Info Z (rightSnd0 d x e)
  rightSnd1 ι x e = refl
  rightSnd1 (σ d A) (x , g) e = Σ-≡ (rightSnd1 d x e) refl
  rightSnd1 (δ d A) (x , g) e = Σ-≡ (rightSnd1 d x e)
                                        (subst-dom (rightSnd1 d x e))

-----------------------------------------------------
right0 : ∀ {D c E} d → {Z : Fam D} ->
        (y : ⟦ (c ++[ E ⟶ d ]) ⟧Uni Z) ->
        Σ[ x ∈ ⟦ c ⟧Uni Z ] ((e : E (⟦ c ⟧Info Z x)) -> ⟦ d ⟧Uni Z)
right0 d y = (rightFst0 d y , rightSnd0 d y)

right1 : ∀ {D c E} d → {Z : Fam D} ->
         (x : ⟦ (c ++[ E ⟶ d ]) ⟧Uni Z) ->
         both d (⟦ (c ++[ E ⟶ d ]) ⟧Info Z x)
                ≡ map (⟦ c ⟧Info Z) (λ g → (⟦ d ⟧Info Z) ∘ g) (right0 d x)
right1 {E = E} d x = Σ-≡ (rightFst1 d x)
                         (trans (subst-dom {A' = E} (rightFst1 d x))
                                (ext (rightSnd1 d x)))
------------------------------------------------------

mutual

  left0 : ∀ {D c E} d → {Z : Fam D} ->
          Σ[ x ∈ ⟦ c ⟧Uni Z ] ((e : E (⟦ c ⟧Info Z x)) -> ⟦ d ⟧Uni Z) ->
          ⟦ (c ++[ E ⟶ d ]) ⟧Uni Z
  left0 ι (x , _) = x
  left0 {E = E} (σ d A) (x , g) =
    (left0 d (x , proj₁ ∘ g) ,
     (λ e → subst A (leftSnd1 d x (proj₁ ∘ g) e)
                     (proj₂ (g (subst E (sym (leftFst1 d x (proj₁ ∘ g))) e)))))
  left0 {E = E} (δ d A) (x , g) =
    (left0 d (x , proj₁ ∘ g) ,
     (λ { (e , a)→ proj₂ (g (subst E (sym (leftFst1 d x (proj₁ ∘ g))) e))
                            (subst A (sym (leftSnd1 d x (proj₁ ∘ g) e)) a)}))

  leftFst1 : ∀ {D c E} d → {Z : Fam D} ->
             (x : ⟦ c ⟧Uni Z)(g : (e : E (⟦ c ⟧Info Z x)) -> ⟦ d ⟧Uni Z)  ->
             ⟦ c ⟧Info Z x ≡ fst d (⟦ (c ++[ E ⟶ d ]) ⟧Info Z (left0 d ((x , g))))
  leftFst1 ι x g = refl
  leftFst1 (σ d A) x g = leftFst1 d x (proj₁ ∘ g)
  leftFst1 (δ d A) x g = leftFst1 d x (proj₁ ∘ g)

  leftSnd1 : ∀ {D c E} d → {Z : Fam D} ->
             (x : ⟦ c ⟧Uni Z)(g : (e : E (⟦ c ⟧Info Z x)) -> ⟦ d ⟧Uni Z)  ->
             (e : E _) ->
             ⟦ d ⟧Info Z (g (subst E (sym (leftFst1 d x g)) e))
                     ≡ snd d (⟦ (c ++[ E ⟶ d ]) ⟧Info Z (left0 d ((x , g)))) e
  leftSnd1 ι x g e = refl
  leftSnd1 (σ d A) x g e
    = Σ-≡ (leftSnd1 d x (proj₁ ∘ g) e) refl
  leftSnd1 {E = E} (δ d A) {Z = Z} x g e
    = Σ-≡ (leftSnd1 d x (proj₁ ∘ g) e)
          (trans (subst-dom (leftSnd1 d x (proj₁ ∘ g) e)) refl)

left1 : ∀ {D c E} d → {Z : Fam D} ->
        (x : ⟦ c ⟧Uni Z)(g : (e : E (⟦ c ⟧Info Z x)) -> ⟦ d ⟧Uni Z)  ->
        (⟦ c ⟧Info Z x , ⟦ d ⟧Info Z ∘ g)
            ≡ both d (⟦ (c ++[ E ⟶ d ]) ⟧Info Z (left0 d (x , g)))
left1 {c = c} {E} d {Z} x g
   = Σ-≡ (leftFst1 {c = c} d x g)
         (trans (subst-dom {A' = E} (leftFst1 {c = c} d x g))
                (ext (leftSnd1 d x g)))