\import Function
\import Function.Meta
\import HLevel
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set.Filter
\import Set.Subset
\import Topology.CoverSpace
\import Topology.RatherBelow
\import Topology.TopSpace
\open Bounded(top)

\record CauchyFilter (S : CoverSpace) \extends ProperFilter
  | X => S
  | isCauchyFilter {C : Set (Set S)} : isCauchy C -> ∃ (U : C) (F U)

\record CauchyMap \extends ContMap {
  \override Dom : CoverSpace
  \override Cod : CoverSpace

  | func-cauchy (F : CauchyFilter Dom) : CauchyFilter Cod { | ProperFilter => ProperFilter-map func F }

  \default func-cont Uo => cauchy-open. \lam {x} Ufx => \case isCauchyFilter {func-cauchy (pointCF x)} $ cauchy-open. Uo Ufx \with {
    | inP (V,h,fx<=<V) => cauchy-subset (unfolds in fx<=<V) $ later \lam {W} g Wx {y} Wy => h (<=<_<= fx<=<V idp) $ g (x, (idp, Wx)) Wy
  }
} \where {
  \lemma fromContMap {X : CompleteCoverSpace} {Y : CoverSpace} (f : ContMap X Y) : CauchyMap X Y f \cowith
    | func-cauchy F => \new CauchyFilter {
      | isCauchyFilter Cc => \case Y.cauchy-regular-cover Cc (f $ X.filter-point F) \with {
        | inP (U,CU,fx<=<U) => inP (U, CU, X.filter-point-sub $ <=<-cont fx<=<U)
      }
    }
}

\record CoverMap \extends PrecoverMap, CauchyMap {
  \override Dom : CoverSpace
  \override Cod : CoverSpace

  | func-cauchy F => \new CauchyFilter {
    | isCauchyFilter Cc => \case isCauchyFilter {F} (func-cover Cc) \with {
      | inP (U, inP (V, CV, p), FU) => inP (V, CV, transport F p FU)
    }
  }

  \lemma embedding->contEmbedding (e : IsEmbedding) : ContMap.IsEmbedding
    => ContMap.embedding-char. \lam Uo {x} Ux => \case CoverSpace.cauchy-regular-cover (e $ cauchy-open. Uo Ux) (func x) \with {
      | inP (V, inP (W,h,p), fx<=<V) => inP (_, CoverSpace.interior {_} {V}, fx<=<V, \lam {y} fy<=<V => h (p $ <=<_<= fx<=<V idp) (p $ <=<_<= fy<=<V idp))
    }
} \where {
  \func id {X : CoverSpace} : CoverMap X X \cowith
    | PrecoverMap => PrecoverMap.id

  \func compose \alias \infixl  ∘ {X Y Z : CoverSpace} (g : CoverMap Y Z) (f : CoverMap X Y) : CoverMap X Z \cowith
    | PrecoverMap => g PrecoverMap.∘ f

  \func const {Y X : CoverSpace} (x : X) : CoverMap Y X \cowith
    | PrecoverMap => PrecoverMap.const x

  \lemma closure-univ {X : \Set} {A : Set (Set X) -> \Prop} {S : CoverSpace X} {Y : CoverSpace} (AS : \Pi {C : Set (Set X)} -> isCauchy C -> ClosurePrecoverSpace.Closure A C) (f : Y -> X) (Ap : ∀ {C : A} (isCauchy \lam U => ∃ (V : Set X) (C V) (U = f ^-1 V))) : CoverMap Y S f \cowith
    | func-cover Cc => ClosurePrecoverSpace.closure-univ-cover Ap (AS Cc)

  \lemma id-denseEmbedding {X : CoverSpace} : IsDenseEmbedding {id {X}}
    => PrecoverMap.id-denseEmbedding
}

\instance CauchyFilterPoset (S : CoverSpace) : Poset (CauchyFilter S)
  | <= F G => F ⊆ G
  | <=-refl c => c
  | <=-transitive f g c => g (f c)
  | <=-antisymmetric f g => exts \lam U => ext (f,g)

\type \infix  CF~ {S : CoverSpace} (F G : CauchyFilter S) : \Prop
  => \Pi {C : Set (Set S)} -> isCauchy C -> ∃ (U : C) (\Sigma (F U) (G U))

\lemma CF~-sym {S : CoverSpace} {F G : CauchyFilter S} (p : F CF~ G) : G CF~ F
  => \case p __ \with {
    | inP (U,CU,(FU,GU)) => inP (U,CU,(GU,FU))
  }

