\import Equiv
\import Equiv.Fiber
\import Equiv.Univalence
\import HLevel
\import Homotopy.Fibration
\import Paths
\import Paths.Meta

\record HAEquiv \extends QEquiv
| f_ret_f=f_sec_f : \Pi (x : A) -> pmap f (ret_f x) = f_sec (f x)
\where {
\use \coerce fromQEquiv (e : QEquiv) : HAEquiv \cowith
| Section => e
| f_sec y => inv (e.f_sec (e (e.ret y))) *> pmap e (e.ret_f (e.ret y)) *> e.f_sec y
| f_ret_f=f_sec_f x => inv (rotatePathLeft (
pmap e (e.ret_f (e.ret (e x))) *> e.f_sec (e x)               ==< pmap (pmap e __ *> e.f_sec (e x)) (homotopy_app-comm (\lam x => e.ret (e x)) e.ret_f x) >==
pmap (\lam x => e (e.ret (e x))) (e.ret_f x) *> e.f_sec (e x) ==< homotopy-isNatural (\lam y => e (e.sec y)) (\lam y => y) e.f_sec (pmap e (e.ret_f x))              >==
e.f_sec (e (e.ret (e x))) *> pmap e (e.ret_f x)               qed
))

\use \level levelProp {A B : \Type} {f : A -> B} (e e' : HAEquiv f) : e = e' =>
\let -- HAEquiv = Retraction + T1' = Retraction + T1
| T1' (r : Retraction f) (x : A) =>
(r.sec (f x), r.f_sec (f x)) = {Fib f (f x)} (x,idp)
| T1 (r : Retraction f) (x : A) =>
\Sigma (p : r.sec (f x) = x) (pmap f p = r.f_sec (f x))
| T1'=T1 (r : Retraction f) (x : A) : T1' r x = T1 r x =>
Equiv-to-= (Fib.equiv (f x) (r.sec (f x), r.f_sec (f x)) (x,idp))
| T1'-isContr (r : Retraction f) (x : A) : Contr (T1' r x) =>
isProp=>HLevel_-2+1 (Fib f (f x)) (isContr=>isProp (Equiv=>contrFibers e (f x))) _ _
| T1-isContr (r : Retraction f) (x : A) : Contr (T1 r x) =>
rewriteI (T1'=T1 r x) (T1'-isContr r x)
| T2 => \Sigma (r : Retraction f) (\Pi (x : A) -> T1 r x)
| T2-isContr : Contr T2 => HLevels_-2-sigma (\Pi (x : A) -> T1 __ x) {0}
(Retraction.isContr e)
(\lam r => HLevels_-2-pi (T1 r) {0} (T1-isContr r))
| E : T2 = HAEquiv f => path (iso (\lam (t : T2) => \new HAEquiv f {
| ret => sec {t.1}
| f_sec => f_sec {t.1}
| ret_f x => (t.2 x).1
| f_ret_f=f_sec_f x => (t.2 x).2
}) (\lam (r : HAEquiv f) => (\new Retraction f r.sec r.f_sec, \lam x => (r.ret_f x, r.f_ret_f=f_sec_f x)))
(\lam t2 => idp) (\lam (hae : HAEquiv f) => idp {HAEquiv f hae.ret hae.ret_f hae.f_sec hae.f_ret_f=f_sec_f}))
\in isContr=>isProp (rewriteI E T2-isContr) e e'
}
`