{- | We follow the following paper:
     Graham Manuell, Uniform locales and their constructive aspects, 2021, https://arxiv.org/abs/2106.00678
 -}

\import Algebra.Meta
\import Category
\import Category.Factorization
\import Category.Meta
\import Category.Subcat
\import Equiv
\import Function (IsSurj)
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.Lattice.CompleteLattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.SetHom
\import Set.Set
\import Topology.Locale
\import Topology.Locale.HausdorffLocale
\import Topology.Locale.LocaleCat
\import Topology.Locale.PreorderSite
\open Locale
\open Nucleus
\open MeetSemilattice
\open FrameHom
\open CompleteLattice
\open Cover

\func star {L : Locale} (x : L) (U : L -> \Prop) => Join (\lam y => \Sigma (U y) (IsPositive (x ∧ y)))
  \where {
    \lemma star-monotone {L : Locale} {x y : L} (x<=y : x <= y) {V U : L -> \Prop} (V<=U : ∀ {x : V} (U x)) : star x V <= star y U
      => Join-univ \lam j => Join-cond (V<=U j., positive_<= j. $ MeetSemilattice.meet-monotone x<=y <=-refl)

    \lemma star_<= {L : Locale} {x y : L} (x<=y : x <= y) (U : L -> \Prop) : star x U <= star y U
      => star-monotone x<=y (\lam u => u)

    \lemma star-refl {L : PreuniformLocale} {x : L} {U : L -> \Prop} (uU : isUniform U) : x <= star x U
      => meet-univ <=-refl (top-univ <=∘ isCovering uU) <=∘ Join-ldistr>= <=∘ L.SJoin-univ \lam {b} Ub =>
          IsOvert_IJoin L.uniform-overt <=∘ L.IJoin-univ \lam xb>0 => meet-right <=∘ Join-cond (Ub,xb>0)
  }

\func nucleus-star {L : Locale} (j : Nucleus L) (U : L -> \Prop) => Join (\lam y => \Sigma (U y) (j.locale.IsPositive (j y, nucleus-join>=)))
  \where {
    \lemma star_open {L : Locale} (a : L) (U : L -> \Prop) : nucleus-star (open a) U = star a U
      => pmap Join $ ext \lam x =>
          \let a-->x : (open a).Subtype => (a L.--> x, (open a).nucleus-join>=)
          \in propExt
            (\lam (Ux,a-->x>0) => (Ux, positive_<= ((open_IsPositive {L} {a} {a-->x}). a-->x>0) $ meet-univ meet-right L.<=-eval))
            (\lam (Ux,ax>0) => (Ux, (open_IsPositive {L} {a} {a-->x}). $ positive_<= ax>0 $ meet-univ (L.<=-curry $ meet-left <=∘ meet-right) meet-left))
  }

\class PreuniformLocale \extends Locale
  | uniform-overt : IsOvert
  | isUniform : (E -> \Prop) -> \Prop
  | isCovering {U : E -> \Prop} : isUniform U -> top <= Join U
  | isDownset {U : E -> \Prop} {x y : E} : isUniform U -> U y -> x <= y -> U x
  | top-uniform : isUniform (\lam _ => \Sigma)
  | meet-uniform {U V : E -> \Prop} : isUniform U -> isUniform V -> isUniform (\lam x => \Sigma (U x) (V x))
  | <=-uniform {U V : E -> \Prop} : isUniform U -> (\Pi {x : E} -> U x -> V x) -> (\Pi {x y : E} -> V y -> x <= y -> V x) -> isUniform V
  | star-uniform {U : E -> \Prop} : isUniform U -> ∃ (V : isUniform) ∀ {x : V} (U (star x V))
  \where {
    \lemma dClosure {L M : Preorder} {f : L -> M} {U : L -> \Prop} {x y : M} (p : ∃ (z : L) (U z) (y <= f z)) (x<=y : x <= y) : ∃ (z : L) (U z) (x <= f z) \elim p
      | inP (z,Uz,y<=fz) => inP (z, Uz, x<=y <=∘ y<=fz)
  }

\open PreuniformLocale(dClosure)

