\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths.Meta
\import Set.Filter
\import Set.Subset
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.CoverSpace.StronglyComplete
\import Topology.RatherBelow
\import Topology.UniformSpace
\import Topology.UniformSpace.Complete (CompleteUniformSpace)
\open ClosurePrecoverSpace
\open StrongCompletion

\class StronglyCompleteUniformSpace \extends StronglyRegularUniformSpace, CompleteUniformSpace, StronglyCompleteCoverSpace

\func weaklyDense-uniform-lift {X : RegularPreuniformSpace} {Y : StronglyRegularUniformSpace} {Z : StronglyCompleteUniformSpace} (f : UniformMap X Y) (fd : f.IsWeaklyDenseUniformEmbedding) (g : UniformMap X Z) : UniformMap Y Z \cowith
  | CoverMap => weaklyDense-lift f (fd., f.embedding->coverEmbedding fd.) g
  | func-uniform Dc => uniform-refine (Y.<=<-regular $ fd. $ g.func-uniform $ Z.s<=<-regular Dc) \lam {V'} (inP (V, inP (U, inP (W', inP (W, DW, W'<=<W), p), q), V'<=<V)) =>
      inP (_, inP (W, DW, idp), \lam {y} V'y => <=<_<= (Z.weak-filter-point-elem W'<=<W \case <=<-inter (<=<-right (single_<= V'y) V'<=<V) \with {
        | inP (V'',y<=<V'',V''<=<V) => inP $ later (V'', V, rewrite p in q, V''<=<V, y<=<V'')
      }) idp)

\instance UniformStrongCompletion (X : StronglyRegularUniformSpace) : StronglyCompleteUniformSpace
  | StronglyCompleteCoverSpace => StrongCompletion X
  | isUniform D => ∃ (C : isUniform) (∀ {U : C} ∃ (V : D) (mkSet U ⊆ V))
  | uniform-cover (inP (C,Cu,p)) F =>
    \have | (inP (U,CU,FU)) => isCauchyFilter (X.makeCauchy Cu)
          | (inP (V,DV,q)) => p CU
    \in inP (V, DV, q FU)
  | uniform-top => inP (single top, uniform-top, \lam _ => inP (top, idp, \lam _ => ()))
  | uniform-refine (inP (E,Eu,g)) f => inP (E, Eu, \lam EU =>
      \have | (inP (V,CV,p)) => g EU
            | (inP (W,DW,q)) => f CV
      \in inP (W, DW, p <=∘ q))
  | uniform-inter (inP (C',C'u,f)) (inP (D',D'u,g)) => inP (_, uniform-inter C'u D'u, \lam {U} (inP (V',C'V',W',D'W',p)) => \case f C'V', g D'W' \with {
    | inP (V,CV,eV), inP (W,DW,eW) => inP (V ∧ W, inP (V, CV, W, DW, idp), rewrite p \lam {F} c => (eV $ filter-mono c meet-left, eW $ filter-mono c meet-right))
  })
  | uniform-strongly-star (inP (C',C'u,f)) => \case uniform-strongly-star C'u \with {
    | inP (D',D'u,g) => inP (\lam V => ∃ (V' : D') (V = mkSet V'), inP (D', D'u, \lam {V'} D'V' => inP (mkSet V', inP (V', D'V', idp), <=-refl)), \lam (inP (V',D'V',p)) => \case g D'V' \with {
      | inP (U',C'U',e) => \case f C'U' \with {
        | inP (U,CU,q) => inP (U, CU, \lam (inP (V'',D'V'',p')) => \case e D'V'' \with {
          | byLeft r => byLeft $ rewrite (p,p') \lam (F,(FV',FV'')) => isWeaklyProper {F} $ filter-mono (filter-meet FV' FV'') \lam {x} s => absurd $ r (x,s)
          | byRight r => byRight $ rewrite p' $ mkSet_<= r <=∘ q
        })
      }
    })
  }
  | uniform-cauchy => (\lam (inP (C',C'c,f)) => closure-map mkSet (\lam {F} => filter-top) mkSet_<= (\lam s => filter-meet s. s.) f $ uniform-cauchy. C'c,
                       closure-cauchy $ later \lam (inP (C',C'u,f)) => inP (C', X.makeCauchy C'u, f))
  \where {
    \lemma properUniform (Xp : X.IsProperUniform) : PreuniformSpace.IsProperUniform {UniformStrongCompletion X}
      => \lam (inP (D,Du,h)) => inP (_, Xp $ X.<=<-regular Du, \lam {U'} (inP (U, DU, U'<=<U), inP (x,U'x)) => \case h DU \with {
        | inP (V,CV,p) => inP (V, (CV, inP (pointSCF x, p $ <=<-right (single_<= U'x) U'<=<U)), mkSet_<= (<=<_<= U'<=<U) <=∘ p)
      })

    \lemma makeUniform {C : Set (Set X)} (Cu : isUniform C) : isUniform {UniformStrongCompletion X} \lam V => ∃ (U : C) (V = mkSet U)
      => inP (C, Cu, \lam CU => inP (_, inP (_, CU, idp), <=-refl))
  }

\func uniform-strongCompletion {X : StronglyRegularUniformSpace} : UniformMap X (UniformStrongCompletion X) \cowith
  | CoverMap => strongCompletion
  | func-uniform (inP (C,Cu,f)) => uniform-refine (X.<=<-regular Cu)
      \case __ \with {
        | inP (U',CU',U<=<U') => \case f CU' \with {
          | inP (V,DV,p) => inP (pointSCF ^-1 V, inP (V, DV, idp), \lam Ux => p $ <=<-right (single_<= Ux) U<=<U')
        }
      }
  \where {
    \lemma isDenseEmbedding : UniformMap.IsWeaklyDenseUniformEmbedding {uniform-strongCompletion {X}}
      => (strongCompletion.isDenseEmbedding., \lam {C} Cu => inP (C, Cu, \lam {U} CU => inP (mkSet U, inP (U, CU, <=<_<= __ idp), <=-refl)))
  }

\lemma cauchyFilter-uniform-char {X : PreuniformSpace} {F : SetFilter X} : ∀ {C : isCauchy} ∃ (U : C) (F U) <-> ∀ {C : isUniform} ∃ (U : C) (F U)
  => (\lam Fc Cu => Fc $ X.makeCauchy Cu, \lam f Cc => closure-filter F f (uniform-cauchy. Cc))

\lemma regularFilter-uniform-char {X : RegularPreuniformSpace} {F : CauchyFilter X} : ∀ {U : F.F} ∃ (V : Set X) (V <=< U) (F V) <-> ∀ {U : F.F} ∃ (V : Set X) (V <=* U) (F V)
  => (\lam Fr => RegularCauchyFilter.ratherBelow StarRatherBelow StarRatherBelow.<=<-left (\lam p => <=<_<= (<=*_<=< p)) X.<=*-cauchy-regular (\new RegularCauchyFilter { | CauchyFilter => F | isRegularFilter => Fr }), \lam f FU => TruncP.map (f FU) \lam (V,p,FV) => (V, <=*_<=< p, FV))