\import Equiv
\import Equiv.Fiber
\import Equiv.HalfAdjoint
\import HLevel
\import Homotopy.Fibration
\import Logic
\import Paths
\import Paths.Meta

\func lsigma {A : \Type} (a0 : A) : Contr (\Sigma (x : A) (a0 = x)) \cowith
  | center => (a0,idp)
  | contraction p => Jl (\lam x q => (a0,idp) = {\Sigma (y : A) (a0 = y)} (x,q)) idp p.

\func rsigma {A : \Type} (a0 : A) : Contr (\Sigma (x : A) (x = a0)) \cowith
  | center => (a0,idp)
  | contraction p => Jl (\lam x q => (a0,idp) = {\Sigma (y : A) (y = a0)} (x, inv q)) idp (inv p.) *> path (\lam i => (p., inv_inv p. @ i))

\func equiv= (e : QEquiv) : e.A = e.B => path (iso e.f e.ret e.ret_f e.f_sec)

\func contr-left {A : \Type} (c : Contr A) {B : A -> \Type} : QEquiv {\Sigma (x : A) (B x)} {B c.center} \cowith
  | f p => transport B (inv (c.contraction p.)) p.
  | ret b => (c.center, b)
  | ret_f p => inv (ext (inv (c.contraction p.), idp))
  | f_sec b => rewriteI (isProp=>isSet A (isContr=>isProp c) c.center c.center idp (c.contraction c.center)) idp

\func contr-right {A : \Type} (C : A -> Contr) : QEquiv {\Sigma (x : A) (C x)} {A} \cowith
  | f p => p.
  | ret a => (a, Contr.center {C a})
  | ret_f p => path (\lam i => (p., Contr.contraction {C p.} p. @ i))
  | f_sec a => idp

\func pi-contr-left {A : \Type} (a : A) (B : \Pi (a' : A) -> a = a' -> \Type) : QEquiv {\Pi (a' : A) (p : a = a') -> B a' p} {B a idp} \cowith
  | f h => h a idp
  | ret b a' => Jl B b
  | ret_f h => path (\lam i a' p => Jl (\lam x q => Jl B (h a idp) q = h x q) idp p @ i)
  | f_sec => idpe

\func pi-contr-right {A : \Type} (a' : A) (B : \Pi (a : A) -> a = a' -> \Type) : QEquiv {\Pi (a : A) (p : a = a') -> B a p} {B a' idp} \cowith
  | f h => h a' idp
  | ret b a => Jl.Jr B b
  | ret_f h => path (\lam i a p => Jl.Jr (\lam x q => Jl.Jr B (h a' idp) q = h x q) idp p @ i)
  | f_sec => idpe

\func sigma-left {A A' : \Type} {B' : A' -> \Type} (e : HAEquiv {A} {A'}) : QEquiv {\Sigma (a : A) (B' (e a))} {\Sigma (a' : A') (B' a')} \cowith
  | f p => (e p., p.)
  | ret p => (e.ret p., transport B' (inv (e.f_sec p.)) p.)
  | ret_f p => ext (e.ret_f p., path (\lam i => coe (\lam j => B' (e.f_ret_f=f_sec_f p. i j) ) _ right) *> transport_id_inv B' _ _)
  | f_sec p => ext (e.f_sec p., transport_id_inv B' _ _)
  \where {
    \func path-func (p : A = A') : (\Sigma (x : A) (B' (coe (p @) x right))) = (\Sigma (x' : A') (B' x')) =>
      path (\lam i => \Sigma (x : p @ i) (B' (coe2 (p @) i x right)))
  }

\func sigma-right {A : \Type} {B B' : A -> \Type} (q : \Pi (a : A) -> Equiv {B a} {B' a})
  : Equiv {\Sigma (a : A) (B a)} {\Sigma (a : A) (B' a)} \cowith
  | f p => (p., q p. p.)
  | ret p' => (p'., ret {q p'.} p'.)
  | sec p' => (p'., sec {q p'.} p'.)
  | ret_f p => path (\lam i => (p., ret_f {q p.} p. @ i))
  | f_sec p' => path (\lam i => (p'., f_sec {q p'.} p'. @ i))

\func sigma-equiv {A A' : \Type} {B : A -> \Type} {B' : A' -> \Type} (e1 : Equiv {A} {A'}) (e2 : \Pi (a : A) -> Equiv {B a} {B' (e1 a)})
  : Equiv {\Sigma (a : A) (B a)} {\Sigma (a : A') (B' a)}
  => sigma-right e2 `transEquiv` sigma-left e1

\func unit-func (A : \Type) : QEquiv {\Sigma -> A} {A} \cowith
  | f g => g ()
  | ret a _ => a
  | ret_f g => idp
  | f_sec a => idp

-- | The HoTT book, Theorem 4.7.7
\lemma totalEquiv {J : \Type} {A B : J -> \Type} (f : \Pi (j : J) -> A j -> B j)
  : (\Pi (j : J) -> Equiv (f j)) = Equiv total
  => propExt (\lam e => contrFibers=>Equiv (\lam p => rewrite (totalFiber p. p.) (Equiv=>contrFibers (e p.) p.)))
             (\lam e j => contrFibers=>Equiv (\lam b => rewriteI (totalFiber j b) (Equiv=>contrFibers e ((j,b) : \Sigma (j : J) (B j)))))
  \where {
    \func total (p : \Sigma (j : J) (A j)) : \Sigma (j : J) (B j)
      => (p., f p. p.)

    -- | Theorem 4.7.6
    \func totalFiber (j : J) (b : B j)
      : Fib total ((j,b) : \Sigma (j : J) (B j)) = Fib (f j) b
      => \let | S (X : J -> \Type) => \Sigma (j : J) (X j)
              | R (p : \Sigma (j' : J) (j' = j)) => \Sigma (a : A p.) (transport B p. (f p. a) = b)
         \in (\Sigma (p : S A) ((p., f p. p.) = {S B} (j,b)))                       ==< path (\lam i => \Sigma (p : S A) (equiv= (sigmaEquiv B (p., f p. p.) (j,b)) @ i)) >==
             (\Sigma (p : S A) (\Sigma (q : p. = j) (transport B q (f p. p.) = b))) ==< path (iso {\Sigma (p : S A) (\Sigma (q : p. = j) (transport B q (f p. p.) = b))}
                                                                                                     {\Sigma (p : \Sigma (j' : J) (j' = j)) (R p)}
                                                                                                     (\lam t => ((t..,t..),(t..,t..)))
                                                                                                     (\lam t => ((t..,t..),(t..,t..)))
                                                                                                     idpe idpe) >==
             (\Sigma (p : \Sigma (j' : J) (j' = j)) (R p))                             ==< equiv= (contr-left (rsigma j)) >==
             (\Sigma (a : A j) (f j a = b))                                            `qed
  }