module Uniform.AppLift where

open import Prelude.Basic
open import Prelude.Fam
open import Prelude.Equality
open import Prelude.Equivalences
open import Uniform.IR

-- maps back and forth
import Uniform.AppLift.Maps as A

-- and they compose to the identity
import Uniform.AppLift.Rightleft as AR
import Uniform.AppLift.Leftright as AL

-- In order to confirm that the below equivalence is all we need, we
-- do re-export Uniform.AppLift.Maps and Uniform.AppLift.{Rightleft,
-- Leftright}. However, we do reexport _++[_⟶_]:

_++[_⟶_] = A._++[_⟶_]
fst       = A.fst
snd       = A.snd
both      = A.both

applift-equiv : ∀ {D} →
                (c : Uni D) -> (E : Info c -> Set) -> (d : Uni D) ->
                {Z : Fam D} ->
                (⟦ c , id ⟧ Z Fam->>== (λ e → (E e) Fam⟶ ⟦ d , id ⟧ Z))
                    ≃ ⟦ (c ++[ E ⟶ d ]) , both d ⟧ Z
applift-equiv c E d
 = record { left = A.left0 d , (λ x → A.left1 d (proj₁ x) (proj₂ x))
          ; right = A.right0 d , A.right1 d
          ; leftright = comp-is-id-ext
                         (A.left0 d , (λ x →
                                    (A.left1 {c = c} d (proj₁ x) (proj₂ x))))
                         (A.right0 d , A.right1 d)
                         (AL.leftright0 {c = c} {E} d)
                         (AL.leftright1 d)
          ; rightleft = comp-is-id-ext
                         (A.right0 d , A.right1 d)
                         (A.left0 d , (λ x →
                                    (A.left1 {c = c} {E} d (proj₁ x) (proj₂ x))))
                         (AR.rightleft0 {c = c} {E} d)
                         (AR.rightleft1 d)
          }


