module Uniform.AppLift.Leftright where
open import Prelude.Basic
open import Prelude.Equality
open import Prelude.Fam
open import Uniform.IR
open import Uniform.AppLift.Maps
mutual
leftright0 : ∀ {D c}{E : Info c -> Set} d → {Z : Fam D} ->
(y : ⟦ (c ++[ E ⟶ d ]) ⟧Uni Z) ->
y ≡ left0 {D} {c} {E} d (right0 d y)
leftright0 {D} {c} {E} ι y = refl
leftright0 {D} {c} {E} (σ d A) {Z} (x , g)
= Σ-≡ (leftright0 d x)
(trans
(subst-domcod (leftright0 d x))
(ext (λ e →
trans
(subst-cong {B = A} (Σ-≡ (leftright0 d x)
(subst-sym-subst (leftright0 d x))))
(trans
(trans
(congSubst (leftrightSnd1 d x e))
(trans
(subst-trans (cong (snd d (⟦ c ++[ E ⟶ d ] ⟧Info Z x))
(trans
(subst-cong (sym (leftright0 d x)))
(trans
(congSubst (leftrightFst1 d x))
(subst-trans
(sym (leftFst1 d (rightFst0 d x)
(rightSnd0 d x)))
(sym (rightFst1 d x))))))
(snd-proof e))
(cong (subst A (snd-proof e)) (g-part e))))
(subst-trans {B = A}
(rightSnd1 d x
(subst E (sym (leftFst1 d (rightFst0 d x) (rightSnd0 d x))) e))
(leftSnd1 d (rightFst0 d x) (rightSnd0 d x) e))))))
where
snd-proof
= λ e -> trans
(rightSnd1 d x (subst E (sym (leftFst1 d (rightFst0 d x) (rightSnd0 d x))) e))
(leftSnd1 d (rightFst0 d x) (rightSnd0 d x) e)
g-part
= λ e →
let lemma-e = trans (congSubst (leftrightFst1 d x))
(subst-trans (sym (leftFst1 d (rightFst0 d x) (rightSnd0 d x)))
(sym (rightFst1 d x)))
in
trans
(trans
(sym (subst-cong (trans (subst-cong (sym (leftright0 d x))) lemma-e)))
(trans
(subst-trans (subst-cong (sym (leftright0 d x))) lemma-e)
(cong (subst (A ∘ (snd d (⟦ c ++[ E ⟶ d ] ⟧Info Z x))) lemma-e)
(congd g (subst-cong {B = E} (sym (leftright0 d x)))))))
(congd g lemma-e)
leftright0 {D} {c} {E} (δ d A) {U , T} (x , g)
= Σ-≡ (leftright0 d x)
(trans
(subst-dom (leftright0 d x))
(ext (λ { (e , a) →
let lemma-e = trans (congSubst (leftrightFst1 d x))
(subst-trans (sym (leftFst1 d (rightFst0 d x)
(rightSnd0 d x)))
(sym (rightFst1 d x)))
in
cong g
(trans
(subst-cong-Σ {B = E} {C = A} (sym (leftright0 d x)))
(Σ-≡ lemma-e
(trans
(subst-cong {B = A} lemma-e)
(trans
(sym (subst-trans
(cong₂d
((snd d) ∘ ⟦ c ++[ E ⟶ d ] ⟧Info (U , T))
(sym (leftright0 d x))
(subst-cong (sym (leftright0 d x))))
(cong (snd d (⟦ c ++[ E ⟶ d ] ⟧Info (U , T) x))
lemma-e)))
(trans
(congSubst (leftrightSnd1' d x e))
(subst-trans
(sym (leftSnd1 d (rightFst0 d x) (rightSnd0 d x) e))
(sym
(rightSnd1 d x
(subst E (sym (leftFst1 d
(rightFst0 d x)
(rightSnd0 d x)))
e))))))))) })))
leftrightFst1 : ∀ {D c}{E : Info c -> Set} d → {Z : Fam D} ->
(y : ⟦ (c ++[ E ⟶ d ]) ⟧Uni Z) ->
cong (fst d ∘ (⟦ c ++[ E ⟶ d ] ⟧Info Z)) (sym (leftright0 d y))
≡ trans (sym (leftFst1 d (rightFst0 d y) (rightSnd0 d y)))
(sym (rightFst1 d y))
leftrightFst1 d y = UIP _ _
leftrightSnd1 : ∀ {D c}{E : Info c -> Set} d → {Z : Fam D} ->
(y : ⟦ (c ++[ E ⟶ d ]) ⟧Uni Z) ->
(e : E _) ->
cong (λ z → snd d (⟦ c ++[ E ⟶ d ] ⟧Info Z (proj₁ z)) (proj₂ z))
(Σ-≡ (leftright0 d y)
(subst-sym-subst (leftright0 d y)))
≡ trans (cong (snd d (⟦ c ++[ E ⟶ d ] ⟧Info Z y))
(trans (subst-cong {B = E} (sym (leftright0 d y)))
(trans (congSubst (leftrightFst1 d y))
(subst-trans (sym (leftFst1 d (rightFst0 d y)
(rightSnd0 d y)))
(sym (rightFst1 d y))))))
(trans
(rightSnd1 d y (subst E (sym (leftFst1 d (rightFst0 d y)
(rightSnd0 d y))) e))
(leftSnd1 d (rightFst0 d y) (rightSnd0 d y) e))
leftrightSnd1 d y e = UIP _ _
leftrightSnd1' : ∀ {D c}{E : Info c -> Set} d → {Z : Fam D} ->
(y : ⟦ (c ++[ E ⟶ d ]) ⟧Uni Z) ->
(e : E _) ->
trans (cong₂d ((snd d) ∘ ⟦ c ++[ E ⟶ d ] ⟧Info Z)
(sym (leftright0 d y))
(subst-cong (sym (leftright0 d y))))
(cong (((snd d) ∘ ⟦ c ++[ E ⟶ d ] ⟧Info Z) y)
(trans (congSubst (leftrightFst1 d y))
(subst-trans (sym (leftFst1 d (rightFst0 d y)
(rightSnd0 d y)))
(sym (rightFst1 d y)))))
≡ trans (sym (leftSnd1 d (rightFst0 d y) (rightSnd0 d y) e))
(sym
(rightSnd1 d y (subst E (sym (leftFst1 d (rightFst0 d y)
(rightSnd0 d y))) e)))
leftrightSnd1' d y e = UIP _ _
leftright1 : ∀ {D c}{E : Info c -> Set} d → {Z : Fam D} ->
(y : ⟦ (c ++[ E ⟶ d ]) ⟧Uni Z) ->
trans (right1 d y) (left1 d (rightFst0 d y) (rightSnd0 d y))
≡ cong (both d ∘ (⟦ c ++[ E ⟶ d ] ⟧Info Z)) (leftright0 d y)
leftright1 d y = UIP _ _