\import Equiv.Fiber
\import Equiv.Path
\import Function
\import HLevel
\import Homotopy.Fibration
\import Logic
\import Logic.Meta
\import Paths
\import Paths.Meta

-- # Definition of equivalences

\protected \record Map {A B : \Type} (\coerce f : A -> B)

\record Section \extends Map
| ret : B -> A
| ret_f : \Pi (x : A) -> ret (f x) = x
\where {
\func =Fiber {A B : \Type} (f : A -> B) : Section f = Fib (-o f) id
=> path (iso (\lam (s : Section f) => Fib.make s.ret (path (\lam i x => s.ret_f x @ i)))
(\lam z => \new Section f z.1 (\lam x => path ((z.2 @ __) x)))
idpe
idpe)

\lemma isContr (e : Equiv) : Contr (Section e)
=> rewrite (=Fiber e) (Equiv=>contrFibers (-o_Equiv e) id)

\lemma levelProp (r : Retraction) : isProp (Section r)
=> \lam s => isContr=>isProp (isContr (\new Equiv { | Section => s | Retraction => r })) s
}

\record Retraction \extends Map
| sec : B -> A
| f_sec : \Pi (y : B) -> f (sec y) = y
\where {
\func =Fiber {A B : \Type} (f : A -> B) : Retraction f = Fib (f o-) id
=> path (iso (\lam (s : Retraction f) => Fib.make s.sec (path (\lam i x => s.f_sec x @ i)))
(\lam z => \new Retraction f z.1 (\lam x => path ((z.2 @ __) x)))
idpe
idpe)

\lemma isContr (e : Equiv) : Contr (Retraction e)
=> rewrite (=Fiber e) (Equiv=>contrFibers (o-_Equiv e) id)

\lemma levelProp (s : Section) : isProp (Retraction s)
=> \lam r => isContr=>isProp (isContr (\new Equiv { | Section => s | Retraction => r })) r
}

