\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) {}
                                        (Retraction.isContr e)
                                        (\lam r => HLevels_-2-pi (T1 r) {} (T1-isContr r))
           | E : T2 = HAEquiv f => path (iso (\lam (t : T2) => \new HAEquiv f {
                                          | ret => sec {t.}
                                          | f_sec => f_sec {t.}
                                          | ret_f x => (t. x).
                                          | f_ret_f=f_sec_f x => (t. x).
                                          }) (\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'
  }