CoverSpace

\import Data.Bool
\import Function.Meta
\import Logic
\import Logic.Meta
\import Logic.TFAE
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.Filter
\import Set.Subset
\import Topology.RatherBelow
\import Topology.TopSpace
\open Set
\open ClosurePrecoverSpace

\class PrecoverSpace \extends TopSpace {
  | isCauchy : Set (Set E) -> \Prop
  | cauchy-cover {C : Set (Set E)} : isCauchy C -> \Pi (x : E) -> ∃ (U : C) (U x)
  | cauchy-top : isCauchy (single top)
  | cauchy-refine {C D : Set (Set E)} : isCauchy C -> Refines C D -> isCauchy D
  | cauchy-glue {C : Set (Set E)} : isCauchy C -> \Pi {D : Set E -> Set (Set E)} -> (\Pi {U : Set E} -> C U -> isCauchy (D U))
    -> isCauchy (\lam U => ∃ (V W : Set E) (C V) (D V W) (U = V ∧ W))
  | cauchy-open {S : Set E} : isOpen S <-> ∀ {x : S} (isCauchy \lam U => U x -> U ⊆ S)

  \default open-top => cauchy-open.2 \lam _ => cauchy-refine cauchy-top \lam {U} _ => inP (U, \lam _ _ => (), <=-refl)
  \default open-inter Uo Vo => cauchy-open.2 $ later \lam {x} (Ux,Vx) => cauchy-refine (cauchy-glue (cauchy-open.1 Uo Ux) (\lam _ => cauchy-open.1 Vo Vx))
      \lam (inP (U',V',Uc,Vc,W=U'V')) => inP (U' ∧ V', \lam (U'x,V'x) {y} (U'y,V'y) => (Uc U'x U'y, Vc V'x V'y), =_<= W=U'V')
  \default open-Union So => cauchy-open.2 $ later \lam {x} (inP (U,SU,Ux)) => cauchy-refine (cauchy-open.1 (So SU) Ux) \lam {V} Vc => inP (V, \lam Vx => Vc Vx <=∘ Set.Union-cond SU, <=-refl)

  \default isOpen S : \Prop => ∀ {x : S} (isCauchy \lam U => U x -> U ⊆ S)
  \default cauchy-open \as cauchy-open-impl {S} : isOpen S <-> _ => <->refl

  \lemma cauchy-trans-dep {C : Set (Set E)} {D : \Pi {U : Set E} -> C U -> Set (Set E)} (Cc : isCauchy C) (Dc : \Pi {U : Set E} (c : C U) -> isCauchy (D c))
    : isCauchy (\lam U => ∃ (V W : Set E) (c : C V) (D c W) (U = V ∧ W))
    => transport isCauchy (ext \lam U => ext (\lam (inP (V,W,CV,DW,p)) => inP (V, W, CV, transport (D __ W) prop-pi DW.2, p), \lam (inP (V,W,c,DW,p)) => inP (V, W, c, (c,DW), p))) $ cauchy-glue Cc {\lam U V => \Sigma (c : C U) (D c V)} \lam CU => transport isCauchy (ext \lam V => ext (\lam d => (CU,d), \lam s => transport (D __ V) prop-pi s.2)) (Dc CU)

  \lemma open-char {S : Set E} : TopSpace.isOpen S <-> ∀ {x : S} (single x <=< S)
    => (\lam So Sx => cauchy-subset (cauchy-open.1 So Sx) $ later \lam f (y,(p,q)) => f $ rewrite p q,
        \lam f => cauchy-open.2 \lam {x} Sx => cauchy-subset (later $ f Sx) $ later \lam g Ux => g (x, (idp,Ux)))

  \func HasWeaklyDensePoints => \Pi {C : Set (Set E)} -> isCauchy (\lam U => (U = {Set E} bottom) || C U) -> isCauchy C

  \func HasDensePoints => \Pi {C : Set (Set E)} -> isCauchy C -> isCauchy \lam U => \Sigma (C U) (∃ U)

  \lemma hasDensePoints_hasWeaklyDensePoints (d : HasDensePoints) : HasWeaklyDensePoints
    => \lam Cc => cauchy-subset (d Cc) \case __ \with {
      | (byLeft e, inP (x,Ux)) => bottom-empty (rewrite e in Ux)
      | (byRight CU, _) => CU
    }
} \where {
  \lemma PrecoverSpace-ext {X : \Set} {S T : PrecoverSpace X} (p : \Pi {C : Set (Set X)} -> S.isCauchy C <-> T.isCauchy C) : S = T
    => exts (\lam U => <->_=.1 S.cauchy-open *> ext (\lam f Ux => p.1 (f Ux), \lam f Ux => p.2 (f Ux)) *> inv (<->_=.1 T.cauchy-open), \lam C => ext p)
}

\lemma cauchy-subset {X : PrecoverSpace} {C D : Set (Set X)} (Cc : isCauchy C) (e : \Pi {U : Set X} -> C U -> D U) : isCauchy D
  => cauchy-refine Cc \lam {U} CU => inP (U, e CU, <=-refl)

\lemma top-cauchy {X : PrecoverSpace} {C : Set (Set X)} (Ct : C top) : isCauchy C
  => cauchy-subset cauchy-top $ later \lam p => rewriteI p Ct

\lemma cauchy-inter {X : PrecoverSpace} {C D : Set (Set X)} (Cc : isCauchy C) (Dc : isCauchy D)
  : isCauchy (\lam U => ∃ (V W : Set X) (C V) (D W) (U = V ∧ W))
  => cauchy-glue Cc \lam _ => Dc

\lemma cauchy-array-inter {X : PrecoverSpace} (Cs : Array (Given X.isCauchy)) : isCauchy \lam V => ∃ (Us : Array (Set X) Cs.len) (\Pi (j : Fin Cs.len) -> (Cs j).1 (Us j)) (V = MeetSemilattice.Big_∧ (top :: Us)) \elim Cs
  | nil => top-cauchy $ inP $ later (nil, \case __ \with {}, idp)
  | C :: Cs => cauchy-subset (cauchy-inter C.2 (cauchy-array-inter Cs)) \lam {W} (inP (U, V, CU, inP (Us,f,q), p)) => inP $ later (U :: Us, \case \elim __ \with {
    | 0 => CU
    | suc j => f j
  }, p *> pmap (U ∧) q)

