\import Homotopy.Fibration
\import Paths
\import Logic.Unique
\import Equiv
\import Equiv.HalfAdjoint

\func hasContrFibers {A B : \Type} (f : A -> B) => \Pi (b : B) -> Contr (\Sigma (a : A) (f a = b))
  \where
    \lemma levelProp : isProp (hasContrFibers f)
      => pi-isProp (\lam b0 => Contr (Fib f b0)) (\lam b0 => Contr.levelProp (Fib f b0))

\func contrFibers=>Equiv {A B : \Type} {f : A -> B} (p : hasContrFibers f) : QEquiv f =>
  \let sec y => Contr.center {p y}
  \in \new QEquiv {
    | ret y => (sec y).
    | ret_f x => pmap (\lam (r : Fib f (f x)) => r.) (Contr.contraction {p (f x)} (x,idp))
    | f_sec y => (sec y).
  }

\lemma Equiv=>contrFibers (e : Equiv) : hasContrFibers e
  => fromSection e e
  \where {
    \protected \lemma fromSection (s : Section) (r : Retraction s) : hasContrFibers s
      => \lam b0 =>
          \let | r' y => pmap (\lam y => s (s.ret y)) (inv (r.f_sec y)) *> pmap s (s.ret_f (r.sec y)) *> r.f_sec y
               | f_sec => HAEquiv.coh_f_sec s r'
               | x0 => Fib.make (s.ret b0) (f_sec b0)
          \in Contr.make x0 (\lam x =>
              \let -- p0 proves that the first components are equal: x0.over = x.over.
                   | p0 => pmap s.ret (inv x.) *> s.ret_f x.
                   -- q0 proves that the second compontents are equal: pmap f p0 *> x.basePath = x0.basePath.
                   | q0 =>
                     pmap s p0 *> x.                                               ==< pmap (`*> x.) (pmap_*>-comm s _ _) >==
                     (pmap s (pmap s.ret (inv x.)) *> pmap s (s.ret_f x.)) *> x. ==< pmap ((pmap s (pmap s.ret (inv x.)) *> __) *> x.) (HAEquiv.coh_f_ret_f=f_sec_f s r' x.) >==
                     (pmap s (pmap s.ret (inv x.)) *> f_sec (s x.)) *> x.      ==< pmap (`*> x.) (homotopy-isNatural (\lam x => s (s.ret x)) (\lam x => x) f_sec (inv x.)) >==
                     (f_sec b0 *> inv x.) *> x.                                 ==< *>-assoc _ _ _ >==
                     f_sec b0 *> (inv x. *> x.)                                 ==< pmap (f_sec b0 *>) (inv_*> x.) >==
                     f_sec b0                                                     `qed
              \in Fib.ext b0 x0 x p0 q0)
  }