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

\func OpenCoverSpace (X : CoverSpace) {S : Set X} (So : X.isOpen S) : CoverSpace (Total S)
  => ClosureCoverSpace isBasicCover basicCover-cover basicCover-regular
  \where {
    \open ClosurePrecoverSpace

    \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 {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 {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) : PrecoverMap (OpenCoverSpace X So) X __. \cowith
      | func-cover Dc => makeBasicCover (byLeft Dc)

    \lemma <=<-conv (X : CoverSpace) {S : Set X} (So : X.isOpen S) {x' : Total S} {U' : Set (Total S)} (x'<=<U' : single x' <=< {OpenCoverSpace X So} U') : single x'. <=< extend U'
      => \case closure-filter {OpenCoverSpace X 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).))
         }
  }

\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 X 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
  | SeparatedCoverSpace => Separated-char (OpenCoverSpace X So)   $ inP (X, func X So, \lam p => ext p)
  | isComplete F =>
    \let | F' => cauchy-filter-extend X 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 X So x<=<V')) \lam s => transport V' (ext idp) s.)
  \where \open OpenCoverSpace

\func ClosedCompleteCoverSpace {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.
      }
  }