\record PrecoverMap \extends ContMap {
  \override Dom : PrecoverSpace
  \override Cod : PrecoverSpace
  | func-cover {D : Set (Set Cod)} : isCauchy D -> isCauchy \lam U => ∃ (V : D) (U = func ^-1 V)

  \default func-cont Uo => cauchy-open.2 $ later \lam {x} Ufx => cauchy-refine (func-cover (cauchy-open.1 Uo Ufx)) \lam (inP (W,c,d)) => inP (func ^-1 W, \lam a {_} => c a, =_<= d)

  \func IsEmbedding : \Prop
    => \Pi {C : Set (Set Dom)} -> isCauchy C -> isCauchy \lam V => ∃ (U : C) (func ^-1 V ⊆ U)

  -- | A map is an embedding if and only if the structure on the domain is the smallest compatible with the map.
  \lemma embedding-char : TFAE (
    {- 0 -} IsEmbedding,
    {- 1 -} \Pi {X : PrecoverSpace Dom} -> PrecoverMap X Cod func -> \Pi {C : Set (Set Dom)} -> isCauchy C -> X.isCauchy C,
    {- 2 -} \Pi {C : Set (Set Dom)} -> isCauchy C -> isCauchy {PrecoverTransfer func} C,
    {- 3 -} Dom = {PrecoverSpace Dom} PrecoverTransfer func
  ) => TFAE.cycle (
    \lam p f Cc => cauchy-refine (func-cover {f} $ p Cc) \lam (inP (V, inP (U',CU',p), q)) => inP (U', CU', rewrite q p),
    \lam f => f (PrecoverTransfer-map _),
    \lam f => PrecoverSpace.PrecoverSpace-ext {_} {Dom} {PrecoverTransfer func} \lam {C} => (f,PrecoverTransfer-char),
    \lam p => unfolds $ rewrite p \lam Dc => Dc)

  \func IsWeaklyDenseEmbedding : \Prop
    => \Sigma IsWeaklyDense IsEmbedding

  \func IsDenseEmbedding : \Prop
    => \Sigma IsDense IsEmbedding
} \where {
  \func id {X : PrecoverSpace} : PrecoverMap X X \cowith
    | func x => x
    | func-cover Dc => cauchy-subset Dc \lam {U} DU => inP $ later (U, DU, idp)

  \func compose \alias \infixl 8 ∘ {X Y Z : PrecoverSpace} (g : PrecoverMap Y Z) (f : PrecoverMap X Y) : PrecoverMap X Z \cowith
    | func x => g (f x)
    | func-cover Dc => cauchy-subset (f.func-cover $ g.func-cover Dc) \lam (inP (V, inP (W,DW,q), p)) => inP $ later (W, DW, p *> rewrite q idp)

  \func const {Y X : PrecoverSpace} (x : X) : PrecoverMap Y X \cowith
    | func _ => x
    | func-cover Dc => top-cauchy \case cauchy-cover Dc x \with {
      | inP (U,DU,Ux) => inP $ later (U, DU, ext \lam y => ext (\lam _ => Ux, \lam _ => ()))
    }

  \lemma id-denseEmbedding {X : PrecoverSpace} : PrecoverMap.IsDenseEmbedding {id {X}}
    => (\lam {x} _ Ux => inP (x, inP (x, idp), Ux), \lam Cc => cauchy-subset Cc \lam {U} CU => inP $ later (U, CU, <=-refl))

  \lemma embedding-left {X Y Z : PrecoverSpace} (f : PrecoverMap X Y) (g : PrecoverMap Y Z) (fg : PrecoverMap.IsEmbedding {g ∘ f}) : f.IsEmbedding
    => \lam Cc => cauchy-subset (g.func-cover $ fg Cc) \lam {_} (inP (V,r,idp)) => r
}

\type \infix 4 <=< {X : PrecoverSpace} (V U : Set X) : \Prop
  => isCauchy \lam W => Given (V ∧ W) -> W ⊆ U

\lemma <=<_single {X : PrecoverSpace} {x : X} {U : Set X} : single x <=< U <-> isCauchy \lam W => W x -> W ⊆ U
  => (\lam p => cauchy-subset (unfolds in p) \lam {W} h Wx => h (x, (idp, Wx)), \lam p => cauchy-subset p $ later \lam {W} h (y,(q,Wy)) => h $ rewrite q Wy)

\lemma <=<_<= {X : PrecoverSpace} {V U : Set X} (p : V <=< U) : V <= U
  => \lam {x} Vx => \case cauchy-cover (unfolds in p) x \with {
    | inP (W,f,Wx) => f (x, (Vx, Wx)) Wx
  }

\lemma <=<_^-1 {X Y : PrecoverSpace} {f : PrecoverMap X Y} {U V : Set Y} (U<=<V : U <=< V) : f ^-1 U <=< f ^-1 V
  => cauchy-subset (f.func-cover U<=<V) \lam (inP (W,g,p)) => rewrite p $ later \lam (x,s) => g (f x, s) __

\lemma <=<-cont {X : PrecoverSpace} {Y : CoverSpace} {f : ContMap X Y} {x : X} {U : Set Y} (fx<=<U : single (f x) <=< U) : single x <=< f ^-1 U
  => RegularRatherBelow.<=<-left (PrecoverSpace.open-char.1 (f.func-cont $ Y.interior {U}) fx<=<U) (<=<_<= __ idp)

\type \infix 4 s<=< {X : PrecoverSpace} (V U : Set X) : \Prop
  => isCauchy \lam W => (W = Compl V) || (W = U)

\lemma s<=<_<=< {X : PrecoverSpace} {V U : Set X} (p : V s<=< U) : V <=< U
  => cauchy-subset (unfolds in p) $ later \case __ \with {
    | byLeft q => rewrite q \lam (x,(Vx,nVx)) => absurd (nVx Vx)
    | byRight q => \lam _ => rewrite q <=-refl
  }

\lemma s<=<_<= {X : PrecoverSpace} {V U : Set X} (p : V s<=< U) : V <= U
  => <=<_<= (s<=<_<=< p)

\lemma s<=<_bottom {X : PrecoverSpace} {U : Set X} : bottom s<=< U
  => unfolds $ top-cauchy $ byLeft $ <=-antisymmetric (later \lam _ => \lam (inP s) => s.1) top-univ