\func CF~_meet {S : CoverSpace} {F G : CauchyFilter S} (p : F CF~ G) : CauchyFilter S \cowith
  | ProperFilter => F ∧ {ProperFilterSemilattice S} G
  | isCauchyFilter => p

\lemma CF~_<= {S : CoverSpace} {F G : CauchyFilter S} (p : F ⊆ G) : F CF~ G
  => \lam c => \case isCauchyFilter c \with {
    | inP (U,CU,FU) => inP (U, CU, (FU, p FU))
  }

\lemma CF~_<=< {S : CoverSpace} {F G : CauchyFilter S} (F~G : F CF~ G) {U V : Set S} (p : U <=< V) (FU : F U) : G V
  => \case F~G p \with {
    | inP (W, f, (FW, GW)) => filter-mono (\case isProper $ filter-meet FU FW \with {
      | inP s => f s
    }) GW
  }

\instance CauchyFilterEquivalence (S : CoverSpace) : Equivalence (CauchyFilter S)
  | ~ => CF~
  | ~-transitive p q c => \case p (isRegular c) \with {
    | inP (U, inP (V, CV, U<=<V), (FU, GU)) => inP (V, CV, (filter-mono (<=<_<= U<=<V) FU, CF~_<=< q U<=<V GU))
  }
  | ~-reflexive c => \case isCauchyFilter c \with {
    | inP (U,CU,FU) => inP (U,CU,(FU,FU))
  }
  | ~-symmetric => CF~-sym

\record RegularCauchyFilter \extends CauchyFilter
  | isRegularFilter {U : Set S} : F U -> ∃ (V : Set S) (V <=< U) (F V)
  \where {
    \lemma Reg_CF~_<= {X : CoverSpace} {F : RegularCauchyFilter X} {G : CauchyFilter X} (p : F CF~ G) : F ⊆ G
      => \case isRegularFilter __ \with {
        | inP (V,V<=<U,FV) => CF~_<=< p V<=<U FV
      }

    \lemma equality {X : CoverSpace} {F G : RegularCauchyFilter X} (p : F CF~ G) : F = G
      => exts \lam U => ext (Reg_CF~_<= p, Reg_CF~_<= (CF~-sym p))

    \lemma ratherBelow {X : CoverSpace} (R : Set X -> Set X -> \Prop) (Rl : \Pi {U V W : Set X} -> R U V -> V ⊆ W -> R U W) (Rs : \Pi {U V : Set X} -> R V U -> V ⊆ U) (Xr : ∀ {C : isCauchy} (isCauchy \lam V => ∃ (U : C) (R V U))) (F : RegularCauchyFilter X) {U : Set X} (FU : F U) : ∃ (V : Set X) (R V U) (F V)
      => \case isRegularFilter FU \with {
        | inP (V,V<=<U,FV) => \case F.isCauchyFilter $ Xr V<=<U \with {
          | inP (W', inP (W,h,RW'W), FW') => \case isProper (filter-meet FV FW') \with {
            | inP (y,(Vy,W'y)) => inP (W', Rl RW'W \lam Wx => h (y, (Vy, Rs RW'W W'y)) Wx, FW')
          }
        }
      }
  }

