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