\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 (
IsEmbedding,
\Pi {X : PrecoverSpace Dom} -> PrecoverMap X Cod func -> \Pi {C : Set (Set Dom)} -> isCauchy C -> X.isCauchy C,
\Pi {C : Set (Set Dom)} -> isCauchy C -> isCauchy {PrecoverTransfer func} C,
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