\import Equiv
\import Equiv.Sigma
\import Equiv.Univalence
\import HLevel
\import Homotopy.Image
\import Homotopy.Localization.Equiv
\import Homotopy.Localization.Universe
\import Logic
\import Meta
\import Paths
\import Paths.Meta

\func Separated (U : Universe) : Universe \cowith
  | isLocal Z => \Pi (z z' : Z) -> isLocal (z = z')

\func ReflSeparated (U : ReflUniverse \lp) : ReflUniverse \cowith
  | Universe => Separated U
  | localization A =>
    \have | p (a a' : A) : Local (F a = F a') => transport (Local __) (inv (pathEquiv a a')) (LType (a = a'))
          | q (a a' : A) : LType (a = a') = {\hType \lp} (F a = F a') => inv (pathEquiv a a')
          | r (a a' : A) : Localization (a = a') (p a a') =>
             coe (\lam i => Localization (a = a') (\new Local (q a a' @ i) (prop-dpi (\lam j => isLocal (q a a' @ j)) (local {LType (a = a')}) (local {p a a'}) @ i)))
                 (localization (a = a')) right
    \in (separatedLocalization YImage.dom-map-surj (\lam a a' => (p a a', r a a'))).
  \where {
    \func S {U : ReflUniverse} {A : \hType} (a a' : A) : \hType => LType (a = a')

    \func F {U : ReflUniverse} {A : \hType} (a : A) => YImage.dom-map {_} {_} {S} a

    \func pathEquiv {U : ReflUniverse} {A : \hType} (a a' : A) : (F a = F a') = LType (a = a') => Equiv-to-= (=-to-Equiv (
      \let | E => \Pi (x : A) -> Equiv {S a' x} {S a x}
           | emb => transEmbedding (\new Embedding {E} (\lam h x => Equiv.f {h x}) (\lam e e' =>
                                          \new Retraction { | sec p => path (\lam i x => Equiv.equals (path ((p @ __) x)) @ i) | f_sec => idpe }))
                                   (ESEquiv.fromEquiv (localYoneda a' (\lam y => LType (a = y))))
      \in (F a = F a')                    ==< QEquiv-to-= YImage.cod-map-emb.pmap-isEquiv >==
          (S a = S a')                    ==< path-sym (S a) (S a') >==
          (S a' = S a)                    ==< path (iso {S a' = S a} (\lam p x => path ((p @ __) x)) (\lam h => path (\lam i x => h x @ i)) idpe idpe) >==
          (\Pi (x : A) -> S a' x = S a x) ==< path (\lam i => \Pi (x : A) -> QEquiv-to-= univalence @ {_} {_} {Equiv {S a' x} {S a x}} i) >==
          E                               ==< Equiv-to-= (localizationFactorEmbedding
                                                              (piLocal (\lam x => equivLocal (LType (a' = x)) (LType (a = x))))
                                                              (\lam p x => transport (\lam y => Equiv {S y x} {S a x}) p idEquiv)
                                                              emb
                                                              (\lam p => Jl (\lam x p' => transport (\lam y => Equiv {S y x} {S a x}) p' idEquiv (lEta idp) = inL p') idp p)) >==
          (LType (a = a') : \hType)       `qed))

    \lemma separatedLocalization {U : Universe} (f : Surjection) (p : \Pi (a a' : f.A) -> \Sigma (P : Local (f a = f a')) (Localization (a = a') P))
      : \Sigma (L : Local {Separated U} f.B) (Localization {Separated U} f.A L f)
      => \have B-local (b b' : f.B) : isLocal (b = b') =>
                \case f.isSurjMap b, f.isSurjMap b' \with {
                  | inP (a,q), inP (a',q') => transport2 _ q q' (local {(p a a').})
                }
         \in (\new Local { | local => B-local }, \new Localization { | local-univ C => Extension.contr-equiv f (\lam g b =>
            \case f.isSurjMap b \with {
              | inP (a',q) => later rewriteI q (coe (\lam i => Contr (\Sigma (c : C) (\Pi (a : f.A) -> inv (Equiv-to-= (local-univ {(p a a').} (\new Local (g a = c) (local {C} (g a) c)))) @ i)))
                                                    (coe (\lam i => Contr (\Sigma (c : C) (inv (QEquiv-to-= (pi-contr-right a' (\lam x _ => g x = c))) @ i))) (lsigma (g a')) right) right)
            }) })
  }