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