\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.Set
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.RatherBelow
\import Topology.TopSpace
\open Set

\func OpenCoverSpace {X : CoverSpace} {S : Set X} (So : X.isOpen S) : CoverSpace (Total S) \cowith
  | isCauchy => (C So).isCauchy
  | cauchy-cover => (C So).cauchy-cover
  | cauchy-top => (C So).cauchy-top
  | cauchy-refine => (C So).cauchy-refine
  | cauchy-glue => (C So).cauchy-glue
  | isRegular Cc => cauchy-subset ((C So).isRegular Cc) \lam {V} (inP (U,CU,V<=<U)) => inP $ later (U, CU, unfolds V<=<U)
  | TopSpace => TopSub S
  | cauchy-open {W} =>
    (\lam (inP (U,Uo,WU)) {x} Wx =>
       \have x<=<U => <=<-dir-aux So $ X.open-char. Uo (rewrite WU in Wx)
       \in closure-subset x<=<U \lam {V} h Vx {y} Vy => rewrite WU $ h (x, (idp, Vx)) Vy,
     \lam c => (TopSub S).cover-open \lam {x} Wx => inP
       (\lam y => single y. <=< extend W,
        TopSub-map.func-cont X.interior,
        <=<-conv-aux So (closure-subset (c Wx) $ later \lam {V} h (_,(idp,Vx)) => h Vx),
        \lam {y} y<=<W => (<=<_<= y<=<W idp).))
  \where {
    \open ClosurePrecoverSpace

    \private \meta C So => ClosureCoverSpace isBasicCover (basicCover-cover So) basicCover-regular

    \func isBasicCover {X : CoverSpace} {S : Set X} (C : Set (Set (Total S))) : \Prop
      => ∃ (D : Set (Set X)) (X.isCauchy D || RegularClosure (single (single S)) D) (C = \lam U => ∃ (V : D) (U = restrict V))

    \lemma basicCover-cover {X : CoverSpace} {S : Set X} (So : X.isOpen S) {C : Set (Set (Total S))} (Cc : isBasicCover C) (s : Total S) : ∃ (U : C) (U s) \elim Cc
      | inP (D, byLeft Dc, p) => \case cauchy-cover Dc s. \with {
        | inP (V,DV,Vs) => rewrite p $ inP (_, inP (V, DV, idp), Vs)
      }
      | inP (D, byRight Dr, p) => \case closure-neighborhood (\lam q => rewriteI q $ inP (S, idp, X.open-char. So s.)) Dr \with {
        | inP (U,DU,s<=<U) => rewrite p $ inP (_, inP (U, DU, idp), <=<_<= s<=<U idp)
      }

    \lemma basicCover-regular {X : CoverSpace} {S : Set X} {C : Set (Set (Total S))} (Cc : isBasicCover C) : Closure isBasicCover \lam V => ∃ (U : C) (Closure isBasicCover \lam W => Given (V ∧ W) -> W ⊆ U) \elim Cc
      | inP (D,Dc,p) => closure-subset (makeBasicCover $ ||.map isRegular (regular-closure-extends __ idp) Dc) \lam {V'} => \case \elim __ \with {
        | inP (V, inP (U,DU,V<=<U), V'=V) => inP (restrict U, rewrite p $ inP (U, DU, idp), closure-subset (makeBasicCover {X} $ byLeft V<=<U) \lam {W'} => \case \elim __ \with {
          | inP (W,h,W'=W) => rewrite (V'=V,W'=W) \lam (s,t) => h (s.,t) __
        })
      }

    \lemma makeBasicCover {X : CoverSpace} {S : Set X} {D : Set (Set X)} (e : X.isCauchy D || RegularClosure (single (single S)) D) : Closure isBasicCover \lam U => ∃ (V : D) (U = restrict V)
      => closure $ inP (D, e, idp)

    \truncated \data RegularClosure {X : CoverSpace} (A : Set (Set X) -> \Prop) (C : Set (Set X)) : \Prop
      | regular-closure (A C)
      | regular-closure-extends {D : Set (Set X)} (RegularClosure A D) (C = \lam V => ∃ (U : D) (V <=< U))

    \lemma closure-neighborhood {X : CoverSpace} {A : Set (Set X) -> \Prop} {x : X} (Ax : ∀ {C : A} ∃ (U : C) (single x <=< U)) {C : Set (Set X)} (CC : RegularClosure A C) : ∃ (U : C) (single x <=< U) \elim CC
      | regular-closure AC => Ax AC
      | regular-closure-extends CC p => \case closure-neighborhood Ax CC \with {
        | inP (U,DU,x<=<U) => \case <=<-inter x<=<U \with {
          | inP (V,x<=<V,V<=<U) => inP (V, rewrite p $ inP (U, DU, V<=<U), x<=<V)
        }
      }

    \func func {X : CoverSpace} {S : Set X} (So : X.isOpen S) : CoverMap (OpenCoverSpace So) X __. \cowith
      | func-cover Dc => makeBasicCover (byLeft Dc)

    \private \lemma <=<-dir-aux {X : CoverSpace} {S : Set X} (So : X.isOpen S) {x : Total S} {U : Set X} (x<=<U : single x. <=< U) : single x <=< {C So} restrict U
      => closure-subset (makeBasicCover (byLeft (unfolds in x<=<U))) $ later \lam {_} (inP (V, h, idp)) (_,(idp,Vx)) {y} Vy => h (x., (idp, Vx)) Vy

    \private \lemma <=<-conv-aux {X : CoverSpace} {S : Set X} (So : X.isOpen S) {x : Total S} {U : Set (Total S)} (x<=<U : single x <=< {C So} U) : single x. <=< extend U
      => \case closure-filter {C So} {isBasicCover} (\new SetFilter {
           | F V => single x. <=< extend V
           | filter-mono q p => <=<-left q (extend-mono p)
           | filter-top => <=<-left (X.open-char. So x.) \lam Sx => (Sx,())
           | filter-meet p q => rewrite extend_meet (RatherBelow.<=<_meet-same p q)
         }) (\case \elim __ \with {
           | inP (D,e,p) => \have (inP (V,DV,x<=<V)) : ∃ (V : D) (single x. <=< V) => \case \elim e \with {
             | byLeft Dc => CoverSpace.cauchy-regular-cover Dc x.
             | byRight Dr => closure-neighborhood (\lam q => rewriteI q $ inP (S, idp, X.open-char. So x.)) Dr
           } \in rewrite p $ inP (_, inP (V, DV, idp), RatherBelow.<=<_meet-same (X.open-char. So x.) x<=<V)
         }) x<=<U \with {
           | inP (V,h,x<=<V) => <=<-left x<=<V $ extend-mono $ h (x, (idp, transport V (ext idp) (<=<_<= x<=<V idp).))
         }

    \lemma <=<-dir {X : CoverSpace} {S : Set X} (So : X.isOpen S) {x : Total S} {U : Set X} (x<=<U : single x. <=< U) : single x <=< {OpenCoverSpace So} restrict U
      => unfolds (<=<-dir-aux So x<=<U)

    \lemma <=<-conv {X : CoverSpace} {S : Set X} (So : X.isOpen S) {x : Total S} {U : Set (Total S)} (x<=<U : single x <=< {OpenCoverSpace So} U) : single x. <=< extend U
      => <=<-conv-aux So (unfolds x<=<U)
  }

