module Uniform.AppLift.Rightleft where
open import Prelude.Basic
open import Prelude.Equality
open import Prelude.Fam
open import Uniform.IR
open import Uniform.AppLift.Maps
rightleftFst0 : ∀ {D c}{E : Info c -> Set} d → {Z : Fam D} ->
(x : ⟦ c ⟧Uni Z)(g : (e : E (⟦ c ⟧Info Z x)) -> ⟦ d ⟧Uni Z) ->
x ≡ rightFst0 {D} {c} {E} d (left0 d (x , g))
rightleftFst0 ι x _ = refl
rightleftFst0 (σ d A) x g = rightleftFst0 d x (proj₁ ∘ g)
rightleftFst0 (δ d A) x g = rightleftFst0 d x (proj₁ ∘ g)
rightleftFst1 : ∀ {D c}{E : Info c -> Set} d → {Z : Fam D} ->
(x : ⟦ c ⟧Uni Z)(g : (e : E (⟦ c ⟧Info Z x)) -> ⟦ d ⟧Uni Z) ->
cong (⟦ c ⟧Info Z) (sym (rightleftFst0 d x g))
≡ trans (sym (rightFst1 {D} {c} {E} d (left0 d (x , g))))
(sym (leftFst1 {D} {c} {E} d x g))
rightleftFst1 ι x g = refl
rightleftFst1 (σ d A) x g = rightleftFst1 d _ _
rightleftFst1 (δ d A) x g = rightleftFst1 d _ _
mutual
rightleftSnd0 : ∀ {D c}{E : Info c -> Set} d → {Z : Fam D} ->
(x : ⟦ c ⟧Uni Z)(g : (e : E (⟦ c ⟧Info Z x)) -> ⟦ d ⟧Uni Z) ->
(e : E _) ->
g (subst E (cong (⟦ c ⟧Info Z) (sym (rightleftFst0 {c = c} {E} d x g))) e)
≡ rightSnd0 {c = c} {E} d (left0 d (x , g)) e
rightleftSnd0 ι x g e = refl
rightleftSnd0 {D} {c} {E} (σ d A) {Z} x g e =
let g' = proj₁ ∘ g in
Σ-≡ (rightleftSnd0 d x g' e)
(trans
(subst-cong {B = A} (rightleftSnd0 d x g' e))
(trans
(subst-eventually-trans
(cong (⟦ d ⟧Info Z ∘ g')
(subst-eventually-trans
(sym (rightFst1 d (left0 d (x , g'))))
(rightleftFst1 d x g')))
(rightleftSnd1 d x g' e))
(trans
(subst-trans
(leftSnd1 d x g'
(subst E (sym (rightFst1 d (left0 d (x , g')))) e))
(rightSnd1 d (left0 d (x , g')) e))
(cong
(subst A (rightSnd1 d (left0 d (x , g')) e) ∘
(subst A
(leftSnd1 d x g'
(subst E
(sym
(rightFst1 d
(left0 d
(x , g'))))
e))))
(trans
(sym (subst-cong
(subst-eventually-trans
(sym (rightFst1 d (left0 d (x , g'))))
(rightleftFst1 d x g'))))
(congd (proj₂ ∘ g)
(subst-eventually-trans
(sym (rightFst1 d (left0 d (x , g'))))
(rightleftFst1 d x g'))))))))
rightleftSnd0 {D} {c} {E} (δ d A) {Z} x g e =
let g' = proj₁ ∘ g
fst-proof = trans (congSubst (rightleftFst1 d x g'))
(subst-trans
(sym (rightFst1 d (left0 d (x , g'))))
(sym (leftFst1 d x g')))
in
Σ-≡ (rightleftSnd0 d x g' e)
(trans (subst-dom (rightleftSnd0 d x g' e))
((ext (λ a →
cong₂d
(λ z w → proj₂ (g z) w)
fst-proof
(trans
(trans
(subst-cong {B = A ∘ (⟦ d ⟧Info Z)} fst-proof)
(trans
(sym (subst-trans (sym (rightleftSnd0 d x g' e))
(cong g' fst-proof)))
(subst-cong {B = A}
(trans
(sym (rightleftSnd0 d x g' e))
(cong g' fst-proof)))))
(trans
(congSubst (rightleftSnd1' d x g' e))
(subst-trans
(sym (rightSnd1 d (left0 d (x , g')) e))
(sym
(leftSnd1
d x g'
(subst E (sym (rightFst1 d (left0 d (x , g'))))
e))))))))))
rightleftSnd1 : ∀ {D c}{E : Info c -> Set} d → {Z : Fam D} ->
(x : ⟦ c ⟧Uni Z)(g : (e : E (⟦ c ⟧Info Z x)) -> ⟦ d ⟧Uni Z) ->
(e : E _) ->
cong (⟦ d ⟧Info Z)
(rightleftSnd0 {D} {c} {E} d x g e)
≡ trans
(cong (⟦ d ⟧Info Z ∘ g)
(subst-eventually-trans
(sym (rightFst1 d (left0 d (x , g))))
(rightleftFst1 d x g)))
(trans
(leftSnd1 {D} {c} {E} d x g
(subst E
(sym
(rightFst1 d (left0 d (x , g))))
e))
(rightSnd1 d (left0 d (x , g)) e))
rightleftSnd1 d x g e = UIP _ _
rightleftSnd1' : ∀ {D c}{E : Info c -> Set} d → {Z : Fam D} ->
(x : ⟦ c ⟧Uni Z)(g : (e : E (⟦ c ⟧Info Z x)) -> ⟦ d ⟧Uni Z) ->
(e : E _) ->
cong (⟦ d ⟧Info Z)
(trans
(sym (rightleftSnd0 {D} {c} {E} d x g e))
(cong g (subst-eventually-trans {B = E}
(sym (rightFst1 {D} {c} {E} d (left0 d (x , g))))
(rightleftFst1 {D} {c} {E} d x g))))
≡ trans (sym (rightSnd1 {D} {c} {E} d (left0 d (x , g)) e))
(sym (leftSnd1 {D} {c} {E} d x g
(subst E
(sym
(rightFst1 d (left0 d (x , g))))
e)))
rightleftSnd1' d x g e = UIP _ _
rightleft0 : ∀ {D c}{E : Info c -> Set} d → {Z : Fam D} ->
(y : Σ[ x ∈ ⟦ c ⟧Uni Z ] ((e : E (⟦ c ⟧Info Z x)) -> ⟦ d ⟧Uni Z)) ->
y ≡ right0 {D} {c} {E} d (left0 d y)
rightleft0 {D} {c} {E} d {Z} y =
let x = proj₁ y
g = proj₂ y
in Σ-≡ (rightleftFst0 {D} {c} {E} d x g)
(trans (subst-dom (rightleftFst0 d x g))
(ext (λ e → trans
(cong g (subst-cong (sym (rightleftFst0 d x g))))
(rightleftSnd0 d x g e))))
rightleft1 : ∀ {D c}{E : Info c -> Set} d → {Z : Fam D} ->
(y : _) ->
trans (left1 {c = c} {E} d (proj₁ y) (proj₂ y))
(right1 d (left0 d y))
≡ cong (map (⟦ c ⟧Info Z) (λ h → (⟦ d ⟧Info Z) ∘ h))
(rightleft0 d y)
rightleft1 d y = UIP _ _