\record Equiv \extends Section, Retraction {
\func f_ret (y : B) : f (ret y) = y
=> pmap (\lam y => f (ret y)) (inv (f_sec y)) *> pmap f (ret_f (sec y)) *> f_sec y

\func isInj {a a' : A} (p : f a = f a') : a = a'
=> inv (ret_f a) *> pmap ret p *> ret_f a'

\lemma isSurj : Function.isSurj f
=> \lam y => inP (ret y, f_ret y)

\func adjoint {a : A} {b : B} (p : f a = b) : a = ret b
=> inv (ret_f a) *> pmap ret p

\func adjointInv {a : A} {b : B} (p : a = ret b) : f a = b
=> pmap f p *> f_ret b
}
\where {
\use \level levelProp {A B : \Type} {f : A -> B} (e e' : Equiv f) : e = e' =>
path (\lam i => \new Equiv {
| Section => isContr=>isProp {Section f} (Section.isContr e) e e' @ i
| Retraction => isContr=>isProp {Retraction f} (Retraction.isContr e) e e' @ i
})

\func equals {A B : \Type} {e e' : Equiv {A} {B}} (p : e.f = e'.f) : e = e' =>
path (\lam i => \new Equiv {
| Section => pathOver (isContr=>isProp (Section.isContr e')
(rewriteI p (\new Section e.f e.ret e.ret_f))
(\new Section e'.f e'.ret e'.ret_f)) @ i
| Retraction => pathOver (isContr=>isProp (Retraction.isContr e')
(rewriteI p (\new Retraction e.f e.sec e.f_sec))
(\new Retraction e'.f e'.sec e'.f_sec)) @ i
})

\lemma fromInjSurj {A B : \Set} (f : A -> B) (inj : Function.isInj f) (surj : Function.isSurj f) : Equiv {A} {B} f
=> \new ESEquiv {
| Embedding => Embedding.fromInjection inj
| isSurjMap => surj
}
}

\record QEquiv \extends Equiv { | sec => ret }
\where {
\use \coerce fromEquiv (e : Equiv) : QEquiv \cowith
| Section => e
| f_sec => e.f_ret

\func fromEquiv' (e : Equiv) : QEquiv \cowith
| Map => e
| ret => e.sec
| ret_f a => inv (e.ret_f (e.sec (e a))) *> pmap e.ret (e.f_sec (e a)) *> e.ret_f a
| f_sec => e.f_sec
}

-- # Examples of equialences

\func idEquiv {A : \Type} : QEquiv \cowith
| A => A
| B => A
| f x => x
| ret x => x
| ret_f _ => idp
| f_sec _ => idp

\func symQEquiv {A B : \Type} (e : QEquiv {A} {B}) : QEquiv {B} {A} \cowith
| f => e.ret
| ret => e.f
| ret_f => e.f_sec
| f_sec => e.ret_f

\func \fixr 3 transQEquiv {A B C : \Type} (e1 : QEquiv {A} {B}) (e2 : QEquiv {B} {C}) : QEquiv {A} {C} \cowith
| f x => e2 (e1 x)
| ret y => e1.ret (e2.ret y)
| ret_f x => pmap e1.ret (e2.ret_f (e1 x)) *> e1.ret_f x
| f_sec y => pmap e2 (e1.f_sec (e2.sec y)) *> e2.f_sec y

\module TwoOutOfThree \where {
\func leftFactor {A B C : \Type} (e1 : Retraction {A} {B}) (g : B -> C) (e3 : QEquiv (g o e1)) : QEquiv g \cowith
| ret c => e1 (e3.ret c)
| ret_f b =>
e1 (e3.ret (g b))               ==< pmap (e1 o e3.ret o g) (inv (e1.f_sec b)) >==
e1 (e3.ret (g (e1 (e1.sec b)))) ==< pmap e1 (e3.ret_f (e1.sec b)) >==
e1 (e1.sec b)                   ==< e1.f_sec b >==
b                               qed
| f_sec => e3.f_sec

\func leftFactorPath {A B C : \Type} (e1 : Retraction {A} {B}) {g : B -> C} (e3 : QEquiv {A} {C}) (p : g o e1 = e3) : QEquiv g
=> leftFactor e1 g (transportInv (QEquiv __) p e3)

\func rightFactor {A B C : \Type} (f : A -> B) (e2 : Section {B} {C}) (e3 : QEquiv (\lam a => e2 (f a))) : QEquiv f \cowith
| ret b => e3.ret (e2 b)
| ret_f => e3.ret_f
| f_sec b =>
f (e3.ret (e2 b))               ==< inv (e2.ret_f (f (e3.ret (e2 b)))) >==
e2.ret (e2 (f (e3.ret (e2 b)))) ==< pmap e2.ret (e3.f_sec (e2 b)) >==
e2.ret (e2 b)                   ==< e2.ret_f b >==
b                               qed

\func rightFactorPath {A B C : \Type} {f : A -> B} (e2 : Section {B} {C}) (e3 : QEquiv {A} {C}) (p : e2 o f = e3) : QEquiv f
=> rightFactor f e2 (transportInv (QEquiv __) p e3)

\lemma rightEmbedding {A B C : \Type} (f : A -> B) (e2 : B >-> C) (e3 : QEquiv (e2 o f)) : Equiv f
=> rightFactor f (\new ESEquiv e2 {
| isEmb => e2.isEmb
| isSurjMap c => inP (f (e3.ret c), e3.f_sec c)
}) e3

\lemma parallelEquiv {A B C D : \Type} (ab : A -> B) (cd : C -> D) (ac : Equiv {A} {C}) (bd : Equiv {B} {D}) (h : \Pi (a : A) -> bd (ab a) = cd (ac a)) : Equiv ab = Equiv cd
=> propExt (\lam e => leftFactor ac cd (coe (\lam i => QEquiv (h __ @ i)) (transQEquiv e bd) right))
(\lam e => rightFactor ab bd (coe (\lam i => QEquiv (\lam a => inv (h a) @ i)) (transQEquiv ac e) right))

\lemma leftEquiv {A B C : \Type} (e : Equiv {A} {B}) (g : B -> C) : Equiv g = Equiv (g o e)
=> propExt (\lam e2 => transEquiv e e2) (\lam e3 => leftFactor e g e3)

\lemma rightEquiv {A B C : \Type} (f : A -> B) (e : Equiv {B} {C}) : Equiv f = Equiv (e o f)
=> propExt (\lam e1 => transEquiv e1 e) (\lam e3 => rightFactor f e e3)

\lemma compositeEquiv {A B C : \Type} (f : A -> B) (g : B -> C) (e : Equiv (g o f)) : Equiv f = Equiv g
=> propExt (\lam e1 => leftFactor e1 g e) (\lam e2 => rightFactor f e2 e)
}

\func \fixr 3 transEquiv {A B C : \Type} (e1 : Equiv {A} {B}) (e2 : Equiv {B} {C}) : Equiv {A} {C} \cowith
| f x => e2 (e1 x)
| ret y => e1.ret (e2.ret y)
| ret_f x => pmap e1.ret (e2.ret_f (e1 x)) *> e1.ret_f x
| sec y => e1.sec (e2.sec y)
| f_sec y => pmap e2 (e1.f_sec (e2.sec y)) *> e2.f_sec y

\func -o_Equiv {C : \Type} (e : Equiv) : Equiv {e.B -> C} {e.A -> C} (-o e) \cowith
| ret => -o e.sec
| ret_f g => path (\lam i x => g (e.f_sec x @ i))
| sec => -o e.ret
| f_sec g => path (\lam i x => g (e.ret_f x @ i))

\func o-_Equiv {C : \Type} (e : Equiv) : Equiv {C -> e.A} (e o-) \cowith
| ret => e.ret o-
| ret_f g => path (\lam i x => e.ret_f (g x) @ i)
| sec => e.sec o-
| f_sec g => path (\lam i x => e.f_sec (g x) @ i)

\func piEquiv {A : \Type} (B : A -> \Type) (f f' : \Pi (a : A) -> B a) : QEquiv \cowith
| A => f = f'
| B => \Pi (a : A) -> f a = f' a
| f p a => path ((p @ __) a)
| ret g => path (\lam i a => g a @ i)
| ret_f _ => idp
| f_sec _ => idp

\func sigmaEquiv {A : \Type} (B : A -> \Type) (p p' : \Sigma (a : A) (B a)) : QEquiv \cowith
| A => p = p'
| B => \Sigma (s : p.1 = p'.1) (transport B s p.2 = p'.2)
| f q => (pmap __.1 q, pmapd __.2 q)
| ret q => ext q
| ret_f q => Jl (\lam p'' q' => ext (pmap __.1 q', pmapd __.2 q') = q') idp q
| f_sec q =>
ext (idp, \case p'.1 \as p'1        , q.1 \as q1 : p.1 = p'1,
p'.2 \as p'2 : B p'1, q.2 \as q2 : transport B q1 p.2 = p'2
\return pmapd __.2 {p} {p'1, p'2} (ext (q1,q2)) = q2 \with {
| p'1, idp, p'2, idp => idp
})

\func piSigmaEquiv {A A' : \Type} (h : A -> A') (B : A' -> \Type)
: QEquiv {\Pi (a : A) -> B (h a)}
{\Sigma (g : A -> \Sigma (a' : A') (B a')) ((\lam a => (g a).1) = h)}
\cowith
| f g => (\lam a => (h a, g a), idp)
| ret p => \lam a => transport B (path ((p.2 @ __) a)) (p.1 a).2
| ret_f g => idp
| f_sec p => Jl (\lam (h' : A -> A') q => (\lam a => (h' a, transport B (path ((q @ __) a)) (p.1 a).2), idp)
= {\Sigma (g : A -> \Sigma (a' : A') (B a')) ((\lam a => (g a).1) = h')}
(p.1, q))
idp
p.2

\func piSigmaIdEquiv {A : \Type} (B : A -> \Type)
: QEquiv {\Pi (a : A) -> B a}
{\Sigma (g : A -> \Sigma (a : A) (B a)) ((\lam a => (g a).1) = id)}
=> piSigmaEquiv id B

\func emptyEquiv {A B : \Type} (Ae : A -> Empty) (Be : B -> Empty) : QEquiv {A} {B} \cowith
| f a => absurd (Ae a)
| ret b => absurd (Be b)
| ret_f a => absurd (Ae a)
| f_sec b => absurd (Be b)

-- # Embeddings and surjections

\record Embedding \extends Map {
| isEmb : \Pi (a a' : A) -> Retraction (pmap f {a} {a'})
\func pmap-isEquiv {a a' : A} : QEquiv (pmap f {a} {a'}) => pathEquiv (f __ = f __) (\lam {a} {a'} => isEmb a a')
} \where {
\use \level levelProp {A B : \Type} {f : A -> B} (e e' : Embedding f) : e = e'
=> path (\lam i => \new Embedding f (\lam a a' => Retraction.levelProp (e.pmap-isEquiv {a} {a'}) (e.isEmb a a') (e'.isEmb a a') @ i))

\func fromInjection {A : \Type} {B : \Set} {f : A -> B} (inj : \Pi {a a' : A} -> f a = f a' -> a = a') : Embedding f \cowith
| isEmb a a' => \new Retraction {
| sec => inj
| f_sec p => prop-pi {f a = f a'}
}

-- | The diagonal of an embedding is an equivalence
\lemma diag-equiv (e : Embedding) : Equiv {e.A} {\Sigma (a1 a2 : e.A) (e a1 = e a2)} (\lam a => (a, a, idp)) =>
\let | S => \Sigma (x : e.A) (\Sigma (y : e.A) (x = y))
| T => \Sigma (x y : e.A) (e x = e y)
| q => \new QEquiv {e.A} {S} (\lam x => (x,(x,idp))) {
| ret t => t.1
| ret_f x => idp
| f_sec t => pmap (\lam r => ((t.1,r) : S)) (Jl (\lam x p => (t.1,idp) = {\Sigma (x : e.A) (t.1 = x)} (x,p)) idp t.2.2)
}
| pe {a} {a'} : QEquiv (pmap e {a} {a'}) => e.pmap-isEquiv {a} {a'}
| s => \new QEquiv {S} {T} (\lam t => (t.1, t.2.1, pmap e t.2.2)) {
| ret t => (t.1, (t.2, pe.ret t.3))
| ret_f t => pmap (\lam r => ((t.1, (t.2.1, r)) : S)) (pe.ret_f t.2.2)
| f_sec t => pmap (\lam r => ((t.1, t.2, r) : T)) (pe.f_sec t.3)
}
\in transQEquiv q s

\lemma projection {A : \Type} (B : A -> \Prop) : Embedding {\Sigma (a : A) (B a)} __.1 \cowith
| isEmb p p' => \new Retraction {
| sec q => ext q
| f_sec => idpe
}

-- | If the fibers of a map are propositions, then the map is an embedding
\lemma fibers {A B : \Type} (f : A -> B) (p : \Pi (b : B) -> isProp (Fib f b)) : Embedding f \cowith
| isEmb a a' =>
\have e (q : f a = f a') => Fib.equiv (f a') (a,q) (a',idp) (p (f a') (a,q) (a',idp))
\in \new Retraction {
| sec q => (e q).1
| f_sec q => (e q).2
}

-- | The fibers of an embedding are propositions.
\lemma embeddingFiber-isProp (e : Embedding) (b : e.B) : isProp (Fib e b) => \lam x x' =>
\let | eq : Retraction (pmap e {x.1} {x'.1}) => e.isEmb x.1 x'.1
| fx=fx' => x.2 *> inv x'.2
\in Fib.ext b x x' (eq.sec fx=fx') (
pmap e (eq.sec fx=fx') *> x'.2 ==< pmap (*> x'.2) (eq.f_sec fx=fx') >==
fx=fx' *> x'.2                   ==< *>-assoc _ _ _ >==
x.2 *> inv x'.2 *> x'.2          ==< pmap (x.2 *>) (inv_*> _) >==
x.2                              qed
)
}

\func transEmbedding {A B C : \Type} (e1 : Embedding {A} {B}) (e2 : Embedding {B} {C}) : Embedding {A} {C} \cowith
| f a => e2 (e1 a)
| isEmb a a' => \new Retraction {
| sec p => sec {e1.isEmb a a'} (sec {e2.isEmb (e1 a) (e1 a')} p)
| f_sec p => pmap (pmap e2) (f_sec {e1.isEmb a a'} (sec {e2.isEmb (e1 a) (e1 a')} p)) *> f_sec {e2.isEmb (e1 a) (e1 a')} p
}

\func \infixr 1 >-> (A B : \Type) => Embedding {A} {B}

\record Surjection \extends Map
| isSurjMap (y : B) : ∃ (x : A) (f x = y)

\func \infixr 1 ->> (A B : \Type) => Surjection {A} {B}

\record ESEquiv \extends Embedding, Surjection, Equiv
| ret y => (aux \this isSurjMap y).1
| sec y => (aux \this isSurjMap y).1
| ret_f x => sec {isEmb _ _} (aux \this isSurjMap (f x)).2
| f_sec y => (aux \this isSurjMap y).2
\where {
\use \level levelProp {A B : \Type} {f : A -> B} (e e' : ESEquiv f) : e = e' =>
path (\lam i => \new ESEquiv { | Embedding  => Embedding.levelProp  e e' @ i
| Surjection => prop-isProp {Surjection f} e e' @ i })

\use \coerce fromEquiv (e : Equiv) : ESEquiv e.f \cowith
| isEmb a a' => pmapEquiv e {a} {a'}
| isSurjMap y => inP (e.sec y, e.f_sec y)

\lemma aux (e : Embedding) (s : \Pi (y : e.B) -> ∃ (x : e.A) (f x = y)) (y : e.B)
=> TruncP.remove (Embedding.embeddingFiber-isProp e y) (s y)
}