\func filter-extend {X : \Set} (U : Set X) (F : SetFilter (Total U)) : SetFilter X \cowith
  | F V => F \lam s => V s.
  | filter-mono q p => filter-mono q \lam c => p c
  | filter-top => filter-top
  | filter-meet c d => filter-meet c d

\func proper-filter-extend {X : \Set} (U : Set X) (F : ProperFilter (Total U)) : ProperFilter X \cowith
  | SetFilter => filter-extend U F
  | isProper c => \case F.isProper c \with {
    | inP (s,Us) => inP (s.,Us)
  }

\func cauchy-filter-extend {X : CoverSpace} {S : Set X} (So : X.isOpen S) (F : CauchyFilter (OpenCoverSpace So)) : CauchyFilter X \cowith
  | ProperFilter => proper-filter-extend S F
  | isCauchyFilter Cc => \case F.isCauchyFilter (OpenCoverSpace.makeBasicCover $ byLeft Cc) \with {
    | inP (U', inP (U,CU,U'=U), FU') => inP (U, CU, rewrite U'=U in FU')
  }

\func OpenCompleteCoverSpace {X : CompleteCoverSpace} {S : Set X} (So : X.isOpen S) : CompleteCoverSpace (Total S) \cowith
  | CoverSpace => OpenCoverSpace So
  | isSeparatedCoverSpace c => Separated-char.fromInj (func So) (\lam p => ext p) c
  | isComplete F =>
    \let | F' => cauchy-filter-extend So F
         | x => X.filter-point F'
         | (inP (U', inP (U, inP (_, idp, U<=<S), U'=U), FU')) => isCauchyFilter {F} $ makeBasicCover $ byRight $ regular-closure-extends (regular-closure idp) idp
    \in inP ((x, <=<_<= (X.filter-point-elem {F'} U<=<S $ rewrite U'=U in FU') idp), \lam {V'} x<=<V' => filter-mono (X.filter-point-sub (<=<-conv So x<=<V')) \lam s => transport V' (ext idp) s.)
  \where \open OpenCoverSpace

\func ClosedCoverSpace {X : CompleteCoverSpace} {S : Set X} (Sc : X.IsClosed S) : CompleteCoverSpace (Total S) \cowith
  | CoverSpace => CoverTransfer __.
  | isSeparatedCoverSpace f => ext $ isSeparatedCoverSpace \lam Cc => \case f (PrecoverTransfer.makeCauchy Cc) \with {
    | inP (_, inP (U,CU,idp), s) => inP (U, CU, s)
  }
  | isComplete F => \let G => \new CauchyFilter X {
      | F U => F (Set.restrict U)
      | filter-mono Fa p => filter-mono Fa (p __)
      | filter-top => filter-top
      | filter-meet => filter-meet
      | isProper FU => \case isProper FU \with {
        | inP (x,Ux) => inP (x., Ux)
      }
      | isCauchyFilter Cc => \case isCauchyFilter {F} (PrecoverTransfer.makeCauchy Cc) \with {
        | inP (_, inP (U, CU, idp), FU) => inP (U,CU,FU)
      }
    }
    | x => X.filter-point G
    \in inP ((x, Sc \lam {V} Vo VG => \case (X.filter-point-char {G} {V}). $ X.open-char. Vo VG \with {
      | inP (W,W<=<V,GW) => \case isProper GW \with {
        | inP ((x,Sx),Wx) => inP (x, Sx, <=<_<= W<=<V Wx)
      }
    }), \lam {V} c => \case X.cauchy-regular-cover c x \with {
      | inP (U, inP (W,h,p), x<=<U) => filter-mono (X.filter-point-sub x<=<U) (p <=∘ h (_, (idp, p $ <=<_<= x<=<U idp)))
    })
  \where {
    \protected \lemma conv {X : SeparatedCoverSpace} {S : Set X} (Sc : IsCompleteCoverSpace (CoverTransfer {Total S} __.)) : X.IsClosed S
      => \lam {x} h => \case IsCompleteCoverSpace.cauchyFilterToPoint Sc (later \new CauchyFilter {
        | F V => ∃ (U : Set X) (single x <=< U) (restrict U ⊆ V)
        | filter-mono (inP (U,x<=<U,q)) p => inP (U, x<=<U, q <=∘ p)
        | filter-top => inP (top, <=<_top, top-univ)
        | filter-meet (inP (U,x<=<U,p)) (inP (V,x<=<V,q)) => inP (U ∧ V, <=<-right (meet-univ <=-refl <=-refl) $ <=<_meet x<=<U x<=<V, MeetSemilattice.meet-monotone p q)
        | isProper (inP (V,x<=<V,p)) => \case h X.interior x<=<V \with {
          | inP (y,Sy,y<=<V) => inP ((y,Sy), p $ <=<_<= y<=<V idp)
        }
        | isCauchyFilter Cc => \case X.cauchy-regular-cover Cc x \with {
          | inP (V, inP (U,CU,p), x<=<V) => inP (U, CU, inP (V, x<=<V, p))
        }
      }) \with {
        | inP (s,p) => transport S (isSeparatedCoverSpace $ SeparatedCoverSpace.separated-char   \lam s<=<U x<=<V => later
            \case p $ <=<-right (\lam q => pmap __. q) $ unfolds in <=<_^-1 {_} {_} {PrecoverTransfer-map {Total S} __.} s<=<U \with {
              | inP (W,x<=<W,q) => \case h X.interior $ <=<-right (meet-univ <=-refl <=-refl) $ <=<_meet x<=<W x<=<V \with {
                | inP (y,Sy,y<=<WV) => inP (y, (q {y,Sy} (<=<_<= y<=<WV idp)., (<=<_<= y<=<WV idp).))
              }
            }) s.
      }
  }