\import Equiv
\import Equiv.HalfAdjoint
\import Paths

-- | If ``a = a'`` is a retract of ``R a a'``, then ``a = a'`` is equivalent to ``R a a'``.
\func pathEquiv {A : \Type} (R : A -> A -> \Type) (p : \Pi {a a' : A} -> Retraction {a = a'} {R a a'}) {a a' : A} : QEquiv {a = a'} p \cowith
  | ret => p.sec
  | ret_f => Jl (\lam _ q' => p.sec (p q') = q') (
    \let | h {a a' : A} (q : a = a') => p.sec (p q)
         | h-idemp {a a' : A} (q : a = a') : h (h q) = h q => pmap p.sec (p.f_sec (p q))
    \in Jl (\lam _ q => h idp = h q *> inv q) idp (h idp) *> pmap (`*> inv (h idp)) (h-idemp idp) *> *>_inv (h idp)
  )
  | f_sec => p.f_sec

\func pathConcatEquiv {A : \Type} {a b c : A} (p : a = b) : QEquiv {a = c} {b = c} \cowith
  | f => inv p *>
  | ret => p *>
  | ret_f q => inv (*>-assoc _ _ _) *> pmap (`*> q) (*>_inv p) *> idp_*> q
  | f_sec q => inv (*>-assoc _ _ _) *> pmap (`*> q) (inv_*> p) *> idp_*> q

-- | If ``f : A -> B`` is an equivalence, then ``pmap f`` is also an equivalence.
\func pmapEquiv (e : Equiv) {a a' : e.A} : QEquiv {a = a'} => pathEquiv (e __ = e __) (\lam {a} {a'} => \new Retraction {
  | f => pmap e
  | sec p => inv (e.ret_f a) *> pmap e.ret p *> e.ret_f a'
  | f_sec p => \let hae : HAEquiv => e \in
    pmap e (inv (e.ret_f a) *> pmap e.ret p *> e.ret_f a')                   ==< pmap_*>-comm e (inv (e.ret_f a)) (pmap e.ret p *> e.ret_f a') >==
    pmap e (inv (e.ret_f a)) *> pmap e (pmap e.ret p *> e.ret_f a')          ==< pmap2 (*>) (pmap_inv-comm e (e.ret_f a)) (pmap_*>-comm e (pmap e.ret p) (e.ret_f a')) >==
    inv (pmap e (e.ret_f a)) *> pmap e (pmap e.ret p) *> pmap e (e.ret_f a') ==< rotatePathLeft (
        pmap e (pmap e.ret p) *> pmap e (e.ret_f a') ==< pmap (pmap e (pmap e.ret p) *> __) (hae.f_ret_f=f_sec_f a') >==
        pmap e (pmap e.ret p) *> hae.f_sec (e a')    ==< homotopy-isNatural (\lam y => e (e.ret y)) (\lam y => y) hae.f_sec p >==
        hae.f_sec (e a) *> p                         ==< inv (pmap (`*> p) (hae.f_ret_f=f_sec_f a)) >==
        pmap e (e.ret_f a) *> p                      `qed) >==
    p `qed
  })

-- | If ``f : A -> B`` is an embedding, then ``pmap f`` is also an embedding.
\func pmapEmbedding (e : Embedding) {a a' : e.A} : Embedding {a = a'} (pmap e) \cowith
  | isEmb _ _ => pmapEquiv (e.pmap-isEquiv {a} {a'})

-- | If ``f : A -> B`` is a section, then ``pmap f`` is also a section.
\func pmapSection (s : Section) {a a' : s.A} : Section {a = a'} (pmap s) \cowith
  | ret q => (inv (s.ret_f a) *> pmap s.ret q) *> s.ret_f a'
  | ret_f q => Jl (\lam a'' q' => (inv (s.ret_f a) *> pmap s.ret (pmap s q')) *> s.ret_f a'' = q') (inv_*> (s.ret_f a)) q