\import Function
\import Function.Meta
\import Logic.Unique
\import Logic
\import Logic.Meta
\import Logic.TFAE
\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

\func IsCauchyFilter {S : CoverSpace} (F : SetFilter S) : \Prop
  => \Pi {C : Set (Set S)} -> isCauchy C -> ∃ (U : C) (F U)

\lemma filter-limit-cauchy {X : CoverSpace} {F : SetFilter X} {a : X} (Fa : X.IsFilterLimit F a) : IsCauchyFilter F
  => \lam Cc => \case X.cauchy-regular-cover Cc a \with {
    | inP (U,CU,a<=<U) => inP (U, CU, filter-mono (Fa X.interior a<=<U) \lam x<=<U => <=<_<= x<=<U idp)
  }

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

\record CauchyFilter \extends WeaklyCauchyFilter, ProperFilter

\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
  }

  \lemma func-CF~ {F G : CauchyFilter Dom} (p : F CF~ G) : func-cauchy F CF~ func-cauchy G
    => isCauchyFilter {func-cauchy (CF~_meet p)} __
} \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 StronglyCauchyMap \extends CauchyMap
  | func-weak-cauchy (F : WeaklyCauchyFilter Dom) : WeaklyCauchyFilter Cod { | WeaklyProperFilter => WeaklyProperFilter-map func F }
  | func-cauchy F => \new CauchyFilter {
    | isCauchyFilter => isCauchyFilter {func-weak-cauchy F}
  }

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

  | func-weak-cauchy F => \new WeaklyCauchyFilter {
    | 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->topEmbedding (e : IsEmbedding) : IsTopEmbedding
    => ContMap.topEmbedding-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} : PrecoverMap.IsDenseEmbedding {id {X}}
    => PrecoverMap.id-denseEmbedding
}

\lemma CoverTransfer-map {X : \Set} {Y : CoverSpace} (f : X -> Y) : CoverMap (CoverTransfer f) Y f \cowith
  | func-cover => func-cover {PrecoverTransfer-map f}

\lemma CoverTransfer-univ {X Z : CoverSpace} {Y : \Set} (f : X -> Y) (g : Y -> Z) (fg : CoverMap X Z \lam x => g (f x)) : CoverMap X (CoverTransfer g) f \cowith
  | func-cover => func-cover {PrecoverTransfer-univ fg}

\lemma CoverTransfer_<=< {X : \Set} {Y : CoverSpace} {f : X -> Y} {x : X} {U : Set X} (x<=<U : single x <=< {CoverTransfer f} U)
  : ∃ (V : Set Y) (f ^-1 V ⊆ U) (single (f x) <=< V)
  => \case CoverSpace.interior {CoverTransfer f} {U} \with {
    | inP (V,Vo,p) => inP (V, rewriteI p \lam s => <=<_<= s idp, PrecoverSpace.open-char. Vo (transport {Set X} (__ x) p x<=<U))
  }

\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 : WeaklyCauchyFilter S) : \Prop
  => \Pi {C : Set (Set S)} -> isCauchy C -> ∃ (U : C) (\Sigma (F U) (G U))

\lemma CF~-sym {S : CoverSpace} {F G : WeaklyCauchyFilter 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 : WeaklyCauchyFilter 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 GW \case isProper $ filter-meet FU FW \with {
      | inP s => f s
    }
  }

\instance CauchyFilterEquivalence (S : CoverSpace) : Equivalence (CauchyFilter S)
  | ~ F G => F CF~ G
  | ~-transitive p q c => \case p (isRegular c) \with {
    | inP (U, inP (V, CV, U<=<V), (FU, GU)) => inP (V, CV, (filter-mono FU (<=<_<= U<=<V), 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 q p c => filter-mono (q c) p
  | 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 (inP (V,W,W<=<V,V<=<U,FW)) p => 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 FW $ <=<_<= W<=<V <=∘ <=<_<= V<=<U) \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 => <=<-left
  | 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

  \default isHausdorff p => isSeparatedCoverSpace (separated-char   p)
  \default isSeparatedCoverSpace p => isHausdorff (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 (S.open-char. Uo Ux) (S.open-char. Vo Vy),
      \lam f Cc => \have | (inP (_, inP (U', inP (U,CU,U'<=<U), idp), x<=<U')) => cauchy-cover (S.cauchy-open-cover $ isRegular Cc) x
                         | (inP (_, inP (V,h,idp), y<=<V)) => cauchy-cover (S.cauchy-open-cover (unfolds in U'<=<U)) y
                         | (inP (x',(x'<=<U,x'<=<V))) => f S.interior S.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 filter-point-limit {F : CauchyFilter \this} : IsFilterLimit F (filter-point F)
    => \lam Uo Up => \case filter-point-char. (open-char. Uo Up) \with {
      | inP (V,V<=<U,FV) => filter-mono FV (<=<_<= V<=<U)
    }
}

\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 (inP (V',V,p,V'<=<V,FV')) U<=U' => 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 FV' (<=<_<= V'<=<V)))
      }
  }


\sfunc cauchy-lift {X Y : CoverSpace} {Z : CompleteCoverSpace} (f : CoverMap X Y) (\property fd : f.IsDenseEmbedding) (g : CauchyMap X Z) (y : Y) : Z
  => Z.filter-point $ g.func-cauchy $ dense-filter-lift f fd (pointCF y)

\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 => cauchy-lift f fd g
  | 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 FV' \lam {y} V'y => transportInv U (\peval cauchy-lift f fd g y) $ <=<_<= (Z.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)
    }
  }

\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 => transportInv W (\peval cauchy-lift f fd g 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) : cauchy-lift f fd g (f x) = g x
  => (\peval cauchy-lift f fd g (f 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 (cauchy-lift f fd g y) <=< W <-> ∃ (W' : Set Z) (W' <=< W) (V : Set Y) (f ^-1 V ⊆ g ^-1 W') (single y <=< V)
  => rewrite (\peval cauchy-lift f fd g y) $ <->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 $ later $ filter-mono (filter-point-sub q) p
  }

\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)
  }

\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 FU' \lam U'x => g (F, (idp, U<=W $ filter-mono FU' $ <=<_<= U'<=<U)) $ U<=W $ <=<-right (single_<= U'x) U'<=<U

    \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)))
  }

\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 FU' \lam U'x => g (F, (idp, q $ filter-mono FU' $ <=<_<= U'<=<U)) $ q $ <=<-right (single_<= U'x) U'<=<U
        }
      }

    \lemma mkSet_<=<-point {F : RegularCauchyFilter X} {U : Set X} : single F <=< {Completion X} mkSet U <-> F U
      => (\lam p => filter-mono (pointCF_^-1_<=< p) (<=<_<= __ idp), \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 FU'V' meet-left, V'<=V $ filter-mono FU'V' meet-right)))
      | 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-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 {g} 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 {g} 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