\lemma s<=<_^-1 {X Y : PrecoverSpace} (f : PrecoverMap X Y) {U V : Set Y} (U<=<V : U s<=< V) : f ^-1 U s<=< f ^-1 V
  => cauchy-subset (f.func-cover U<=<V) \case __ \with {
    | inP (_, byLeft idp, p) => byLeft p
    | inP (_, byRight idp, p) => byRight p
  }

\instance RegularRatherBelow {X : PrecoverSpace} : RatherBelow {SetLattice X} (<=<)
  | <=<_top => unfolds $ top-cauchy \lam _ => <=-refl
  | <=<-left p q => cauchy-subset (unfolds in p) \lam f t => f t <=∘ q
  | <=<-right p q => cauchy-subset (unfolds in q) $ later \lam {Z} f (x,(Wx,Zx)) => f (x, (p Wx, Zx))
  | <=<_meet U<=<U' V<=<V' => cauchy-subset (cauchy-inter (unfolds in U<=<U') V<=<V') $ later \lam (inP (U'', V'', t1, t2, p)) =>
      rewrite p \lam (x,((Ux,Vx),(U''x,V''x))) => MeetSemilattice.meet-monotone (t1 (x,(Ux,U''x))) (t2 (x,(Vx,V''x)))

\instance StronglyRatherBelow {X : PrecoverSpace} : RatherBelow {SetLattice X} (s<=<)
  | <=<_top => unfolds $ top-cauchy $ byRight idp
  | <=<-left p q => cauchy-refine (unfolds in p) \lam {U'} => later \case __ \with {
    | byLeft r => rewrite r $ inP (_, byLeft idp, <=-refl)
    | byRight r => rewrite r $ inP (_, byRight idp, q)
  }
  | <=<-right p q => cauchy-refine (unfolds in q) \lam {U'} => later \case __ \with {
    | byLeft r => inP (_, byLeft idp, rewrite r \lam nVx Wx => nVx (p Wx))
    | byRight r => inP (U', byRight r, <=-refl)
  }
  | <=<_meet U<=<U' V<=<V' => cauchy-refine (cauchy-inter (unfolds in U<=<U') V<=<V') $ later \lam (inP (U'', V'', t1, t2, p)) => rewrite p \case \elim t1, \elim t2 \with {
    | byLeft r, _ => inP (_, byLeft idp, rewrite r \lam (nUx,_) (Ux,_) => nUx Ux)
    | _, byLeft r => inP (_, byLeft idp, rewrite r \lam (_,nVx) (_,Vx) => nVx Vx)
    | byRight q, byRight r => inP (_, byRight $ pmap2 (∧) q r, <=-refl)
  }

\class CoverSpace \extends PrecoverSpace {
  | isRegular {C : Set (Set E)} : isCauchy C -> isCauchy \lam V => ∃ (U : C) (V <=< U)

  \lemma cauchy-regular-cover {C : Set (Set E)} (Cc : isCauchy C) (x : E) : ∃ (U : C) (single x <=< U)
    => \case cauchy-cover (isRegular Cc) x \with {
      | inP (U, inP (V, CV, U<=<V), Ux) => inP (V, CV, <=<-right (single_<= Ux) U<=<V)
    }

  \lemma interior {U : Set E} : TopSpace.isOpen \lam x => single x <=< U
    => open-char.2 \lam x<=<U => \case <=<-inter x<=<U \with {
      | inP (V,x<=<V,V<=<U) => <=<-left x<=<V \lam Vx => later $ <=<-right (single_<= Vx) V<=<U
    }

  \lemma cauchy-open-cover {C : Set (Set E)} (Cc : isCauchy C) : isCauchy \lam V => ∃ (U : C) (V = \lam x => single x <=< U)
    => cauchy-refine (isRegular Cc) \lam {V} (inP (U,CU,V<=<U)) => inP $ (_, inP (U, CU, idp), \lam Vx => <=<-right (single_<= Vx) V<=<U)
} \where {
  \lemma CoverSpace-ext {X : \Set} {S T : CoverSpace X} (p : \Pi {C : Set (Set X)} -> S.isCauchy C <-> T.isCauchy C) : S = T
    => exts (\lam U => <->_=.1 S.cauchy-open *> ext (\lam f Ux => p.1 (f Ux), \lam f Ux => p.2 (f Ux)) *> inv (<->_=.1 T.cauchy-open), \lam C => ext p)
}

\lemma <=<-inter {X : CoverSpace} {x : X} {U : Set X} (x<=<U : single x <=< U) : ∃ (V : Set X) (single x <=< V) (V <=< U)
  => \case X.cauchy-regular-cover (isRegular x<=<U) x \with {
    | inP (V, inP (U', f, V<=<U'), x<=<V) => inP (V, x<=<V, <=<-left V<=<U' $ f (x, (idp, <=<_<= V<=<U' $ <=<_<= x<=<V idp)))
  }

\lemma s<=<-inter {X : StronglyRegularCoverSpace} {x : X} {U : Set X} (x<=<U : single x <=< U) : ∃ (V : Set X) (single x s<=< V) (V s<=< U)
  => \case cauchy-cover (isStronglyRegular $ isStronglyRegular $ unfolds in x<=<U) x \with {
    | inP (V'', inP (V', inP (V, h, V'<=<V), V''<=<V'), V''x) => inP (V', <=<-right (single_<= V''x) V''<=<V', <=<-left V'<=<V $ h (x, (idp, s<=<_<= V'<=<V $ s<=<_<= V''<=<V' V''x)))
  }

\lemma denseSet-char {X : CoverSpace} {S : Set X} : TFAE (
    IsDenseSet S,
    \Pi {x : X} {U : Set X} -> single x <=< U -> ∃ (x' : S) (U x'),
    ∀ {C : isCauchy} (isCauchy \lam V => ∃ (U : C) (V ⊆ U) (Given V -> ∃ (x : S) (U x)))
) => TFAE.proof (
      ((0,1), \lam d x<=<U => \case d X.interior x<=<U \with {
        | inP (x',Sx',x'<=<U) => inP (x', Sx', <=<_<= x'<=<U idp)
      }),
      ((1,0), \lam d Uo Uy => d $ PrecoverSpace.open-char.1 Uo Uy),
      ((1,2), \lam d Cc => cauchy-subset (isRegular Cc) \lam (inP (V,CV,U<=<V)) => inP $ later (V, CV, <=<_<= U<=<V, \lam (x,Ux) => d $ <=<-right (single_<= Ux) U<=<V)),
      ((2,1), \lam d {x} {U} x<=<U => \case cauchy-cover (d x<=<U) x \with {
         | inP (V, inP (W,f,V<=W,g), Vx) => \case g (x,Vx) \with {
           | inP (y,Sy,Wy) => inP (y, Sy, f (x, (idp, V<=W Vx)) Wy)
         }
       }))

\lemma dense-char {X : PrecoverSpace} {Y : CoverSpace} {f : PrecoverMap X Y} : f.IsDense <-> (\Pi {y : Y} {U : Set Y} -> single y <=< U -> ∃ (x : X) (U (f x)))
  => (\lam d p => \case denseSet-char 0 1 d p \with {
    | inP (y, inP (x,fx=y), Uy) => inP (x, rewrite fx=y Uy)
  }, \lam d => denseSet-char 1 0 \lam p => \case d p \with {
    | inP (x,Ufx) => inP (f x, inP $ later (x, idp), Ufx)
  })

\class StronglyRegularCoverSpace \extends CoverSpace
  | isStronglyRegular {C : Set (Set E)} : isCauchy C -> isCauchy \lam V => ∃ (U : C) (V s<=< U)
  | isRegular Cc => cauchy-subset (isStronglyRegular Cc) \lam (inP (V,CV,Us<=<V)) => inP $ later (V, CV, s<=<_<=< Us<=<V)

\class OmegaRegularCoverSpace \extends CoverSpace
  | isOmegaRegular {C : Set (Set E)} : isCauchy C -> isCauchy \lam V => ∃ (U : C) (V RegularRatherBelow.<=<o U)
  | isRegular Cc => cauchy-subset (isOmegaRegular Cc) \lam (inP (V,CV,p)) => inP $ later (V, CV, RegularRatherBelow.<=<o_<=< p)

\class CompletelyRegularCoverSpace \extends OmegaRegularCoverSpace
  | isCompletelyRegular {C : Set (Set E)} : isCauchy C -> isCauchy \lam V => ∃ (U : C) (V RegularRatherBelow.<=<c U)
  | isOmegaRegular Cc => cauchy-subset (isCompletelyRegular Cc) \lam (inP (V,CV,U<=<cV)) => inP $ later (V, CV, RatherBelow.<=<c_<=<o U<=<cV)

\class CompletelyStronglyRegularCoverSpace \extends StronglyRegularCoverSpace, CompletelyRegularCoverSpace
  | isCompletelyStronglyRegular {C : Set (Set E)} : isCauchy C -> isCauchy \lam V => ∃ (U : C) (V StronglyRatherBelow.<=<c U)
  | isStronglyRegular Cc => cauchy-subset (isCompletelyStronglyRegular Cc) \lam {V} (inP (U,CU,V<=<U)) => inP $ later (U, CU, RatherBelow.<=<c_<=< V<=<U)
  | isCompletelyRegular Cc => cauchy-subset (isCompletelyStronglyRegular Cc) \lam {V} (inP (U,CU,V<=<U)) => inP $ later (U, CU, StronglyRatherBelow.<=<c-func s<=<_<=< V<=<U)

\func AntiDiscreteCover (X : \Set) : CompletelyStronglyRegularCoverSpace X \cowith
  | isCauchy C => C top
  | cauchy-cover Ct x => inP (top, Ct, ())
  | cauchy-top => idp
  | cauchy-refine Ct e => \case e Ct \with {
    | inP (V,DV,t<=V) => rewrite (<=-antisymmetric t<=V top-univ) DV
  }
  | cauchy-glue Ct e => inP (top, top, Ct, e Ct, <=-antisymmetric (\lam _ => ((), ())) top-univ)
  | isCompletelyStronglyRegular Ct => inP (top, Ct, RatherBelow.Interpolative.<=<_top)

\func DiscreteCover (X : \Set) : CompletelyRegularCoverSpace X \cowith
  | TopSpace => DiscreteTopSpace X
  | isCauchy C => \Pi (x : X) -> ∃ (U : C) (U x)
  | cauchy-cover c => c
  | cauchy-top x => inP (top, idp, ())
  | cauchy-refine c d x =>
    \have | (inP (U,CU,Ux)) => c x
          | (inP (V,DV,U<=V)) => d CU
    \in inP (V, DV, U<=V Ux)
  | cauchy-glue c d x =>
    \have | (inP (U,CU,Ux)) => c x
          | (inP (V,DV,Vx)) => d CU x
    \in inP (U ∧ V, inP (U, V, CU, DV, idp), (Ux,Vx))
  | isCompletelyRegular f x => \case f x \with {
    | inP (U,CU,Ux) => inP (U, inP (U, CU, inP (=, \lam p => rewrite p \lam x => inP (single x, \lam (y,(Uy,x=y)) => rewrite x=y $ single_<= Uy, idp), \lam p => inP (_, idp, p), idp)), Ux)
  }
  | cauchy-open => (\lam _ Sx x' => inP (= x', \lam p => rewrite p $ single_<= Sx, idp), \lam _ => ())

