\import Equiv
\import Equiv.Fiber
\import Equiv.Univalence
\import Function
\import HLevel
\import Homotopy.Fibration
\import Homotopy.Localization.Accessible
\import Homotopy.Localization.Connected
\import Homotopy.Localization.Universe
\import Logic
\import Paths
\import Paths.Meta

\func isLocalEquiv {U : Universe} {A B : \hType} (f : A -> B) => \Pi (Z : Local) -> Equiv {B -> Z} {A -> Z} (-o f)

\module Extension \where {
-- | The type of extensions of {g} along {f}
\func ext {A B C : \hType} (f : A -> B) (g : A -> C) => Fib (-o f) g

\func ext-equiv {A B C : \hType} (f : A -> B) (g : A -> C) : QEquiv {ext f g} {\Pi (b : B) -> \Sigma (c : C) (\Pi (a : A) -> f a = b -> g a = c)} \cowith
| f p b => (p.1 b, \lam a fa=b => inv (path ((p.2 @ __) a)) *> pmap p.1 fa=b)
| ret K => ((K __).1, path (\lam i a => inv ((K (f a)).2 a idp) @ i))
| ret_f b => path (\lam j => (b.1, path (\lam i a => inv_inv (path ((b.2 @ __) a)) @ j @ i)))
| f_sec K =>
\have p (b : B) (a : A) (q : f a = b) =>
Jl (\lam b' q' => inv (inv ((K (f a)).2 a idp)) *> pmap (K __).1 q' = (K b').2 a q') (inv_inv ((K (f a)).2 a idp)) q
\in path (\lam i b => ((K b).1, p b __ __ @ i))

\lemma contr-equiv {A B C : \hType} (f : A -> B) (p : \Pi (g : A -> C) (b : B) -> Contr (\Sigma (c : C) (\Pi (a : A) -> f a = b -> g a = c)))
: Equiv {B -> C} {A -> C} (-o f)
=> contrFibers=>Equiv (\lam g => rewrite (QEquiv-to-= (ext-equiv f g)) (HLevels_-2-pi (\lam b => \Sigma (c : C) (\Pi (a : A) -> f a = b -> g a = c)) {0} (p g)))
}

\lemma connected_isLocalEquiv {U : Universe} {A B : \hType} (f : A -> B) (conn : isConnectedMap f) : isLocalEquiv f
=> \lam C => Extension.contr-equiv f (\lam g b =>
\let | G (x : Fib f b) => g x.1
| p c => \new QEquiv {(\lam _ => c) = G} {\Pi (a : A) -> f a = b -> g a = c} {
| f q a r => path ((inv q @ __) (a,r))
| ret h => inv (path (\lam i (x : Fib f b) => h x.1 x.2 @ i))
| ret_f q => inv_inv q
| f_sec h => path (\lam k a r => path (\lam i => (inv_inv (path (\lam j (x : Fib f b) => h x.1 x.2 @ j)) @ k @ i) (a,r)))
}
\in rewriteI (path (\lam i => \Sigma (c : C) (QEquiv-to-= (p c) @ i)))
(Equiv=>contrFibers (propExt.dir (nullTypeUniverse.localDesc (Fib f b) C) (conn b C)) G))

-- | A map between local types is a local equivalence if and only if it is an equivalence
\lemma localTypesEquiv {U : Universe} {A B : Local} (f : A -> B) : isLocalEquiv f = Equiv f
=> propExt (dir f) (\lam e C => -o_Equiv {C} e)
\where {
-- | A local equivalence between local types is an equivalence
\lemma dir {U : Universe} {A B : Local} (f : A -> B) (p : isLocalEquiv f) : Equiv f
=> \let | g => sec {p A} id
| g_f => f_sec {p A} id
| H => ret {p B}
\in \new QEquiv {
| ret => g
| ret_f a => path ((g_f @ __) a)
| f_sec b => path (\lam i => ((
f o g           ==< inv (ret_f {p B} (f o g)) >==
H (f o g o f) ==< pmap (\lam t => H (f o t)) g_f >==
H f               ==< ret_f {p B} id >==
id                qed) @ i) b)
}
}

\lemma localEquivMap {U : ReflUniverse} {A B : \hType} (f : A -> B) : isLocalEquiv f = Equiv (lmap f)
=> \have p (C : Local) : Equiv {LType B -> C} {LType A -> C} (-o (lmap f)) = Equiv {B -> C} {A -> C} (-o f)
=> TwoOutOfThree.parallelEquiv (-o (lmap f))
(-o f)
(local-univ {localization B} C)
(local-univ {localization A} C)
(\lam h => path (\lam i a => h (Localization.lift-prop (inL o f) a @ i)))
\in path (\lam i => \Pi (C : Local) -> inv (p C) @ i) *> localTypesEquiv (lmap f)
`