-- | The unique regular Cauchy filter equivalent to the given one.
\func regCF {X : CoverSpace} (F : CauchyFilter X) : RegularCauchyFilter X \cowith
  | F U => \Pi {G : CauchyFilter X} -> G ⊆ F -> G U
  | filter-mono p q c => filter-mono p (q c)
  | filter-top _ => filter-top
  | filter-meet p q c => filter-meet (p c) (q c)
  | isProper p => F.isProper (p <=-refl)
  | isCauchyFilter c => \case F.isCauchyFilter (isRegular c) \with {
    | inP (U, inP (V, CV, U<=<V), FU) => inP (V, CV, \lam p => CF~_<=< (CF~-sym $ CF~_<= p) U<=<V FU)
  }
  | isRegularFilter c =>
    \case c {\new CauchyFilter {
                   | F U => ∃ (V W : Set X) (W <=< V) (V <=< U) (F W)
                   | filter-mono p (inP (V,W,W<=<V,V<=<U,FW)) => inP (V, W, W<=<V, <=<-left V<=<U p, FW)
                   | filter-top => inP (top, top, <=<_top, <=<_top, filter-top)
                   | filter-meet (inP (V,W,W<=<V,V<=<U,FW)) (inP (V',W',W'<=<V',V'<=<U',FW')) => inP (V ∧ V', W ∧ W', <=<_meet W<=<V W'<=<V', <=<_meet V<=<U V'<=<U', filter-meet FW FW')
                   | isProper (inP (V,W,W<=<V,V<=<U,FW)) => TruncP.map (isProper FW) \lam (x,Wx) => (x, <=<_<= V<=<U (<=<_<= W<=<V Wx))
                   | isCauchyFilter Cc => \case F.isCauchyFilter $ isRegular $ isRegular Cc \with {
                     | inP (W, inP (V, inP (U, CU, V<=<U), W<=<V), FW) => inP (U, CU, inP (V, W, W<=<V, V<=<U, FW))
                   }
                 }} (\lam {U} (inP (V,W,W<=<V,V<=<U,FW)) => filter-mono (<=<_<= W<=<V <=∘ <=<_<= V<=<U) FW) \with {
      | inP (V,W,W<=<V,V<=<U,FW) => inP (V, V<=<U, \lam p => CF~_<=< (CF~-sym $ CF~_<= p) W<=<V FW)
    }

\lemma regCF_<= {S : CoverSpace} {F : CauchyFilter S} : regCF F ⊆ F
  => \lam u => u <=-refl

\open RatherBelow

\func pointCF {S : CoverSpace} (x : S) : RegularCauchyFilter S \cowith
  | F U => single x <=< U
  | filter-mono p q => <=<-left q p
  | filter-top => <=<_top
  | filter-meet p q => <=<-right (meet-univ <=-refl <=-refl) (<=<_meet p q)
  | isProper p => inP (x, <=<_<= p idp)
  | isCauchyFilter c => S.cauchy-regular-cover c x
  | isRegularFilter p => \case S.cauchy-regular-cover (isRegular $ unfolds in p) x \with {
    | inP (V, inP (W, f, V<=<W), x<=<V) => inP (V, <=<-left V<=<W $ f (x, (idp, <=<_<= V<=<W $ <=<_<= x<=<V idp)), x<=<V)
  }

\class SeparatedCoverSpace \extends CoverSpace, HausdorffTopSpace
  | isSeparatedCoverSpace {x y : E} : (\Pi {C : Set (Set E)} -> isCauchy C -> ∃ (U : C) (\Sigma (U x) (U y))) -> x = y
  | isHausdorff p => isSeparatedCoverSpace (separated-char   p)
  \where {
    \lemma separated-char {S : CoverSpace} {x y : S} : TFAE (
    {- 0 -} pointCF x ⊆ pointCF y,
    {- 1 -} pointCF x CF~ pointCF y,
    {- 2 -} pointCF x = pointCF y,
    {- 3 -} \Pi {U : Set S} -> single x <=< U <-> single y <=< U,
    {- 4 -} \Pi {U : Set S} -> single x <=< U -> U y,
    {- 5 -} \Pi {U V : Set S} -> single x <=< U -> single y <=< V -> ∃ (U ∧ V),
    {- 6 -} ∀ {U V : isOpen} (U x) (V y) ∃ (U ∧ V),
    {- 7 -} \Pi {C : Set (Set S)} -> isCauchy C -> ∃ (U : C) (\Sigma (U x) (U y))
    ) => TFAE.cycle (
      CF~_<= {S},
      RegularCauchyFilter.equality {S},
      \lam p {U} => <->_=. $ path \lam i => RegularCauchyFilter.F {p i} U,
      \lam f p => <=<_<= (f. p) idp,
      \lam f p q => inP (y, (f p, <=<_<= q idp)),
      \lam f Uo Vo Ux Vy => f (open-char. Uo Ux) (open-char. Vo Vy),
      \lam f Cc => \have | (inP (_, inP (U', inP (U,CU,U'<=<U), idp), x<=<U')) => cauchy-cover (cauchy-open-cover $ isRegular Cc) x
                         | (inP (_, inP (V,h,idp), y<=<V)) => cauchy-cover (cauchy-open-cover (unfolds in U'<=<U)) y
                         | (inP (x',(x'<=<U,x'<=<V))) => f interior interior x<=<U' y<=<V
                   \in inP (U, CU, (<=<_<= U'<=<U (<=<_<= x<=<U' idp), h (x', (<=<_<= x'<=<U idp, <=<_<= x'<=<V idp)) (<=<_<= y<=<V idp))),
      \lam f {U} p => \case f (isRegular p) \with {
        | inP (V, inP (W,g,V<=<W), (Vx,Vy)) => <=<-left (<=<-right (single_<= Vy) V<=<W) $ g (x, (idp, <=<_<= V<=<W Vx))
      })
  }

\lemma embedding-inj {X : SeparatedCoverSpace} {Y : PrecoverSpace} {f : PrecoverMap X Y} (fe : f.IsEmbedding) : isInj f
  => \lam {x} {y} p => isSeparatedCoverSpace \lam Cc => \case cauchy-cover (fe Cc) (f y) \with {
    | inP (V, inP (U,CU,q), Vfy) => inP (U, CU, (q $ unfolds $ rewrite p Vfy, q Vfy))
  }

\func IsCompleteCoverSpace (S : CoverSpace) => \Pi (F : RegularCauchyFilter S) -> ∃ (x : S) (pointCF x ⊆ F)
  \where {
    \lemma cauchyFilterToPoint (Sc : IsCompleteCoverSpace S) (F : CauchyFilter S) : ∃ (x : S) (pointCF x ⊆ F)
      => \case Sc (regCF F) \with {
        | inP (x,p) => inP (x, p <=∘ regCF_<=)
      }
  }

\class CompleteCoverSpace \extends SeparatedCoverSpace {
  | isComplete : IsCompleteCoverSpace \this

  \protected \lemma filter-point-unique (F : CauchyFilter \this) : isProp (\Sigma (x : E) (pointCF x ⊆ F))
    => \lam s t => ext $ isSeparatedCoverSpace $ SeparatedCoverSpace.separated-char   $ ~-transitive {_} {_} {F} (CF~_<= {_} {_} {F} s.) $ ~-symmetric (CF~_<= {_} {pointCF t.} t.)

  \protected \lemma filter-point-pair (F : CauchyFilter \this) : \Sigma (x : E) (pointCF x ⊆ F) \level filter-point-unique F
    => \case isComplete (regCF F) \with {
      | inP (x,p) => (x, p <=∘ \lam u => u <=-refl)
    }

  \sfunc filter-point (F : CauchyFilter \this) : E
    => (filter-point-pair F).

  \lemma filter-point-sub {F : CauchyFilter \this} : pointCF (filter-point F) ⊆ F
    => rewrite (\peval filter-point F) (filter-point-pair F).

  \lemma filter-point-elem {F : CauchyFilter \this} {U V : Set E} (p : V <=< U) (FV : F V) : single (filter-point F) <=< U
    => CF~_<=< (~-symmetric {_} {pointCF (filter-point F)} {F} $ CF~_<= {_} {pointCF (filter-point F)} filter-point-sub) p FV

  \lemma filter-point-char {F : CauchyFilter \this} {U : Set E} : single (filter-point F) <=< U <-> ∃ (V : Set E) (V <=< U) (F V)
    => (\lam p => \case <=<-inter p \with {
          | inP (V,q,V<=<U) => inP (V, V<=<U, filter-point-sub q)
        }, \lam (inP (V,p,FV)) => filter-point-elem p FV)
}

\lemma func-cauchy_<= {X Y : CoverSpace} {f : CoverMap X Y} (F G : CauchyFilter X) (p : F ⊆ G) : f.func-cauchy F ⊆ f.func-cauchy G
  => p __

\func dense-filter-lift {X Y : CoverSpace} (f : CoverMap X Y) (fd : f.IsDenseEmbedding) (F : CauchyFilter Y) : CauchyFilter X \cowith
  | F U => ∃ (V' V : Set Y) (f ^-1 V ⊆ U) (V' <=< V) (F V')
  | filter-mono U<=U' (inP (V',V,p,V'<=<V,FV')) => inP (V', V, p <=∘ U<=U', V'<=<V, FV')
  | filter-top => inP (top, top, \lam _ => (), <=<_top, filter-top)
  | filter-meet (inP (U',U,p,U'<=<U,FU')) (inP (V',V,q,V'<=<V,FV')) => inP (U' ∧ V', U ∧ V, MeetSemilattice.meet-monotone p q, <=<_meet U'<=<U V'<=<V, filter-meet FU' FV')
  | isProper (inP (V',V,p,V'<=<V,FV')) => \case F.isProper FV' \with {
    | inP (y,V'y) => \case dense-char. fd. (<=<-right (single_<= V'y) V'<=<V) \with {
      | inP (x,Vfx) => inP (x, p Vfx)
    }
  }
  | isCauchyFilter Cc => \case F.isCauchyFilter $ isRegular $ fd. Cc \with {
    | inP (V', inP (V, inP (U, CU, p), V'<=<V), FV') => inP (U, CU, inP (V', V, p, V'<=<V, FV'))
  }
  \where {
    \lemma map-equiv (fd : f.IsDenseEmbedding) : f.func-cauchy (dense-filter-lift f fd F) CF~ F
      => \lam {C} Cc => \case isCauchyFilter (isRegular Cc) \with {
        | inP (V', inP (V, CV, V'<=<V), FV') => inP (V, CV, (inP (V', V, <=-refl, V'<=<V, FV'), filter-mono (<=<_<= V'<=<V) FV'))
      }
  }

\func dense-cauchy-lift {X Y : CoverSpace} {Z : CompleteCoverSpace} (f : CoverMap X Y) (fd : f.IsDenseEmbedding) (g : CauchyMap X Z) : CauchyMap Y Z \cowith
  | func y => Z.filter-point $ g.func-cauchy $ dense-filter-lift f fd (pointCF y)
  | func-cauchy F => \new CauchyFilter {
    | isCauchyFilter Cc => \case isCauchyFilter {g.func-cauchy $ dense-filter-lift f fd F} (isRegular Cc) \with {
      | inP (U', inP (U,CU,U'<=<U), inP (V',V,p,V'<=<V,FV')) => inP (U, CU, filter-mono (\lam {y} V'y => <=<_<= (CompleteCoverSpace.filter-point-elem U'<=<U \case <=<-inter $ <=<-right (single_<= V'y) V'<=<V \with {
        | inP (V'',y<=<V'',V''<=<V) => inP $ later (V'', V, p, V''<=<V, y<=<V'')
      }) idp) FV')
    }
  }

\func dense-lift {X Y : CoverSpace} {Z : CompleteCoverSpace} (f : CoverMap X Y) (fd : f.IsDenseEmbedding) (g : CoverMap X Z) : CoverMap Y Z \cowith
  | CauchyMap => dense-cauchy-lift f fd g
  | func-cover Dc => cauchy-refine (isRegular $ fd. $ g.func-cover $ isRegular 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.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)

\lemma dense-lift-char {X Y : CoverSpace} {Z : CompleteCoverSpace} {f : CoverMap X Y} (fd : f.IsDenseEmbedding) {g : CoverMap X Z} (x : X) : dense-lift f fd g (f x) = g x
  => isSeparatedCoverSpace $ SeparatedCoverSpace.separated-char   $ later \case CompleteCoverSpace.filter-point-sub __ \with {
    | inP (V',V,p,V'<=<V,fx<=<V') => p $ <=<_<= V'<=<V $ <=<_<= fx<=<V' idp
  }

\lemma dense-lift-neighborhood {X Y : CoverSpace} {Z : CompleteCoverSpace} {f : CoverMap X Y} (fd : f.IsDenseEmbedding) {g : CoverMap X Z} (y : Y) (W : Set Z)
  : single (dense-lift f fd g y) <=< W <-> ∃ (W' : Set Z) (W' <=< W) (V : Set Y) (f ^-1 V ⊆ g ^-1 W') (single y <=< V)
  => <->trans Z.filter-point-char $ later (\lam (inP (W', W'<=<W, inP (V',V,p,V'<=<V,y<=<V'))) => inP (W', W'<=<W, V, p, <=<-right (<=<_<= y<=<V') V'<=<V),
                                           \lam (inP (W',W'<=<W,V,p,y<=<V)) => \case <=<-inter y<=<V \with {
                                             | inP (V',y<=<V',V'<=<V) => inP (W', W'<=<W, inP (V', V, p, V'<=<V, y<=<V'))
                                           })

\open CompleteCoverSpace

\lemma dense-lift-natural {X : CoverSpace} {Y Z : CompleteCoverSpace} {f : CoverMap X Y} (fd : f.IsDenseEmbedding) {g : CoverMap X Z} (F : CauchyFilter X)
  : dense-lift f fd g (Y.filter-point $ f.func-cauchy F) = Z.filter-point (g.func-cauchy F)
  => isSeparatedCoverSpace $ SeparatedCoverSpace.separated-char   \lam {U} c => \case (dense-lift-neighborhood fd (Y.filter-point $ f.func-cauchy F) _). c \with {
    | inP (U',U'<=<U,V,p,q) => filter-point-elem U'<=<U $ filter-mono p $ later (filter-point-sub q)
  }

\lemma dense-complete {X Y : CoverSpace} {f : CoverMap X Y} (fd : f.IsDenseEmbedding) (p : \Pi (F : RegularCauchyFilter X) -> ∃ (y : Y) (pointCF y ⊆ f.func-cauchy F)) : IsCompleteCoverSpace Y
  => \lam F => \case p $ regCF $ dense-filter-lift f fd F \with {
    | inP (y,q) => inP (y, RegularCauchyFilter.Reg_CF~_<= {_} {pointCF y} $ ~-transitive {_} {pointCF y} (CF~_<= {_} {pointCF y} $ q <=∘ func-cauchy_<= (regCF $ dense-filter-lift f fd F) (dense-filter-lift f fd F) \lam u => u <=-refl) $ dense-filter-lift.map-equiv fd)
  }

\instance Completion (X : CoverSpace) : CompleteCoverSpace (RegularCauchyFilter X)
  | CoverSpace => coverSpace
  | isSeparatedCoverSpace p => RegularCauchyFilter.equality \lam Cc => \case p (makeCover Cc) \with {
    | inP (_, inP (U,CU,idp), r) => inP (U,CU,r)
  }
  | isComplete => dense-complete completion.isDenseEmbedding \lam F => inP (F, completion.dense-aux {_} {F} __)
  \where {
    \func mkSet (U : Set X) : Set (RegularCauchyFilter X)
      => \lam F => F U

    \lemma mkSet_<= {U V : Set X} (p : U ⊆ V) : mkSet U ⊆ mkSet V
      => \lam {F} => filter-mono p

    \lemma mkSet-open {U : Set X} (Uo : isOpen U) : isOpen {Completion X} (mkSet U)
      => (PrecoverSpace.open-char {Completion X}). $ \lam {F} FU => \case isRegularFilter FU \with {
        | inP (V,V<=<U,FV) => inP (_, V<=<U, \lam {W} g => inP (mkSet W, \lam (_,(idp,FW)) => mkSet_<= \case isProper (filter-meet FV FW) \with {
          | inP s => g s
        }, <=-refl))
      }

    \lemma pointCF_^-1_<=< {F : RegularCauchyFilter X} {U : Set (RegularCauchyFilter X)} (p : single F <=< {Completion X} U) : F (pointCF ^-1 U) \elim p
      | inP (C,Cc,h) => \case F.isCauchyFilter (isRegular Cc) \with {
        | inP (U', inP (U,CU,U'<=<U), FU') => \case h CU \with {
          | inP (V,g,q) => filter-mono (\lam U'x => g (F, (idp, q $ filter-mono (<=<_<= U'<=<U) FU')) $ q $ <=<-right (single_<= U'x) U'<=<U) FU'
        }
      }

    \lemma mkSet_<=<-point {F : RegularCauchyFilter X} {U : Set X} : single F <=< {Completion X} mkSet U <-> F U
      => (\lam p => filter-mono (<=<_<= __ idp) (pointCF_^-1_<=< p), \lam FU => \case isRegularFilter FU \with {
        | inP (V,V<=<U,FV) => inP (_, V<=<U, \lam {W} g => inP (mkSet W, \lam (_,(idp,FW)) => mkSet_<= $ \case isProper (filter-meet FV FW) \with {
          | inP s => g s
        }, <=-refl))
      })

    \func isCCauchy (D : Set (Set (RegularCauchyFilter X)))
      => ∃ (C : X.isCauchy) (∀ {U : C} ∃ (V : D) (mkSet U ⊆ V))

    \lemma makeCover {C : Set (Set X)} (Cc : isCauchy C) : isCCauchy \lam V => ∃ (U : C) (V = mkSet U)
      => inP (C, Cc, \lam {U} CU => inP (mkSet U, inP (U,CU,idp), <=-refl))

    \func coverSpace : CoverSpace (RegularCauchyFilter X) \cowith
      | isCauchy => isCCauchy
      | cauchy-cover {D} (inP (C,Cc,p)) F =>
        \have | (inP (U,CU,FU)) => isCauchyFilter Cc
              | (inP (V,DV,q)) => p CU
        \in inP (V, DV, q FU)
      | cauchy-top => inP (single top, cauchy-top, \lam _ => inP (top, idp, \lam _ => ()))
      | cauchy-refine (inP (E,Ec,g)) f => inP (E, Ec, \lam EU =>
          \have | (inP (V,CV,p)) => g EU
                | (inP (W,DW,q)) => f CV
          \in inP (W, DW, p <=∘ q))
      | cauchy-glue {C} (inP (C',C'c,f)) {D} Dc => inP (_, cauchy-glue C'c {\lam U' V' => ∃ (U : C) (V : D U) (mkSet U' ⊆ U) (mkSet V' ⊆ V)} \lam {U'} C'U' =>
          \have | (inP (U,CU,U'<=U)) => f C'U'
                | (inP (D',D'c,g)) => Dc CU
          \in cauchy-refine D'c \lam {V'} D'V' => \case g D'V' \with {
            | inP (V,DV,V'<=V) => inP (V', inP (U, CU, V, DV, U'<=U, V'<=V), <=-refl)
          }, \lam {W'} (inP (U', V', C'U', inP (U, CU, V, DV, U'<=U, V'<=V), W'=U'V')) => inP (U ∧ V, inP (U, V, CU, DV, idp), rewrite W'=U'V' \lam {F} FU'V' => (U'<=U $ filter-mono meet-left FU'V', V'<=V $ filter-mono meet-right FU'V')))
      | isRegular {D} (inP (C,Cc,f)) =>
        \have <=<_mkFilters {U' U : Set X} (p : U' <=< U) : mkSet U' <=< mkSet U
              => unfolds $ inP (_, p, \lam {W} g => inP (mkSet W, \lam (F,(FU',FW)) => \case isProper (filter-meet FU' FW) \with {
                   | inP s => mkSet_<= (g s)
                 }, <=-refl))
        \in inP (_, isRegular Cc, \lam {U'} (inP (U,CU,U'<=<U)) => \case f CU \with {
          | inP (V,DV,U<=V) => inP (mkSet U', inP (V, DV, <=<-left (<=<_mkFilters U'<=<U) U<=V), <=-refl)
        })
  }

\func completion {S : CoverSpace} : CoverMap S Completion.coverSpace \cowith
  | func => pointCF
  | func-cover (inP (C,Cc,f)) => cauchy-refine (isRegular Cc)
      \case __ \with {
        | inP (U',CU',U<=<U') => \case f CU' \with {
          | inP (V,DV,p) => inP (pointCF ^-1 V, inP (V, DV, idp), \lam Ux => p $ <=<-right (single_<= Ux) U<=<U')
        }
      }
  \where {
    \protected \lemma dense-aux {F : RegularCauchyFilter S} {V : Set (RegularCauchyFilter S)} (r : single F <=< {Completion.coverSpace} V) : F \lam x => V (completion x) \elim r
      | inP (C,Cc,f) =>
        \have | (inP (U', inP (U, CU, U'<=<U), FU')) => isCauchyFilter {F} (isRegular Cc)
              | (inP (W,g,U<=W)) => f CU
        \in filter-mono (\lam U'x => g (F, (idp, U<=W $ filter-mono (<=<_<= U'<=<U) FU')) $ U<=W $ <=<-right (single_<= U'x) U'<=<U) FU'

    \lemma isDenseEmbedding : completion.IsDenseEmbedding
      => (dense-char. \lam r => isProper (dense-aux r), \lam {C} Cc => inP (C, Cc, \lam {U} CU => inP (Completion.mkSet U, inP (U, CU, <=<_<= __ idp), <=-refl)))
  }

\func completion-lift {X : CoverSpace} {Z : CompleteCoverSpace} (g : CoverMap X Z) : PrecoverMap (Completion X) Z
  => dense-lift completion completion.isDenseEmbedding g

\lemma completion-lift-char {X : CoverSpace} {Z : CompleteCoverSpace} {g : CoverMap X Z} (x : X) : completion-lift g (pointCF x) = g x
  => dense-lift-char completion.isDenseEmbedding x

\lemma completion-lift-unique {X : CoverSpace} {Z : SeparatedCoverSpace} (g h : PrecoverMap (Completion X) Z) (p : \Pi (x : X) -> g (pointCF x) = h (pointCF x)) (y : Completion X) : g y = h y
  => dense-lift-unique completion completion.isDenseEmbedding. g h p y

\lemma completion-lift-neighborhood {X : CoverSpace} {Z : CompleteCoverSpace} (g : CoverMap X Z) (y : Completion X) (W : Set Z)
  : single (completion-lift g y) <=< W <-> ∃ (W' : Set Z) (W' <=< W) (V : Set X) (y V) (V ⊆ g ^-1 W')
  => <->trans (dense-lift-neighborhood completion.isDenseEmbedding y W) $ later
      (\lam (inP (W',W'<=<W,V,p,y<=<V)) => inP (W', W'<=<W, pointCF ^-1 V, Completion.pointCF_^-1_<=< y<=<V, p),
       \lam (inP (W',W'<=<W,V,yV,p)) => inP (W', W'<=<W, Completion.mkSet V, (\lam x<=<V => <=<_<= x<=<V idp) <=∘ p, Completion.mkSet_<=<-point. yV))

\lemma completion-lift-natural {X : CoverSpace} {Z : CompleteCoverSpace} {g : CoverMap X Z} (F : CauchyFilter X)
  : completion-lift g (CompleteCoverSpace.filter-point $ completion.func-cauchy F) = CompleteCoverSpace.filter-point (g.func-cauchy F)
  => dense-lift-natural completion.isDenseEmbedding F

\lemma complete-char {X : CoverSpace} : TFAE (
    {- 0 -} CompleteCoverSpace { | CoverSpace => X },
    {- 1 -} ∃ (g : PrecoverMap (Completion X) X) (\Pi (x : X) -> g (pointCF x) = x),
    {- 2 -} ∃ (g : PrecoverMap (Completion X) X) (\Pi (x : X) -> g (pointCF x) = x) (\Pi (y : Completion X) -> pointCF (g y) = y)
  ) => TFAE.cycle (
    \lam c => inP (completion-lift {_} {c} CoverMap.id, completion-lift-char),
    TruncP.map __ \lam (g,p) => (g, p, completion-lift-unique (completion PrecoverMap.∘ g) PrecoverMap.id \lam x => pmap pointCF (p x)),
    \lam (inP (g,p,q)) => \new CompleteCoverSpace {
      | isSeparatedCoverSpace {x} {y} c => inv (p x) *> pmap g (SeparatedCoverSpace.separated-char   c) *> p y
      | isComplete F => inP (g F, transportInv {RegularCauchyFilter X} (`⊆ F) (q F) <=-refl)
    })

\lemma Separated-char (X : CoverSpace) : TFAE (
    {- 0 -} SeparatedCoverSpace { | CoverSpace => X },
    {- 1 -} \Pi {Y : PrecoverSpace} {f : PrecoverMap X Y} -> f.IsEmbedding -> isInj f,
    {- 2 -} isInj (completion {X}),
    {- 3 -} ∃ (Y : SeparatedCoverSpace) (f : PrecoverMap X Y) (isInj f)
  ) => TFAE.cycle (
    \lam Xs {_} {f} fe {x} {x'} fx=fx' => isSeparatedCoverSpace {Xs} $ SeparatedCoverSpace.separated-char   \lam x<=<U => \case cauchy-cover (fe x<=<U) (f x) \with {
      | inP (V, inP (W,h,p), Vfx) => h (x, (idp, p Vfx)) (p $ rewrite fx=fx' in Vfx)
    },
    \lam c => c completion.isDenseEmbedding.,
    \lam ci => inP (Completion X, completion, ci),
    \lam (inP (Y,f,fi)) => \new SeparatedCoverSpace {
      | isSeparatedCoverSpace c => fi $ isSeparatedCoverSpace \lam Cc => \case c (func-cover Cc) \with {
        | inP (U, inP (V,CV,p), (Ux,Uy)) => inP (V, CV, (rewrite p in Ux, rewrite p in Uy))
      }
    })

\func regPrecoverCauchyFilter {X : PrecoverSpace} (F : ProperFilter X) (Fc : ∀ {C : isCauchy} ∃ (U : C) (F U)) : CauchyFilter (RegPrecoverSpace X) \cowith
  | ProperFilter => F
  | isCauchyFilter Cc => ClosurePrecoverSpace.closure-filter F (\lam (inP ((A,A<=X),CAc)) => Fc $ A<=X CAc) Cc

\lemma regPrecoverSpace-extend-coverMap {X : PrecoverSpace} {Y : CoverSpace} (f : PrecoverMap X Y) : CoverMap (RegPrecoverSpace X) Y f \cowith
  | PrecoverMap => regPrecoverSpace-extend f