\record UniformHom \extends FrameHom {
  \override Dom : PreuniformLocale
  \override Cod : PreuniformLocale
  | func-uniform {U : Dom -> \Prop} : isUniform U -> isUniform (\lam y => ∃ (x : Dom) (U x) (y <= func x))
} \where {
  \protected \func id {L : PreuniformLocale} : UniformHom L L \cowith
    | FrameHom => FrameHom.id
    | func-uniform => <=-uniform __ (\lam {x} Ux => inP (x,Ux,<=-refl)) dClosure

  \protected \func compose \alias \infixl  ∘ {X Y Z : PreuniformLocale} (g : UniformHom Y Z) (f : UniformHom X Y) : UniformHom X Z \cowith
    | FrameHom => g FrameHom.∘ f
    | func-uniform uU => <=-uniform (func-uniform {g} (func-uniform {f} uU))
        (\lam {x} (inP (y, inP (z,Uz,y<=fz), x<=gy)) => inP (z, Uz, x<=gy <=∘ func-<= y<=fz)) dClosure
}

\record UniformEmbedding \extends UniformHom {
  | isEmbedding : IsSurj func
  | isUniformEmbedding {U : Cod -> \Prop} : isUniform U -> ∃ (V : isUniform) ∀ {x} (V x -> U (func x))

  \lemma direct-uniform {U : Cod -> \Prop} : isUniform U -> isUniform (\lam x => ∃ (y : Cod) (U y) (x <= direct y))
    => \case isUniformEmbedding __ \with {
      | inP (V,uV,V<=Uf) => <=-uniform uV (\lam {x} Vx => inP (func x, V<=Uf Vx, direct-unit)) (\lam (inP (z,Uz,p)) q => inP (z, Uz, q <=∘ p))
    }
} \where {
    \func comp {L M K : PreuniformLocale} (g : UniformEmbedding M K) (f : UniformEmbedding L M) : UniformEmbedding L K \cowith
      | UniformHom => g UniformHom.∘ f
      | isEmbedding => IsSurj.comp f.isEmbedding g.isEmbedding
      | isUniformEmbedding => \lam uU =>
          \have | (inP (V,uV,cV)) => g.isUniformEmbedding uU
                | (inP (W,uW,cW)) => f.isUniformEmbedding uV
          \in inP (W, uW, \lam Wx => cV (cW Wx))
  }

\func \infix  <=u {L : PreuniformLocale} (a b : L) => ∃ (U : L -> \Prop) (isUniform U) (star a U <= b)
  \where {
    \lemma func-<=u (f : UniformHom) {a b : f.Dom} (p : a <=u b) : f a <=u f b \elim p
      | inP (U,uU,a*U<=b) => inP (_, func-uniform uU, Join-univ \lam {x} (inP (y,Uy,x<=fy), fa*x>0) =>
          x<=fy <=∘ func-<= (Join-cond (Uy, func_positive $ positive_<= fa*x>0 $ meet-monotone <=-refl x<=fy <=∘ func-meet>=)) <=∘ func-<= a*U<=b)

    \lemma adjoint (f : UniformHom) {a : f.Dom} {b : f.Cod} (p : a <=u f.direct b) : f a <=u b
      => <=u-trans-left (f a) (func-<=u f p) direct-counit

    \lemma dense {L : PreuniformLocale} {a c : L} (p : a <=u c) : ∃ (b : L) (a <=u b) (b <=u c) \elim p
      | inP (U,uU,a*U<=c) => \case star-uniform uU \with {
        | inP (V,uV,x*V<-U) => inP (star a V, inP (V,uV,<=-refl), inP (V, uV, Join-univ (\lam {y} (Vy,a*V^b>0) => star.star-refl uV <=∘ Join-cond (x*V<-U Vy, dense.meet_star-comm L.uniform-overt $ rewrite meet-comm a*V^b>0)) <=∘ a*U<=c))
      }
      \where
        \lemma meet_star-comm {L : Locale} (o : L.IsOvert) {a b : L} {U : L -> \Prop} (p : IsPositive (a ∧ star b U)) : IsPositive (b ∧ star a U)
          => \case positive_SJoin o (rewrite Join-ldistr in p) \with {
            | inP (c,(Uc,b^c>0),a^c>0) => rewrite Join-ldistr $ positive_SJoin.conv $ inP (c, (Uc, a^c>0), b^c>0)
          }

    \lemma uniform-refine {L : PreuniformLocale} {U : L -> \Prop} (uU : isUniform U) : isUniform (\lam b => ∃ (a : L) (U a) (b <=u a))
      => \case star-uniform uU \with {
        | inP (V,uV,x*V<-U) => <=-uniform uV (\lam {x} Vx => inP (star x V, x*V<-U Vx, inP (V,uV,<=-refl))) (\lam {x} {y} (inP (a,Ua,y<=ua)) x<=y => inP (a, Ua, <=u-trans-right x<=y y<=ua))
      }
  }