\func PrecoverTransfer {X : \Set} {Y : PrecoverSpace} (f : X -> Y) : PrecoverSpace X \cowith
  | isCauchy C => Y.isCauchy \lam V => ∃ (U : C) (f ^-1 V ⊆ U)
  | cauchy-cover Ec x => \case cauchy-cover Ec (f x) \with {
    | inP (U, inP (V,CV,p), Ufx) => inP (V, CV, p Ufx)
  }
  | cauchy-top => top-cauchy $ inP $ later (top, idp, top-univ)
  | cauchy-refine Ec r => cauchy-subset Ec \lam (inP (V,CV,p)) => \case r CV \with {
    | inP (W,DW,V<=W) => inP $ later (W, DW, p <=∘ V<=W)
  }
  | cauchy-glue {C} Ec {D} Fc => cauchy-subset (cauchy-glue Ec {\lam U V => ∃ (U' : C) (f ^-1 U ⊆ U') (V' : D U') (f ^-1 V ⊆ V')}
      \lam (inP (U',CU',p)) => cauchy-subset (Fc CU') \lam {V} (inP (V',DU'V',q)) => inP $ later (U', CU', p, V', DU'V', q))
      \lam {_} (inP (U, V, _, inP (U',CU',p,V',DU'V',q), idp)) => inP $ later (_, inP (U', V', CU', DU'V', idp), MeetSemilattice.meet-monotone p q)
  \where {
    \lemma makeCauchy {C : Set (Set Y)} (Cc : isCauchy C) : isCauchy {PrecoverTransfer f} \lam U => ∃ (V : C) (U = f ^-1 V)
      => cauchy-subset Cc \lam {V} CV => inP $ later (f ^-1 V, inP (V, CV, idp), <=-refl)
  }

\lemma PrecoverTransfer-map {X : \Set} {Y : PrecoverSpace} (f : X -> Y) : PrecoverMap (PrecoverTransfer f) Y f \cowith
  | func-cover Dc => cauchy-subset Dc \lam DU => inP $ later (_, inP (_, DU, idp), <=-refl)

\lemma PrecoverTransfer-char {X Y : PrecoverSpace} {f : PrecoverMap X Y} {C : Set (Set X)} (Dc : isCauchy {PrecoverTransfer f} C) : X.isCauchy C
  => cauchy-refine (f.func-cover Dc) \lam {_} (inP (V,r,idp)) => r

\lemma PrecoverTransfer-univ {X Z : PrecoverSpace} {Y : \Set} {f : X -> Y} {g : Y -> Z} (fg : PrecoverMap X Z \lam x => g (f x)) : PrecoverMap X (PrecoverTransfer g) f \cowith
  | func-cover Dc => cauchy-refine (fg.func-cover Dc) \lam {_} (inP (V, inP (W,DW,q), idp)) => inP $ (_, inP (W, DW, idp), q __)

\func ClosurePrecoverSpace {X : \Set} (A : Set (Set X) -> \Prop) (CA : \Pi {C : Set (Set X)} -> A C -> \Pi (x : X) -> ∃ (U : C) (U x)) : PrecoverSpace X \cowith
  | isCauchy => Closure A
  | cauchy-cover CC x => closure-filter (pointFilter x) (\lam AC => CA AC x) CC
  | cauchy-top => closure-top idp
  | cauchy-refine => closure-refine
  | cauchy-glue => closure-trans __ __ idp
  \where {
    \truncated \data Closure {X : \Set} (A : Set (Set X) -> \Prop) (C : Set (Set X)) : \Prop
      | closure (A C)
      | closure-top (C = single top)
      | closure-refine {D : Set (Set X)} (Closure A D) (Refines D C)
      | closure-trans {D : Set (Set X)} (Closure A D) {E : \Pi (U : Set X) -> Set (Set X)} (\Pi {U : Set X} -> D U -> Closure A (E U))
                      (C = \lam U => ∃ (V W : Set X) (D V) (E V W) (U = V ∧ W))

    \lemma closure-inter {A : Set (Set X) -> \Prop} {C D : Set (Set X)} (Cc : Closure A C) (Dc : Closure A D)
      : Closure A (\lam W => ∃ (U V : Set X) (C U) (D V) (W = U ∧ V))
      => closure-trans Cc (\lam _ => Dc) idp

    \lemma closure-subset {X : \Set} {A : Set (Set X) -> \Prop} {C D : Set (Set X)} (Dc : Closure A D) (D<=C : D ⊆ C) : Closure A C
      => closure-refine Dc \lam {V} DV => inP (V, D<=C DV, <=-refl)

    \lemma closure-filter {A : Set (Set X) -> \Prop} (F : SetFilter X) (CA : \Pi {C : Set (Set X)} -> A C -> ∃ (U : C) (F U)) {C : Set (Set X)} (CC : Closure A C) : ∃ (U : C) (F U) \elim CC
      | closure AC => CA AC
      | closure-top idp => inP (top, idp, filter-top)
      | closure-refine {D} CD e =>
        \have | (inP (U,DU,FU)) => closure-filter F CA CD
              | (inP (V,CV,U<=V)) => e DU
        \in inP (V, CV, filter-mono FU U<=V)
      | closure-trans {D} CD {E} CE idp =>
        \have | (inP (U,DU,FU)) => closure-filter F CA CD
              | (inP (V,EV,FV)) => closure-filter F CA (CE DU)
        \in inP (U ∧ V, inP (U, V, DU, EV, idp), filter-meet FU FV)

    \lemma closure-cauchy {S : PrecoverSpace X} {A : Set (Set X) -> \Prop} (AS : \Pi {C : Set (Set X)} -> A C -> S.isCauchy C) {C : Set (Set X)} (CC : Closure A C) : S.isCauchy C \elim CC
      | closure AC => AS AC
      | closure-top p => rewrite p cauchy-top
      | closure-refine CD e => cauchy-refine (closure-cauchy AS CD) e
      | closure-trans CD CE idp => S.cauchy-trans-dep (closure-cauchy AS CD) \lam DU => closure-cauchy AS (CE DU)

    \lemma closure-univ-cover {Y : PrecoverSpace} {f : Y -> X} (Ap : ∀ {C : A} (isCauchy \lam U => ∃ (V : Set X) (C V) (U = f ^-1 V))) {C : Set (Set X)} (Cc : Closure A C) : isCauchy \lam U => ∃ (V : Set X) (C V) (U = f ^-1 V) \elim Cc
      | closure a => Ap a
      | closure-top p => cauchy-subset cauchy-top \lam q => inP $ later (top, rewrite p idp, inv q)
      | closure-refine Cc g => cauchy-refine (closure-univ-cover Ap Cc) \lam (inP (V,CV,q)) => TruncP.map (g CV) \lam (V',CV',V<=V') => (f ^-1 V', inP (V', CV', idp), rewrite q \lam c => V<=V' c)
      | closure-trans {D} Cc {E} g p =>
        \have t => cauchy-glue (closure-univ-cover Ap Cc) {\lam V V' => ∃ (U : Set X) (V = f ^-1 U) (D U) (U' : Set X) (E U U') (V' = f ^-1 U')}
                    \lam (inP (V,DV,q)) => cauchy-subset (closure-univ-cover Ap (g DV)) \lam (inP (V',EVV',r)) => inP $ later (V, q, DV, V', EVV', r)
        \in cauchy-subset t \lam (inP (W, W', _, inP (V2,p2,DV2,V2',EV2V2',p2'), U=WW')) => inP $ later $ rewrite p (_, inP (V2, V2', DV2, EV2V2', idp), U=WW' *> pmap2 (∧) p2 p2')

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

    \lemma closure-univ-closure {Y : \Set} {B : Set (Set Y) -> \Prop} (f : Y -> X) (Ap : ∀ {C : A} (Closure B \lam V => ∃ (U : Set X) (C U) (V = f ^-1 U))) {C : Set (Set X)} (Cc : Closure A C) : Closure B \lam U => ∃ (V : Set X) (C V) (U = f ^-1 V) \elim Cc
      | closure a => Ap a
      | closure-top p => closure-subset (closure-top idp) \lam q => inP $ later (top, rewrite p idp, inv q)
      | closure-refine Cc g => closure-refine (closure-univ-closure {X} {A} _ Ap Cc) \lam (inP (V,CV,q)) => TruncP.map (g CV) \lam (V',CV',V<=V') => (f ^-1 V', inP (V', CV', idp), rewrite q \lam c => V<=V' c)
      | closure-trans {D} Cc {E} g p =>
        \have t => closure-trans (closure-univ-closure {X} {A} _ Ap Cc) {\lam V V' => ∃ (U : Set X) (V = f ^-1 U) (D U) (U' : Set X) (E U U') (V' = f ^-1 U')}
            (\lam (inP (V,DV,q)) => closure-subset (closure-univ-closure {X} {A} _ Ap (g DV)) \lam (inP (V',EVV',r)) => inP $ later (V, q, DV, V', EVV', r)) idp
        \in closure-subset t \lam (inP (W, W', _, inP (V2,p2,DV2,V2',EV2V2',p2'), U=WW')) => inP $ later $ rewrite p (_, inP (V2, V2', DV2, EV2V2', idp), U=WW' *> pmap2 (∧) p2 p2')

    \lemma closure-univ-closure-id {B : Set (Set X) -> \Prop} (Ap : ∀ {C : A} (Closure B C)) {C : Set (Set X)} (Cc : Closure A C) : Closure B C
      => closure-subset (closure-univ-closure (\lam x => x) (\lam AC => closure-subset (Ap AC) \lam {U} CU => inP (U, CU, idp)) Cc) \lam {U} (inP (V,CV,p)) => rewrite p CV

    \lemma closure-map {X Y : \Set} (f : Set X -> Set Y) (ft : \Pi {y : Y} -> f top y) (fm : \Pi {U V : Set X} -> U ⊆ V -> f U ⊆ f V) (fi : \Pi {U V : Set X} -> f U ∧ f V ⊆ f (U ∧ V)) {A : Set (Set X) -> \Prop} {C : Set (Set X)} {D : Set (Set Y)} (eCD : ∀ {U : C} ∃ (V : D) (f U ⊆ V)) (CC : Closure A C) : Closure (\lam D => ∃ (C : A) ∀ {U : C} ∃ (V : D) (f U ⊆ V)) D \elim CC
      | closure AC => closure $ inP (C, AC, eCD)
      | closure-top p => \case eCD (rewrite p idp) \with {
        | inP (V,DV,RtV) => closure-refine (closure-top idp) \lam q => inP (V, DV, \lam _ => RtV ft)
      }
      | closure-refine {E} CE e => closure-refine (closure-map f ft fm fi (\lam EU => \case e EU \with {
        | inP (V,CV,U<=V) => \case eCD CV \with {
          | inP (W,DW,RVW) => inP (W, DW, fm U<=V <=∘ RVW)
        }
      }) CE) \lam {V} DV => inP (V, DV, <=-refl)
      | closure-trans {C'} CC' {E} CE p =>
        closure-refine (closure-trans (closure-map f ft fm fi {_} {_} {\lam V => ∃ (U : C') (f U = V)} (\lam {U} C'U => inP (f U, inP (U, C'U, idp), <=-refl)) CC') {\lam U V => ∃ (U' : C') (V' : E U') (f U' = U) (f V' = V)}
            (\lam (inP (U',C'U',RU'U)) => closure-subset (closure-map f ft fm fi {_} {_} {\lam V => ∃ (U : E U') (f U = V)} (\lam {U} EU'U => inP (f U, inP (U, EU'U, idp), <=-refl)) (CE C'U')) \lam {V} (inP (V',EU'V',RV'V)) => inP (U', C'U', V', EU'V', RU'U, RV'V)) idp)
            \lam {W} (inP (U, V, _, inP (U',C'U',V',EU'V',RU'U,RV'V), W=UV)) => \case eCD (rewrite p $ inP (U', V', C'U', EU'V', idp)) \with {
              | inP (W',DW',r) => inP (W', DW', rewrite W=UV $ rewriteI (RU'U,RV'V) $ fi <=∘ r)
            }

    \lemma closure-embedding {S : PrecoverSpace X} {Y : PrecoverSpace} (AS : \Pi {C : Set (Set X)} -> isCauchy C -> Closure A C) (f : PrecoverMap S Y)
                             (p : \Pi {C : Set (Set X)} -> A C -> isCauchy \lam V => ∃ (U : C) (f ^-1 V ⊆ U)) : f.IsEmbedding
      => \lam CC => aux (AS CC)
      \where {
        \private \lemma aux {C : Set (Set X)} (CC : Closure A C) : isCauchy \lam V => ∃ (U : C) (f ^-1 V ⊆ U) \elim CC
          | closure AC => p AC
          | closure-top q => top-cauchy $ inP $ later (top, rewrite q idp, top-univ)
          | closure-refine CD g => cauchy-subset (aux CD) \lam (inP (V,DV,q)) => TruncP.map (g DV) \lam (V',CV',V<=V') => later (V', CV', q <=∘ V<=V')
          | closure-trans {D} CD {E} g q =>
            \let t => cauchy-glue (aux CD) {\lam V V' => ∃ (U U' : Set X) (D U) (f ^-1 V ⊆ U) (f ^-1 V' ⊆ U') (E U U')} \lam (inP (U,DU,r)) => cauchy-subset (aux (g DU)) \lam (inP (U',EUU',r')) => inP $ later (U, U', DU, r, r', EUU')
            \in cauchy-subset t \lam (inP (V, W, _, inP (U1,U2,DU1,r,r',EU1U2), s)) => inP $ later (U1 ∧ U2, rewrite q $ inP (U1, U2, DU1, EU1U2, idp), rewrite s $ MeetSemilattice.meet-monotone r r')
      }
  }

\instance PrecoverLattice (X : \Set) : CompleteLattice (PrecoverSpace X)
  | <= A B => \Pi {C : Set (Set X)} -> isCauchy {A} C -> isCauchy {B} C
  | <=-refl c => c
  | <=-transitive f g c => g (f c)
  | <=-antisymmetric f g => PrecoverSpace.PrecoverSpace-ext \lam {C} => (f,g)
  | top => DiscreteCover X
  | top-univ {A} c => cauchy-cover {A} c
  | Join {J} f => ClosurePrecoverSpace (\lam C => ∃ (j : J) (isCauchy {f j} C))
      \lam e x => \case \elim e \with {
        | inP (j,Cc) => cauchy-cover Cc x
      }
  | Join-cond j Cc => closure $ inP (j,Cc)
  | Join-univ e => closure-cauchy $ later \case __ \with {
    | inP (j,Cc) => e j Cc
  }

\func CoverTransfer {X : \Set} {Y : CoverSpace} (f : X -> Y) : CoverSpace X \cowith
  | TopSpace => TopTransfer f
  | isCauchy => isCauchy {PrecoverTransfer f}
  | cauchy-cover => cauchy-cover {PrecoverTransfer f}
  | cauchy-top => cauchy-top {PrecoverTransfer f}
  | cauchy-refine => cauchy-refine {PrecoverTransfer f}
  | cauchy-glue => cauchy-glue {PrecoverTransfer f}
  | isRegular Dc => cauchy-subset (isRegular Dc) \lam {V} (inP (U, inP (W,CW,p), V<=<U)) => inP $ later
      (_, inP (W, CW, <=<-left (cauchy-subset (unfolds in V<=<U) \lam {W} g => inP $ later (_, \lam (x,s) {_} => g (f x, s), <=-refl)) p), <=-refl)
  | cauchy-open {S} => (\lam (inP (V,Vo,p)) Sx => cauchy-subset (cauchy-open.1 Vo $ rewrite p in Sx) \lam {W} g => inP $ later (f ^-1 W, \lam Wfx {y} Wfy => rewrite p $ g Wfx Wfy, <=-refl),
                        \lam c => inP (Union \lam V' => \Sigma (isOpen V') (f ^-1 V' ⊆ S), open-Union __.1, <=-antisymmetric (\lam {x} Sx => \case Y.cauchy-regular-cover (c Sx) (f x) \with {
                          | inP (V, inP (U,g,p), fx<=<V) => inP (_, (Y.interior {V}, \lam {x'} fx'<=<V => g (p $ <=<_<= fx<=<V idp) (p $ <=<_<= fx'<=<V idp)), fx<=<V)
                        }) \lam (inP (V,(_,p),Vfx)) => p Vfx))

\func CoverSub {X : CoverSpace} (S : Set X) : CoverSpace (Set.Total S)
  => CoverTransfer __.1

\func ClosureCoverSpace {X : \Set} (A : Set (Set X) -> \Prop)
                        (CA : \Pi {C : Set (Set X)} -> A C -> \Pi (x : X) -> ∃ (U : C) (U x))
                        (AS : \Pi {C : Set (Set X)} -> A C -> Closure A \lam V => ∃ (U : C) (Closure A \lam W => Given (V ∧ W) -> W ⊆ U))
  : CoverSpace X \cowith
  | PrecoverSpace => ClosurePrecoverSpace A CA
  | isRegular => closure-regular {ClosurePrecoverSpace A CA} RegularRatherBelow \lam AC => closure-subset (AS AC) \lam (inP (U,CU,c)) => inP (U, CU, c)
  \where {
    \lemma closure-regular {X : PrecoverSpace} (RB : RatherBelow {SetLattice X}) {A : Set (Set X) -> \Prop} (AS : \Pi {C : Set (Set X)} -> A C -> Closure A \lam V => ∃ (U : C) (RB.R V U)) {C : Set (Set X)} (CC : Closure A C)
      : Closure A (\lam V => ∃ (U : C) (RB.R V U)) \elim CC
      | closure AC => AS AC
      | closure-top idp => closure-subset (closure-top idp) \lam p => inP (top, idp, <=<_top)
      | closure-refine CD e => closure-subset (closure-regular RB AS CD) \lam (inP (U,DU,RVU)) => \case e DU \with {
        | inP (W,CW,U<=W) => inP (W, CW, <=<-left RVU U<=W)
      }
      | closure-trans {D} CD {E} CE idp => closure-subset
          (closure-trans (closure-regular RB AS CD) {\lam U V => ∃ (U' : Set X) (D U') (RB.R U U') (V' : E U') (RB.R V V')}
              (\lam (inP (U',DU',RUU')) => closure-subset (closure-regular RB AS (CE DU')) \lam (inP (V',EV',RVV')) => inP (U', DU', RUU', V', EV', RVV')) idp)
          \lam {U} (inP (V, W, _, inP (V',DV',RVV',W',EW',RWW'), U=VW)) => inP (V' ∧ W', inP (V',W',DV',EW',idp), rewrite U=VW $ <=<_meet RVV' RWW')

    \lemma closure-pred {X : PrecoverSpace} (P : Set X -> \Prop) (Pt : P top) (Pm : ∀ {U V : P} (P (U ∧ V))) {A : Set (Set X) -> \Prop} (AP : ∀ {C : A} {U : C} (P U)) {C : Set (Set X)} (CC : Closure A C) : ∃ (D : Closure A) (∀ {V : D} (P V)) (∀ {V : D} ∃ (U : C) (V ⊆ U)) \elim CC
      | closure AC => inP (C, closure AC, AP AC __, \lam {V} CV => inP (V, CV, <=-refl))
      | closure-top idp => inP (single top, closure-top idp, \lam p => rewriteI p Pt, \lam _ => inP (top, idp, top-univ))
      | closure-refine CD e => \case closure-pred P Pt Pm AP CD \with {
        | inP (D',AD',D'P,D'r) => inP (D', AD', D'P, \lam D'V => \case D'r D'V \with {
          | inP (U,DU,V<=U) => \case e DU \with {
            | inP (U',CU',U<=U') => inP (U', CU', V<=U <=∘ U<=U')
          }
        })
      }
      | closure-trans {D} CD {E} CE p => \case closure-pred P Pt Pm AP CD \with {
        | inP (D',AD',D'P,D'r) => inP (_, closure-trans AD' {\lam V' W' => ∃ (V : D) (W : E V) (P W') (V' ⊆ V) (W' ⊆ W)} (\lam {V'} D'V' => \case D'r D'V' \with {
          | inP (V,DV,V'<=V) => \case closure-pred P Pt Pm AP (CE DV) \with {
            | inP (E',AE',E'P,E'r) => closure-subset AE' \lam {W'} E'W' => \case E'r E'W' \with {
              | inP (W,EW,W'<=W) => inP (V, DV, W, EW, E'P E'W', V'<=V, W'<=W)
            }
          }
        }) idp, \lam {U} (inP (V', W', D'V', inP t, q)) => rewrite q $ Pm (D'P D'V') t.5, \lam {U} (inP (V', W', D'V', inP (V,DV,W,EW,PW',V'<=V,W'<=W), q)) => rewrite p $ inP (V ∧ W, inP (V, W, DV, EW, idp), rewrite q $ MeetSemilattice.meet-monotone V'<=V W'<=W))
      }
  }

\func ClosureRegularCoverSpace {X : \Set} (A : Set (Set X) -> \Prop)
                               (CA : \Pi {C : Set (Set X)} -> A C -> \Pi (x : X) -> ∃ (U : C) (U x))
                               (AI : \Pi {C : Set (Set X)} -> A C -> ∃ (D : A) ∀ {V : D} ∃ (U : C) ∀ {V' : D} (Given (V ∧ V') -> V' ⊆ U))
  : CompletelyRegularCoverSpace X \cowith
  | PrecoverSpace => ClosurePrecoverSpace A CA
  | isCompletelyRegular => ClosureCoverSpace.closure-regular {ClosurePrecoverSpace A CA} RegularRatherBelow.Interpolative \case AI __ \with {
    | inP (D,AD,f) => closure-subset (closure AD) \case f __ \with {
      | inP (U,CU,g) => inP (U, CU, inP
          (\lam V' U' => ∃ (E : A) ∀ {W : E} (Given (V' ∧ W) -> W ⊆ U'),
           \lam (inP (E,AE,h)) => closure-subset (closure AE) \lam EW => h EW,
           \lam {V'} (inP (E,AE,h)) => \case AI AE \with {
             | inP (F,AF,k) => inP (Union \lam W => Given (F W) (V' ∧ W), inP (F, AF, \lam c s => Union-cond $ later (c,s.1,s.2)),
                                    inP (F, AF, \lam FW (x, (inP (W', (FW',y,(V'y,W'y)), W'x), Wx)) => \case k FW' \with {
                                      | inP (U,EU,l) => l FW (x, (W'x, Wx)) <=∘ h EU (y, (V'y, l FW' (y,(W'y,W'y)) W'y))
                                    }))
           },
           inP (D, AD, g)))
    }
  }

\instance CoverLattice (X : \Set) : CompleteLattice (CoverSpace X)
  | <= A B => \Pi {C : Set (Set X)} -> isCauchy {A} C -> isCauchy {B} C
  | <=-refl c => c
  | <=-transitive f g c => g (f c)
  | <=-antisymmetric f g => CoverSpace.CoverSpace-ext \lam {C} => (f,g)
  | top => DiscreteCover X
  | top-univ {A} c => cauchy-cover {A} c
  | Join f => \new CoverSpace {
    | PrecoverSpace => Join {PrecoverLattice X} f
    | isRegular => ClosureCoverSpace.closure-regular {Join f} RegularRatherBelow $ later \case __ \with {
      | inP (j,Cc) => closure $ inP (j, cauchy-subset (isRegular {f j} Cc) $ later \lam {U} (inP (V,CV,U<=<V)) => inP (V, CV, Join-cond {PrecoverLattice X} j {f} U<=<V))
    }
  }
  | Join-cond j {f} => Join-cond {PrecoverLattice X} j
  | Join-univ => Join-univ {PrecoverLattice X}
  | join A B => \new CoverSpace {
    | PrecoverSpace => A ∨ {PrecoverLattice X} B
    | isRegular => ClosureCoverSpace.closure-regular {A ∨ B} RegularRatherBelow $ later \case __ \with {
      | inP (true, Cc) => closure $ inP (true, cauchy-subset (isRegular Cc) $ later \lam {U} (inP (V,CV,U<=<V)) => inP (V, CV, join-left {PrecoverLattice X} {A} {B} U<=<V))
      | inP (false, Cc) => closure $ inP (false, cauchy-subset (isRegular Cc) $ later \lam {U} (inP (V,CV,U<=<V)) => inP (V, CV, join-right {PrecoverLattice X} {A} {B} U<=<V))
    }
  }
  | join-left => join-left {PrecoverLattice X}
  | join-right => join-right {PrecoverLattice X}
  | join-univ => join-univ {PrecoverLattice X}

\func RegPrecoverSpace (X : PrecoverSpace) : CoverSpace X
  => CompleteLattice.SJoin {CoverLattice X} \lam A => A <= {PrecoverLattice X} X

\func regPrecoverSpace {X : PrecoverSpace} : PrecoverMap X (RegPrecoverSpace X) \cowith
  | func x => x
  | func-cover d => CompleteLattice.SJoin-univ {PrecoverLattice X} {\lam A => A <= {PrecoverLattice X} X} (\lam p => p) $
      transport (isCauchy {RegPrecoverSpace X}) (ext \lam U => ext (\lam DU => inP (U, DU, idp), \lam (inP (V,DV,U=V)) => rewrite U=V DV)) d

\lemma regPrecoverSpace-extend {X : PrecoverSpace} {Y : CoverSpace} (f : PrecoverMap X Y) : PrecoverMap (RegPrecoverSpace X) Y f \cowith
  | func-cover {D} Dc => CompleteLattice.SJoin-cond {CoverLattice X} {\lam A => A <= {PrecoverLattice X} X} {CoverTransfer f} PrecoverTransfer-char $ func-cover {PrecoverTransfer-map f} Dc