\import Equiv
\import Equiv.Fiber
\import Equiv.Univalence
\import Function.Meta
\import Logic.Unique
\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 {
    \protected \func coh_f_sec (s : Section) (r : \Pi (y : s.B) -> s (s.ret y) = y) (y : s.B) : s (s.ret y) = y
      => inv (r (s (s.ret y))) *> pmap s (s.ret_f (s.ret y)) *> r y

    \protected \func coh_f_ret_f=f_sec_f (s : Section) (r : \Pi (y : s.B) -> s (s.ret y) = y) (x : s.A) : pmap s (s.ret_f x) = coh_f_sec s r (s x)
      => inv $ rotatePathLeft $
          pmap s (s.ret_f (s.ret (s x))) *> r (s x)               ==< pmap (pmap s __ *> r (s x)) (homotopy_app-comm (\lam x => s.ret (s x)) s.ret_f x) >==
          pmap (\lam x => s (s.ret (s x))) (s.ret_f x) *> r (s x) ==< homotopy-isNatural (\lam y => s (s.ret y)) (\lam y => y) r (pmap s (s.ret_f x))   >==
          r (s (s.ret (s x))) *> pmap s (s.ret_f x)               `qed

    \use \coerce fromQEquiv (e : QEquiv) : HAEquiv \cowith
      | Section => e
      | f_sec => coh_f_sec e e.f_sec
      | f_ret_f=f_sec_f => coh_f_ret_f=f_sec_f e e.f_sec

    \lemma levelProp {A B : \Type} {f : A -> B} : isProp (HAEquiv f)
      => \lam 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=>PathContr (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 => sigma-Contr (\Pi (x : A) -> T1 __ x)
                                        (Retraction.isContr e)
                                        (\lam r => pi-Contr (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'
  }