```\import Function.Meta
\import Logic
\import Logic.Meta
\import Order.Lattice
\import Order.PartialOrder
\import Set.Subset
\import Topology.CoverSpace
\import Topology.TopSpace
\open Bounded(top)

\func TopCover {X : TopSpace} (Xr : X.IsRegular) : CoverSpace X \cowith
| isCauchy C => \Pi (x : X) -> ∃ (U : C) (V : X.isOpen) (V x) (V ⊆ U)
| cauchy-cover c x => \case c x \with {
| inP (U,CU,V,_,Vx,V<=U) => inP (U, CU, V<=U Vx)
}
| cauchy-top x => inP (top, idp, top, open-top, (), <=-refl)
| cauchy-refine f e x => \case f x \with {
| inP (U,CU,V,Vo,Vx,V<=U) => \case e CU \with {
| inP (W,DW,U<=W) => inP (W, DW, V, Vo, Vx, \lam c => U<=W \$ V<=U c)
}
}
| cauchy-glue f e x => \case f x \with {
| inP (U,CU,V,Vo,Vx,V<=U) => \case e CU x \with {
| inP (U',DUU',V',V'o,V'x,V'<=U') => inP (U ∧ U', inP (U, U', CU, DUU', idp), V ∧ V', open-inter Vo V'o, (Vx, V'x), MeetSemilattice.meet-monotone V<=U V'<=U')
}
}
| isRegular c x => \case c x \with {
| inP (U,CU,V,Vo,Vx,V<=U) => \case Xr Vo Vx \with {
| inP (W,Wo,Wx,W<=<V) => inP (W, inP (U, CU, \lam y => \case W<=<V y \with {
| inP (W',W'o,W'y,h) => inP (W', \lam s d => V<=U \$ h s d, W', W'o, W'y, <=-refl)
}), W, Wo, Wx, <=-refl)
}
}

\lemma top-cover-unit {X : TopSpace} {Xr : X.IsRegular} : ContMap X (TopCover Xr) (\lam x => x) \cowith
| func-cont c => X.cover-open \lam {x} Ux => \case c Ux x \with {
| inP (W,h,V,Vo,Vx,V<=W) => inP (V, Vo, Vx, \lam {y} Vy => h (V<=W Vx) (V<=W Vy))
}```