\lemma <=u-trans-left {L : PreuniformLocale} (a : L) {b c : L} (p : a <=u b) (b<=c : b <= c) : a <=u c \elim p
  | inP (U,uU,a*U<=b) => inP (U, uU, a*U<=b <=∘ b<=c)

\lemma <=u-trans-right {L : PreuniformLocale} {a b c : L} (a<=b : a <= b) (p : b <=u c) : a <=u c \elim p
  | inP (U,uU,b*U<=c) => inP (U, uU, star.star_<= a<=b U <=∘ b*U<=c)

\lemma <=u_meet {L : PreuniformLocale} {a a' b b' : L} (p : a <=u a') (q : b <=u b') : a ∧ b <=u a' ∧ b' \elim p, q
  | inP (U,uU,a*U<=a'), inP (V,uV,b*V<=b') => inP (_, meet-uniform uU uV, meet-univ
    (star.star-monotone meet-left (later __.) <=∘ a*U<=a')
    (star.star-monotone meet-right (later __.) <=∘ b*V<=b'))

\lemma <=u_top {L : PreuniformLocale} {a : L} : a <=u top
  => inP (_, top-uniform, top-univ)

\lemma <=u_<= {L : PreuniformLocale} {a b : L} (p : a <=u b) : a <= b \elim p
  | inP (U,uU,a*U<=b) => star.star-refl uU <=∘ a*U<=b

\class UniformLocale \extends PreuniformLocale {
  | isAdmissible (b : E) : b <= Join (<=u b)

  \func IsComplete => ∃ (g : UniformHom \this (Completion \this)) (completion UniformHom.∘ g = UniformHom.id) (g UniformHom.∘ completion = UniformHom.id)
} \where {
    \open NucleusFrame

    \lemma star_wclosure {L : PreuniformLocale} {j : Nucleus L} {U : L -> \Prop} (uU : isUniform U) : nucleus-star j.map.wclosed-image U = nucleus-star j U
      => pmap Join $ ext \lam x => propExt
          (\lam (Ux,p) => (Ux, \lam jx<=P => p $ unfolds $ SMeet-univ (later \lam c => SMeet-cond (unfold \lam {Q} {y} jy<=Q => nucleus-unit <=∘ jy<=Q <=∘ =_<= locale_pHat) <=∘ c (unfold $ nucleus-join>= <=∘ jx<=P)) <=∘ =_<= (inv j.map.wclosed-image.locale_pHat)))
          (\lam (Ux,p) => (Ux, \lam Mx<=P => p $ unfolds $ nucleus-univ (j.map.wclosed-image.nucleus-unit <=∘ Mx<=P <=∘ =_<= j.map.wclosed-image.locale_pHat <=∘ wclosure_<=) <=∘ =_<= (inv j.locale_pHat)))

    \lemma top<=star {L : PreuniformLocale} {j : Nucleus L} (o : j.locale.IsOvert) {U : L -> \Prop} (uU : isUniform U) : j <= open (nucleus-star j U)
      => nucleus<=open $ isCovering uU <=∘ Join-univ \lam {w} Uw => j.nucleus-unit <=∘ IsOvert_IJoin o {j w, nucleus-join>=} <=∘ j.locale.IJoin-univ {_} {_} {_, nucleus-join>=} \lam jw>0 => nucleus-<= $ Join-cond (Uw,jw>0)

    \lemma wclosure<=nucleus-star {L : PreuniformLocale} {j : Nucleus L} (o : j.locale.IsOvert) {U : L -> \Prop} (uU : isUniform U) : j.map.wclosed-image <= open (nucleus-star j U)
      => top<=star (sdense_overt {<=-map j.map.wclosed-image j wclosure_<=} wclosure-sdense o) uU <=∘ =_<= (pmap open $ star_wclosure uU)

    \lemma wclosure<=star {L : PreuniformLocale} {a : L} {U : L -> \Prop} (uU : isUniform U) : (open a).map.wclosed-image <= open (star a U)
      => wclosure<=nucleus-star (open_IsOvert uniform-overt) uU <=∘ =_<= (pmap open $ nucleus-star.star_open a U)
  }

\lemma uniform=>wregular {L : UniformLocale} : L.IsWeaklyRegularLocale
  => \lam x => L.isAdmissible x <=∘ Join-univ \lam {b} (inP (U,uU,b*U<=x)) => Join-cond $
        unfold (<=<w) $ UniformLocale.wclosure<=star uU <=∘ NucleusFrame.open_<= b*U<=x

\func PreuniformCat.{u} : Cat PreuniformLocale.{u} \cowith
  | Hom => UniformHom
  | id => UniformHom.id
  | o => UniformHom.∘
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam {X} {S1} {S2} h1 h2 => exts UniformLocale {
    | <= x y => ext (h1.func-<=, h2.func-<=)
    | meet x y => h1.func-meet
    | top => h1.func-top
    | Join C => <=-antisymmetric (S1.Join-univ \lam Cw => h2.func-<= (S2.Join-cond Cw))
                                 (h2.func-<= $ S2.Join-univ \lam Cw => h1.func-<= (S1.Join-cond Cw))
    | isUniform U => ext (\lam uU => uniform-lem (h1.func-uniform uU) (\lam Uy x<=y => isDownset uU Uy (h2.func-<= x<=y)),
                          \lam uU => uniform-lem (h2.func-uniform uU) (\lam Uy x<=y => isDownset uU Uy (h1.func-<= x<=y)))
  }
  \where {
    \lemma uniform-lem {L : PreuniformLocale} {U : L -> \Prop}
                       (u : isUniform (\lam y => ∃ (x : L) (U x) (y <= x)))
                       (d : \Pi {x y : L} -> U y -> x <= y -> U x)
      : isUniform U
      => <=-uniform u (\lam {x} (inP (y,Uy,x<=y)) => d Uy x<=y) d
  }

\func UniformCat.{u} : Cat UniformLocale.{u} => subCat {PreuniformCat.{u}} (\new Embedding {
  | f L => L
  | isEmb L M => \new Retraction {L = {UniformLocale.{u}} M} {
    | sec p => path (\lam i => \new UniformLocale {
      | PreuniformLocale => p i
      | isAdmissible => prop-dpi (\Pi (b : p __) -> b <= Join (<=u b)) L.isAdmissible M.isAdmissible i
    })
    | f_sec => idpe
  }
})

\func CompletionSite (L : UniformLocale) : PreorderSite \cowith
  | Preorder => L
  | isBasicCover a U => OneOf (
    U = \lam x => \Sigma (IsPositive a) (x <= a),
    ∃ (V : isUniform) (U = SetIm (a ∧) V),
    U = (<=u a)
  )
  | basic-cover-stable a<=b {U} => \case \elim U, \elim __ \with {
    | _, inP (, idp) => inP (_, inP (,idp), \lam s => inP (_, (positive_<= s. a<=b, s. <=∘ a<=b), <=-refl), __.)
    | _, inP (, inP (V,Vu,idp)) => inP (_, inP (, inP (V,Vu,idp)), SetIm-elim \lam {v} Vv => inP $ later (_, SetIm-con Vv, L.meet-monotone a<=b <=-refl), SetIm-elim \lam _ => meet-left)
    | _, inP (, idp) => inP (_, inP (,idp), \lam x<=<a => inP (_, <=u-trans-left _ x<=<a a<=b, <=-refl), \lam {t} => <=u_<=)
  }
  \where {
    \lemma subcanonical : (CompletionSite L).IsSubcanonical
      => \lam {x} {U} x<=U {y} => \case \elim U, \elim x<=U \with {
        | _, inP (, idp) => \lam h => IsOvert_IJoin uniform-overt <=∘ IJoin-univ \lam x>0 => h $ later (x>0, <=-refl)
        | _, inP (, inP (V,Vu,idp)) => \lam h => L.meet-univ <=-refl (top-univ <=∘ isCovering Vu) <=∘ Join-ldistr>= <=∘ SJoin-univ \lam Va => h (SetIm-con Va)
        | _, inP (, idp) => \lam h => isAdmissible x <=∘ L.Join-univ h
      }

    \lemma Cover1_<= {x y : L} (c : Cover {CompletionSite L} x (single y)) : x <= y
      => PreorderSite.subcanonical-cover1 subcanonical c
  }

\open CompletionSite
\open SiteLocale

\func CompletionLocale (L : UniformLocale) => SiteLocale (CompletionSite L)

\func completionLocale {L : UniformLocale} : LocaleHom L (CompletionLocale L)
  => LocaleSite.adjointMap completionLocale.presentation
  \where {
    \func presentation {L : UniformLocale} : PreorderSiteHom (CompletionSite L) (LocaleSite L) \cowith
      | func x => x
      | func-<= p => p
      | func-basicCover {x} {C} x<=C => \case \elim C, \elim x<=C \with {
        | _, inP (, idp) => IsOvert_IJoin uniform-overt <=∘ IJoin-univ \lam x>0 => Join-cond $ SetIm-con $ later (x>0,<=-refl)
        | _, inP (, inP (V,Vu,idp)) => meet-univ <=-refl (top-univ <=∘ isCovering Vu) <=∘ Join-ldistr>= <=∘ SJoin-univ \lam Va => Join-cond $ SetIm-con (SetIm-con Va)
        | _, inP (, idp) => isAdmissible x <=∘ Join-univ \lam w<=<x => Join-cond (SetIm-con w<=<x)
      }
      | func-flat-top {u} => cover-refl (TSetIm-con u)
      | func-flat-meet u<=x u<=y => cover-refl $ SetIm-con (u<=x,u<=y)

    \lemma sdense {L : UniformLocale} : IsStronglyDense {completionLocale {L}}
      => sdense-site {_} {_} {completionLocale.presentation} \lam x<=Q => later $ cover-trans (inP (,idp)) \lam (x>0,_) => cover-refl (x>0 x<=Q)

    \lemma completion_embed {L : UniformLocale} {a : L} : completionLocale (embed a) = a
      => <=-antisymmetric (SJoin-univ \lam {b} b<=a => PreorderSite.subcanonical-cover1 subcanonical b<=a) (SJoin-cond $ cover-refl idp)
  }

\func Completion (L : UniformLocale) : UniformLocale \cowith
  | Locale => CompletionLocale L
  | uniform-overt => sdense_overt {completionLocale} completionLocale.sdense uniform-overt
  | isUniform (V : CompletionLocale L -> \Prop) : \Prop => ∃ (U : L -> \Prop) (L.isUniform U) (\Pi {a : L} -> U a -> V (embed a)) (\Pi {x y : CompletionLocale L} -> V y -> x <= y -> V x)
  | isCovering {C} (inP (U,uU,U<=C,dC)) {x} _ => cover-trans (inP (, inP (U, uU, idp))) $ SetIm-elim \lam {a} Ua => cover-refl $ inP $ later (embed a, U<=C Ua, cover-inj meet-right idp)
  | isDownset (inP (U,uU,U<=V,dV)) Vy x<=y => dV Vy x<=y
  | top-uniform => inP (\lam _ => \Sigma, top-uniform, \lam _ => (), \lam _ _ => ())
  | meet-uniform (inP (U,uU,lU,dU)) (inP (V,uV,lV,dV)) =>
      inP (\lam x => \Sigma (U x) (V x), meet-uniform uU uV, \lam p => (lU p., lV p.), \lam p x<=y => (dU p. x<=y, dV p. x<=y))
  | <=-uniform (inP (U,uU,lU,dU)) U<=V dV => inP (U, uU, \lam Ua => U<=V (lU Ua), dV)
  | star-uniform {U} (inP (U',uU,lU,dU)) => TruncP.map (star-uniform uU) \lam (V',uV',sr) =>
    \let (V,uV,q) => make-covering V' uV'
    \in (V, uV, \lam (inP (x',V'x',x<=x')) => dU (lU $ sr V'x') $ star.star_<= x<=x' V <=∘ q x')
  | isAdmissible U {x} Ux =>
    \have embed_<=u {a b : L} (a<=b : a <=u b) : embed a <=u {\this} embed b
            => TruncP.map a<=b \lam (U,uU,a*U<=b) =>
                \have (V,uV,q) => make-covering U uU
                \in (V, uV, q a <=∘ embed-univ (cover-inj a*U<=b idp))
    \in cover-trans (inP (,idp)) \lam {y} y<=<x => cover-refl $ inP (embed y, <=u-trans-left {\this} (embed y) (embed_<=u y<=<x) $ embed-univ Ux, cover-refl idp)
  \where {
    \func make-covering {L : UniformLocale} (U : L -> \Prop) (uU : L.isUniform U)
      : \Sigma (V : CompletionLocale L -> \Prop) (isUniform V) (\Pi (a : L) -> star {CompletionLocale L} (embed a) V <= embed (star a U))
      => (\lam s => ∃ (x : L) (U x) (s <= embed x),
          inP (U, uU, \lam {a} Ua => inP (a,Ua,<=-refl), dClosure), \lam a => Join-univ \lam {V} (inP (x,Ux,V<=x), aV>0) =>
            V<=x <=∘ embed-univ (cover-inj (L.Join-cond (Ux, positive_<= (sdense_positive completionLocale.sdense aV>0) $ Join-univ $
              SetIm-elim $ later \lam {b} (b<=a,Vb) => meet-univ (CompletionSite.Cover1_<= b<=a) (CompletionSite.Cover1_<= $ V<=x Vb))) idp))
  }

\func completion {L : UniformLocale} : UniformEmbedding (Completion L) L \cowith
  | FrameHom => completionLocale
  | func-uniform (inP (V,uV,V<=U,dV)) => <=-uniform uV (\lam {x} Vx => inP (embed x, V<=U Vx, SJoin-cond $ cover-refl idp)) dClosure
  | isEmbedding a => inP (embed a, completionLocale.completion_embed)
  | isUniformEmbedding {U} uU => inP (\lam x => ∃ (a : L) (U a) (x <= embed a),
      inP (U, uU, \lam {a} Ua => inP (a,Ua,<=-refl), \lam (inP (a,Ua,y<=a)) x<=y => inP (a, Ua, x<=y <=∘ y<=a)),
      \lam {x} (inP (a,Ua,x<=a)) => isDownset uU (transportInv U completionLocale.completion_embed Ua) (func-<= {completionLocale} x<=a))
  \where {
    \lemma isMono.{u} {L M : UniformLocale.{u}} {f g : UniformHom M (Completion L)} (p : completion UniformHom.∘ f = completion UniformHom.∘ g) : f = g
      => ext $ path (\lam i => func {WFS.left-epi {LocaleCartesianPrecat} sdense_wclosed_ofs {_} {Completion L} completion completionLocale.sdense {M} (wregular_wHausdorff uniform=>wregular) p i})
  }

\sfunc completion-factor {L M : UniformLocale} (f : UniformEmbedding M L) (sd : f.IsStronglyDense) : \Sigma (g : UniformHom (Completion L) M) (f UniformHom.∘ g = completion)
  => (factor f sd, isFactor f sd)
  \where {
    \func presentation {L M : UniformLocale} (f : UniformEmbedding M L) (sd : f.IsStronglyDense) : PreorderSiteHom (CompletionSite L) (LocaleSite M) \cowith
      | func => f.direct
      | func-<= => direct-<=
      | func-basicCover {x} {C} => \case \elim C, \elim __ \with {
        | _, inP (, idp) => IsOvert_IJoin uniform-overt <=∘ IJoin-univ \lam f_x>0 => Join-cond $ SetIm-con $ later (direct_positive sd f_x>0, <=-refl)
        | _, inP (, inP (U,uU,idp)) =>
          \have (inP (V, uV, V<=Uf)) => f.isUniformEmbedding uU
          \in meet-univ <=-refl (top-univ <=∘ isCovering uV) <=∘ Join-ldistr>= <=∘ SJoin-univ \lam Va =>
              meet-monotone <=-refl f.direct-unit <=∘ inv direct-meet =<= Join-cond (SetIm-con $ SetIm-con $ V<=Uf Va)
        | _, inP (, idp) => isAdmissible _ <=∘ Join-univ \lam w<=f_x => f.direct-unit <=∘ Join-cond (SetIm-con $ <=u.adjoint f w<=f_x)
      }
      | func-flat-top {u} => cover-basic $ f.direct-unit <=∘ Join-cond (TSetIm-con (f u))
      | func-flat-meet u<=x u<=y => cover-basic $ meet-univ u<=x u<=y <=∘ =_<= (inv f.direct-meet) <=∘ Join-cond (SetIm-con (meet-left,meet-right))

    \func factor {L M : UniformLocale} (f : UniformEmbedding M L) (sd : f.IsStronglyDense) : UniformHom (Completion L) M \cowith
      | FrameHom => LocaleSite.adjointMap (presentation f sd)
      | func-uniform (inP (V, uV, V<=U, Ud)) => <=-uniform (f.direct-uniform uV)
        (\lam (inP (y,Vy,x<=f_y)) => inP (embed y, V<=U Vy, x<=f_y <=∘ SJoin-cond (cover-refl idp)))
        (\lam (inP (z,Uz,p)) x<=y => inP (z, Uz, x<=y <=∘ p))

    \lemma isFactor {L M : UniformLocale} (f : UniformEmbedding M L) (sd : f.IsStronglyDense) : f UniformHom.∘ factor f sd = completion
      => exts \lam U => SiteLocale.func-equality {_} {_} {f FrameHom.∘ factor f sd} \lam x => f.func-SJoin *> unfold (pmap (SJoin __ _) $ ext $ surjective-split f.isEmbedding)
  }

\lemma completion-isComplete.{u} (L : UniformLocale.{u}) : (Completion L).IsComplete
  => \have | (g,fact) => completion-factor (UniformEmbedding.comp completion completion) (sdense-comp completion completionLocale.sdense completion completionLocale.sdense)
           | cg=id => completion.isMono {_} {_} {_} {UniformHom.id} fact
     \in inP (g, cg=id, completion.isMono {_} {_} {_} {UniformHom.id} $ pmap (UniformHom.∘ _) cg=id)

\func completion-functor {L M : UniformLocale} (f : UniformHom M L) : UniformHom (Completion M) (Completion L) \cowith
  | FrameHom => LocaleSite.adjointMap (presentation f)
  | func-uniform => \case __ \with {
    | inP (V,uV,V<=U,Ud) => inP (_, f.func-uniform $ <=u.uniform-refine uV, \lam {a} (inP (x, inP (z,Vz,x<=uz), a<=fx)) =>
      inP (embed z, V<=U Vz, embed-univ $ cover-inj a<=fx $ inP (_, SetIm-con $ cover-refl idp, cover-refl $ inP (x, x<=uz, idp))),
        \lam {x} {y} (inP (z,Uz,y<=fz)) x<=y => inP (z, Uz, x<=y <=∘ y<=fz))
  }
  \where {
    \open Cover

    \func presentation {L M : UniformLocale} (f : UniformHom M L) : PreorderSiteHom (CompletionSite M) (LocaleSite (Completion L)) \cowith
      | func a => closure \lam c => ∃ (b : M) (b <=u a) (c = f b)
      | func-<= x<=y => closure-univ $ later \lam {_} (inP (b,b<=<x,idp)) => cover-refl $ inP (b, <=u-trans-left b b<=<x x<=y, idp)
      | func-basicCover {x} {C} => \case \elim C, \elim __ \with {
        | _, inP (, idp) => cover-trans* __ \lam {_} (inP (y,y<=<x,idp)) => cover-trans (inP (,idp)) \lam {z} (fy>0,z<fy) =>
          cover-inj z<fy $ inP (_, SetIm-con (positive_<= (func_positive fy>0) $ <=u_<= y<=<x, <=-refl), cover-refl $ inP (y,y<=<x,idp))
        | _, inP (, inP (V,uV,idp)) => cover-trans* __ \lam {_} (inP (y,y<=<x,idp)) => cover-trans (inP (, inP (_, f.func-uniform $ <=u.uniform-refine uV, idp))) $ SetIm-elim $ later
          \lam (inP (b, inP (v,Vv,b<=<v), a<=fb)) => cover-refl $ inP (_, SetIm-con $ SetIm-con Vv, cover-inj (meet-monotone <=-refl a<=fb <=∘ func-meet>=) $ inP (y ∧ b, <=u_meet y<=<x b<=<v, idp))
        | _, inP (, idp) => cover-sub __ \lam {_} (inP (z,z<=<x,idp)) => \case <=u.dense z<=<x \with {
          | inP (y,z<=<y,y<=<x) => inP (_, SetIm-con y<=<x, cover-refl $ inP (z,z<=<y,idp))
        }
      }
      | func-flat-top => cover-basic \lam {x} _ => unfolds $ cover-left top-univ $ cover-refl $ inP (_, TSetIm-con top, cover-refl $ inP (top, <=u_top, inv func-top))
      | func-flat-meet {x} {y} u<=x u<=y => cover-inj (meet-univ u<=x u<=y) $ inP ((x ∧ y, (meet-left, meet-right)), <=-antisymmetric
        (closure-univ $ later \lam {_} (inP (b,b<=<xy,idp)) => cover-refl $ inP (_, inP (b, <=u-trans-left b b<=<xy meet-left, idp), _, inP (b, <=u-trans-left b b<=<xy meet-right, idp), <=-refl, <=-refl))
        (closure-univ $ later \lam {c} (inP (_, inP (a,a<=<x,idp), _, inP (b,b<=<y,idp), c<=fa, c<=fb)) => cover-inj (L.meet-univ c<=fa c<=fb <=∘ func-meet>=) $ inP (a ∧ b, <=u_meet a<=<x b<=<y, idp)) *> inv closure_embed
      )
  }

\lemma completion-natural {L M : UniformLocale} {f : UniformHom M L} : completion UniformHom.∘ completion-functor f = f UniformHom.∘ completion
  => exts \lam S => <=-antisymmetric
      (SJoin-univ \lam Ca => LocaleSite.locale_cover (completionLocale.presentation.func-Cover Ca) <=∘ Join-univ (SetIm-elim $ later \lam {x} (inP (_, inP ((b,Sb),idp), Cx)) => LocaleSite.locale_cover (completionLocale.presentation.func-Cover Cx) <=∘ Join-univ (SetIm-elim $ later \lam {_} (inP (c,c<=<b,idp)) => f.func-<= $ <=u_<= c<=<b) <=∘ SJoin-cond Sb))
      (SJoin-univ \lam {a} Sa => func-<= (isAdmissible a) <=∘ func-Join>= <=∘ SJoin-univ \lam {b} b<=ua => later $ SJoin-cond $ unfolds $ cover-refl $ inP (_, SetIm-con Sa, cover-refl $ inP (b, b<=ua, idp)))
      *> inv f.func-SJoin

\lemma completion-isReflector.{u} {L M : UniformLocale.{u}} (Mc : M.IsComplete)
  : IsEquiv {UniformHom M (Completion L)} {UniformHom M L} (\lam g => completion UniformHom.∘ g)
  \elim Mc
  | inP Mc => inP \new QEquiv {
    | ret f => completion-functor f UniformHom.∘ Mc.
    | ret_f g => completion.isMono $ pmap (UniformHom.∘ _) completion-natural *> pmap (completion UniformHom.∘ g UniformHom.∘) Mc.
    | f_sec f => pmap (UniformHom.∘ _) completion-natural *> pmap (f UniformHom.∘) Mc.
  }