\import Equiv
\import Equiv.Fiber
\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.2

\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.2) *> path (\lam i => (p.1, inv_inv p.2 @ 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.1)) p.2
| ret b => (c.center, b)
| ret_f p => inv (ext (inv (c.contraction p.1), 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.1
| ret a => (a, Contr.center {C a})
| ret_f p => path (\lam i => (p.1, Contr.contraction {C p.1} p.2 @ 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.1, p.2)
| ret p => (e.ret p.1, transport B' (inv (e.f_sec p.1)) p.2)
| ret_f p => ext (e.ret_f p.1, path (\lam i => coe (\lam j => B' (e.f_ret_f=f_sec_f p.1 i j) ) _ right) *> transport_id_inv B' _ _)
| f_sec p => ext (e.f_sec p.1, 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.1, q p.1 p.2)
| ret p' => (p'.1, ret {q p'.1} p'.2)
| sec p' => (p'.1, sec {q p'.1} p'.2)
| ret_f p => path (\lam i => (p.1, ret_f {q p.1} p.2 @ i))
| f_sec p' => path (\lam i => (p'.1, f_sec {q p'.1} p'.2 @ 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.1 p.2) (Equiv=>contrFibers (e p.1) p.2)))
(\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.1, f p.1 p.2)

-- | 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.1) (transport B p.2 (f p.1 a) = b)
\in (\Sigma (p : S A) ((p.1, f p.1 p.2) = {S B} (j,b)))                       ==< path (\lam i => \Sigma (p : S A) (equiv= (sigmaEquiv B (p.1, f p.1 p.2) (j,b)) @ i)) >==
(\Sigma (p : S A) (\Sigma (q : p.1 = j) (transport B q (f p.1 p.2) = b))) ==< path (iso {\Sigma (p : S A) (\Sigma (q : p.1 = j) (transport B q (f p.1 p.2) = b))}
{\Sigma (p : \Sigma (j' : J) (j' = j)) (R p)}
(\lam t => ((t.1.1,t.2.1),(t.1.2,t.2.2)))
(\lam t => ((t.1.1,t.2.1),(t.1.2,t.2.2)))
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
}
`