{- | The reflective universe of separated types is contructed in the following paper.
     J. Daniel Christensen, Morgan Opie, Egbert Rijke, and Luis Scoccola, Localization in Homotopy Type Theory, https://arxiv.org/pdf/1807.04155
 -}

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

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

\func ReflSeparated.{u} (U : ReflUniverse.{u}) : 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') = {\Type u} (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} {U : ReflUniverse.{u}} {A : \Type u} (a a' : A) : \Type u
      => LType (a = a')

    -- | The localization map for the type {A}.
    \func F.{u} {U : ReflUniverse.{u}} {A : \Type u} (a : A) : YImage S
      => YImage.dom-map a

    \func pathEquiv.{u} {U : ReflUniverse.{u}} {A : \Type u} (a a' : A) : (F a = F a') = LType (a = a') => Equiv_= $ =_Equiv
      \let | E => \Pi (x : A) -> Equiv (S a' x) (S a x)
           | emb => transEmbedding (piEmbedding \lam a'' => Equiv.toFunc-embedding {LType (a' = a'')} {LType (a = a'')})
                                   (Embedding.fromIsEquiv (localYoneda a' (\lam y => LType (a = y))))
      \in (F a = F a')                    ==< QEquiv_= 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_= typeUnivalence @ {_} {_} {Equiv (S a' x) (S a x)} i) >==
          E                               ==< Equiv_= (mkEquiv $ 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 $ mkEquiv $ inP idEquiv)
                                                              emb
                                                              (\lam p => Jl (\lam x p' => transport (\lam y => Equiv (S y x) (S a x)) p' (mkEquiv (inP idEquiv)) (lEta idp) = inL p') idp p)) >==
          (LType (a = a') : \Type u)      `qed

    \lemma separatedLocalization.{u} {U : Universe.{u}} {A B : \Type u} {f : A -> B} (fs : IsSurj f) (p : \Pi (a a' : A) -> \Sigma (P : Local (f a = f a')) (Localization (a = a') P))
      : \Sigma (L : Local {Separated U} B) (Localization {Separated U} A L f)
      => \have B-local (b b' : B) : isLocal (b = b') =>
                \case fs b, fs 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 fs b \with {
              | inP (a',q) => later rewriteI q (coe (\lam i => Contr (\Sigma (c : C) (\Pi (a : A) -> inv (Equiv_= $ mkEquiv ((p a a')..local-univ \new Local (g a = c) (C.local (g a) c))) @ i)))
                                                    (coe (\lam i => Contr (\Sigma (c : C) (inv (QEquiv_= (pi-contr-right a' (\lam x _ => g x = c))) @ i))) (lsigma (g a')) right) right)
            }) })
  }