\import Data.Bool
\import Function.Meta
\import Logic
\import Logic.Meta
\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 Bounded(top,top-univ,bottom)
\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), Preorder.=_<= 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)) => \case rewrite e in Ux \with { | inP ((),_) } | (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, Preorder.=_<= 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 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} : 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)) } \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 | 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)
}

\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 \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 U<=V FU) | 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 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