-- We now re-export the definitions we need from the equivalence.
-- This shows that the equivalence contains all the information we
-- need for the rest of the proof. However their exact definition does
-- not matter, so we can keep them abstract.
abstract

  rightFst0 : {D : Set₁} {c : Uni D} {E : Info c → Set} (d : Uni D)
              {Z : Fam D} → ⟦ c ++[ E ⟶ d ] ⟧Uni Z → ⟦ c ⟧Uni Z
  rightFst0 {D} {c} {E} d {Z} x
    = proj₁ (_Fam⇒_.indmor (_≃_.right (applift-equiv c E d)) x)

  rightFst1 : {D : Set₁} {c : Uni D} {E : Info c → Set} (d : Uni 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 {c = c} {E} d {Z} x
    = cong proj₁ (_Fam⇒_.indmor= (_≃_.right (applift-equiv c E d)) x)

  rightSnd0 : {D : Set₁} {c : Uni D} {E : Info c → Set} (d : Uni D)
               {Z : Fam D} (x : ⟦ c ++[ E ⟶ d ] ⟧Uni Z) →
               E (⟦ c ⟧Info Z (rightFst0 d x)) → ⟦ d ⟧Uni Z
  rightSnd0 {c = c} {E} d {Z} x y
    = proj₂ (_Fam⇒_.indmor (_≃_.right (applift-equiv c E d)) x) y

  rightSnd1 : {D : Set₁} {c : Uni D} {E : Info c → Set} (d : Uni 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 {D} {c = c} {E} d {Z} x y
   = happly
      (trans (sym
        (trans
          (subst-cong (_Fam⇒_.indmor= (_≃_.right (applift-equiv c E d)) x))
          (subst-dom (rightFst1 d x))))
        (congd proj₂ (_Fam⇒_.indmor= (_≃_.right (applift-equiv c E d)) x)))
      y


-- We do need to know that right0 = (right0Fst, right0Snd) and
-- similarly for left0
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)

left0 : {D : Set₁} {c : Uni D} {E : Info c → Set} (d : Uni D)
        {Z : Fam D} →
        Σ-syntax (⟦ c ⟧Uni Z) (λ x → E (⟦ c ⟧Info Z x) → ⟦ d ⟧Uni Z) →
        ⟦ c ++[ E ⟶ d ] ⟧Uni Z
left0 {c = c} {E} d {Z} x = _Fam⇒_.indmor (_≃_.left (applift-equiv c E d)) x

-- But we can keep the rest of the proofs abstract
abstract
  leftright0 : {D : Set₁} {c : Uni D} {E : Info c → Set} (d : Uni D)
        {Z : Fam D} (y : ⟦ c ++[ E ⟶ d ] ⟧Uni Z) →
        y ≡ left0 d (right0 d y)
  leftright0 {c = c} {E} d {Z} y
    = sym (happly (cong _Fam⇒_.indmor
                        (_≃_.leftright (applift-equiv c E d))) y)

  leftFst1 : {D : Set₁} {c : Uni D} {E : Info c → Set} (d : Uni D)
             {Z : Fam D} (x : ⟦ c ⟧Uni Z) (g : E (⟦ c ⟧Info Z x) → ⟦ d ⟧Uni Z) →
             ⟦ c ⟧Info Z x ≡
             fst d (⟦ c ++[ E ⟶ d ] ⟧Info Z (left0 d (x , g)))
  leftFst1 {c = c} {E} d {Z} x g
     = cong proj₁ (_Fam⇒_.indmor= (_≃_.left (applift-equiv c E d)) (x , g))

  leftSnd1 : {D : Set₁} {c : Uni D} {E : Info c → Set} (d : Uni D)
             {Z : Fam D} (x : ⟦ c ⟧Uni Z) (g : E (⟦ c ⟧Info Z x) → ⟦ d ⟧Uni Z)
             (e : E (fst d (⟦ c ++[ E ⟶ d ] ⟧Info Z (left0 d (x , g))))) →
             ⟦ 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 {c = c} {E} d {Z} x g e
   = happly
      (trans
        (sym
          (trans
            (subst-cong (_Fam⇒_.indmor= (_≃_.left (applift-equiv c E d))
                                         (x , g)))
            (subst-dom (leftFst1 d x g))))
        (congd proj₂
               (_Fam⇒_.indmor= (_≃_.left (applift-equiv c E d)) (x , g))))
      e

  rightleftFst0 : {D : Set₁} {c : Uni D} {E : Info c → Set} (d : Uni D)
                  {Z : Fam D}
                  (x : ⟦ c ⟧Uni Z) (g : E (⟦ c ⟧Info Z x) → ⟦ d ⟧Uni Z) →
                  x ≡ rightFst0 {c = c} {E} d (left0 d (x , g))
  rightleftFst0 {c = c} {E} d {Z} x g
    = cong proj₁
           (sym (happly (cong _Fam⇒_.indmor
                              (_≃_.rightleft (applift-equiv c E d))) (x , g)))

  rightleftSnd0 : {D : Set₁} {c : Uni D} {E : Info c → Set} (d : Uni D)
                  {Z : Fam D}
                  (x : ⟦ c ⟧Uni Z) (g : E (⟦ c ⟧Info Z x) → ⟦ d ⟧Uni Z)
                  (e : E (⟦ c ⟧Info Z (rightFst0 {c = c} d
                  (left0 d (x , g))))) →
                  g (subst E (cong (⟦ c ⟧Info Z) (sym (rightleftFst0 d x g))) e)
                    ≡ rightSnd0 {c = c} {E} d (left0 d (x , g)) e
  rightleftSnd0 {c = c} {E} d {Z} x g e
   = trans
      (trans
         (cong g (sym (subst-cong {B = E} (sym (rightleftFst0 d x g)))))
         (happly (sym
            (trans
              (subst-cong {B = λ z → E (⟦ c ⟧Info Z z) -> ⟦ d ⟧Uni Z}
                          (sym (happly
                                 (cong _Fam⇒_.indmor
                                       (_≃_.rightleft (applift-equiv c E d)))
                                 (x , g))))
              (subst-dom (rightleftFst0 d x g)))) e))
      (happly (congd proj₂ (sym (happly
                                  (cong _Fam⇒_.indmor
                                        (_≃_.rightleft (applift-equiv c E d)))
                                  (x , g)))) e)

  rightleftFst1 : {D : Set₁} {c : Uni D} {E : Info c → Set} (d : Uni D)
                  {Z : Fam D}
                  (x : ⟦ c ⟧Uni Z) (g : 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 x g))
  rightleftFst1 {c = c} {E} d {Z} x g = UIP _ _ -- cheating for now

  rightleftSnd1 : {D : Set₁} {c : Uni D} {E : Info c → Set} (d : Uni D)
                  {Z : Fam D} (x : ⟦ c ⟧Uni Z)
                  (g : E (⟦ c ⟧Info Z x) → ⟦ d ⟧Uni Z)
                  (e : E (⟦ c ⟧Info Z
                                   (rightFst0 {D} {c} d (left0 d (x , g))))) ->
                  cong (⟦ d ⟧Info Z) (rightleftSnd0 {D} {c} {E} d x g e) ≡
                  trans
                    (cong ((⟦ d ⟧Info Z) ∘ g)
                    (subst-eventually-trans
                      (sym (rightFst1 {D} {c} d (left0 d (x , g))))
                      (rightleftFst1 {D} {c} d x g)))
                    (trans
                      (leftSnd1 d x g
                                (subst E
                                       (sym (rightFst1 d (left0 d (x , g))))
                                       e))
                      (rightSnd1 d (left0 d (x , g)) e))
  rightleftSnd1 {c = c} {E} d {Z} x g e = UIP _ _ -- cheating for now