\import Equiv
\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