\import Data.Bool
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Operations
\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
\import Topology.TopSpace
\import Topology.TopSpace.Product
\open Bounded(top)
\open CoverMap
\open ClosurePrecoverSpace \hiding (closure-univ)
\open ProductCoverSpace

\instance CoverSpaceHasProduct : HasProduct CoverSpace
  | Product => ProductCoverSpace

\instance ProductCoverSpace (X Y : CoverSpace) : CoverSpace (\Sigma X Y)
  | TopSpace => ProductTopSpace X Y
  | isCauchy => isCauchy {Prod X Y}
  | cauchy-cover => cauchy-cover {Prod X Y}
  | cauchy-top => cauchy-top {Prod X Y}
  | cauchy-refine => cauchy-refine {Prod X Y}
  | cauchy-glue => cauchy-glue {Prod X Y}
  | isRegular Cc => closure-subset (isRegular {Prod X Y} Cc) \lam {V} (inP (U,CU,V<=<U)) => inP (U, CU, unfolds V<=<U)
  | cauchy-open => (\lam f {s} Ss => \case f Ss \with {
    | inP (U,Uo,Ux,V,Vo,Vy,h) => closure-subset (prodCover' (cauchy-open. Uo Ux) (cauchy-open. Vo Vy)) \lam {W} (inP (U',cU',V',cV',p)) => rewrite p \lam (U's,V's) {(x,y)} (U'x,V'y) => h (cU' U's U'x) (cV' V's V'y)
  }, \lam f Ss => \case prod-neighborhood' (PrecoverSpace.open-char. (later f) Ss) \with {
    | inP (U,V,x<=<U,y<=<V,h) => inP (_, X.interior {U}, x<=<U, _, Y.interior {V}, y<=<V, \lam c d => h (<=<_<= c idp) (<=<_<= d idp))
  })
  \where {
    \private \meta Prod X Y => CoverTransfer {\Sigma X Y} {X} __. ∨ CoverTransfer {\Sigma X Y} {Y} __.

    \private \func proj1' {X Y : CoverSpace} : CoverMap (Prod X Y) X \cowith
      | func s => s.
      | func-cover Dc => join-left {CoverLattice (\Sigma X Y)} $ func-cover {PrecoverTransfer-map {\Sigma X Y} __.} Dc

    \private \func proj2' {X Y : CoverSpace} : CoverMap (Prod X Y) Y \cowith
      | func s => s.
      | func-cover Dc => join-right {CoverLattice (\Sigma X Y)} $ func-cover {PrecoverTransfer-map {\Sigma X Y} __.} Dc

    \private \lemma prodCover' {X Y : CoverSpace} {C : Set (Set X)} (Cc : X.isCauchy C) {D : Set (Set Y)} (Dc : Y.isCauchy D)
      : isCauchy {Prod X Y} \lam W => ∃ (U : C) (V : D) (W = \lam s => \Sigma (U s.) (V s.))
      => cauchy-subset {Prod X Y} (cauchy-inter {Prod X Y} (proj1'.func-cover Cc) (proj2'.func-cover Dc))
          \lam (inP (U, V, inP (U',CU',p1), inP (V',DV',p2), q)) => inP $ later (U', CU', V', DV', q *> pmap2 (∧) p1 p2)

    \private \lemma prod-neighborhood' {X Y : CoverSpace} {x : X} {y : Y} {W : Set (\Sigma X Y)} (xy<=<W : single (x,y) <=< {Prod X Y} W) : ∃ (U : Set X) (V : Set Y) (single x <=< U) (single y <=< V) ∀ {x : U} {y : V} (W (x,y))
      => \case closure-filter (\new SetFilter {
                  | F W => ∃ (U : Set X) (V : Set Y) (single x <=< U) (single y <=< V) ∀ {x : U} {y : V} (W (x,y))
                  | filter-mono p (inP (U,V,x<=<U,y<=<V,q)) => inP (U, V, x<=<U, y<=<V, \lam Ux Vy => p (q Ux Vy))
                  | filter-top => inP (top, top, <=<_top, <=<_top, \lam _ _ => ())
                  | filter-meet (inP (U,V,x<=<U,y<=<V,q)) (inP (U',V',x<=<U',y<=<V',q')) => inP (U ∧ U', V ∧ V', RatherBelow.<=<_meet-same x<=<U x<=<U', RatherBelow.<=<_meet-same y<=<V y<=<V', \lam (Ux,U'x) (Vy,V'y) => (q Ux Vy, q' U'x V'y))
                }) (\case __ \with {
                      | inP (true, Dc) => \case CoverSpace.cauchy-regular-cover Dc x \with {
                        | inP (U, inP (W,CW,p), x<=<U) => inP (W, CW, inP (U, top, x<=<U, <=<_top, \lam Ux _ => p Ux))
                      }
                      | inP (false, Dc) => \case CoverSpace.cauchy-regular-cover Dc y \with {
                        | inP (V, inP (W,CW,p), y<=<V) => inP (W, CW, inP (top, V, <=<_top, y<=<V, \lam _ Vy => p Vy))
                      }
      }) xy<=<W \with {
        | inP (W, h, inP (U,V,x<=<U,y<=<V,q)) => inP (U, V, x<=<U, y<=<V, \lam Ux' Vy' => h ((x,y), (idp, q (<=<_<= x<=<U idp) (<=<_<= y<=<V idp))) (q Ux' Vy'))
      }

    \lemma proj1 {X Y : CoverSpace} : CoverMap (X ⨯ Y) X __.
      => proj1'

    \lemma proj2 {X Y : CoverSpace} : CoverMap (X ⨯ Y) Y __.
      => proj2'

    \func tuple {X Y Z : CoverSpace} (f : CoverMap Z X) (g : CoverMap Z Y) : CoverMap Z (X ⨯ Y) \cowith
      | func z => (f z, g z)
      | func-cover => func-cover {precover f g}
      \where {
        \func precover {Z : PrecoverSpace} {X Y : CoverSpace} (f : PrecoverMap Z X) (g : PrecoverMap Z Y) : PrecoverMap Z (X ⨯ Y) \cowith
          | func z => (f z, g z)
          | func-cover => closure-univ-cover $ later \case __ \with {
            | inP (true, Dc) => cauchy-refine (f.func-cover Dc) \lam (inP (V, inP (U',CU',q), p)) => inP (_, inP (U',CU',idp), \lam Ux => q $ rewrite p in Ux)
            | inP (false, Dc) => cauchy-refine (g.func-cover Dc) \lam (inP (V, inP (U',CU',q), p)) => inP (_, inP (U',CU',idp), \lam Ux => q $ rewrite p in Ux)
          }
      }

    \func prod {X Y X' Y' : CoverSpace} (f : CoverMap X Y) (g : CoverMap X' Y') : CoverMap (X ⨯ X') (Y ⨯ Y')
      => tuple (f ∘ proj1) (g ∘ proj2)
      \where {
        \lemma isEmbedding {X Y X' Y' : CoverSpace} {f : CoverMap X Y} {g : CoverMap X' Y'} (fe : f.IsEmbedding) (ge : g.IsEmbedding) : CoverMap.IsEmbedding {prod f g}
          => closure-embedding (\lam c => c) (prod f g) \case __ \with {
            | inP (true,  Dc) => closure $ inP (true,  cauchy-subset (fe Dc) \lam (inP (V, inP (W,CW,q), p)) => inP $ later (_, inP (W, CW, (\lam c => p c) <=∘ q), <=-refl))
            | inP (false, Dc) => closure $ inP (false, cauchy-subset (ge Dc) \lam (inP (V, inP (W,CW,q), p)) => inP $ later (_, inP (W, CW, (\lam c => p c) <=∘ q), <=-refl))
          }

        \lemma isDenseEmbedding {X X' Y Y' : CoverSpace} {f : CoverMap X Y} {g : CoverMap X' Y'} (fde : f.IsDenseEmbedding) (gde : g.IsDenseEmbedding) : CoverMap.IsDenseEmbedding {prod f g}
          => (ProductTopSpace.prod.isDense fde. gde., isEmbedding fde. gde.)
      }

    \lemma prod-neighborhood {X Y : CoverSpace} {x : X} {y : Y} {W : Set (\Sigma X Y)} : single (x,y) <=< {X ⨯ Y} W <-> ∃ (U : Set X) (V : Set Y) (single x <=< U) (single y <=< V) ∀ {x : U} {y : V} (W (x,y))
      => (\lam xy<=<W => prod-neighborhood' $ unfolds xy<=<W, \case \elim __ \with {
        | inP (U,V,x<=<U,y<=<V,h) => cauchy-subset {X ⨯ Y} (prodCover (unfolds in x<=<U) (unfolds in y<=<V)) \lam {_} (inP (U', Ug, V', Vg, idp)) =>
            later \lam s {z} t => h (Ug (s.., (pmap __. s.., s...)) t.) (Vg (s.., (pmap __. s.., s...)) t.)
      })

    \lemma prodCover {X Y : CoverSpace} {C : Set (Set X)} (Cc : X.isCauchy C) {D : Set (Set Y)} (Dc : Y.isCauchy D)
      : isCauchy {X ⨯ Y} \lam W => ∃ (U : C) (V : D) (W = \lam s => \Sigma (U s.) (V s.))
      => prodCover' Cc Dc
  }

\instance ProductSeparatedCoverSpace (X Y : SeparatedCoverSpace) : SeparatedCoverSpace (\Sigma X Y)
  | CoverSpace => ProductCoverSpace X Y
  | isSeparatedCoverSpace p => ext (
    isSeparatedCoverSpace \lam Cc => \case p (proj1.func-cover Cc) \with {
      | inP (U, inP (V,CV,q), s) => inP (V, CV, rewrite q in s)
    }, isSeparatedCoverSpace \lam Cc => \case p (proj2.func-cover Cc) \with {
      | inP (U, inP (V,CV,q), s) => inP (V, CV, rewrite q in s)
    })

\instance ProductCompleteCoverSpace (X Y : CompleteCoverSpace) : CompleteCoverSpace (\Sigma X Y)
  => complete-char   $ inP (ProductCoverSpace.tuple (completion-lift proj1) (completion-lift proj2),
                              \lam s => ext (completion-lift-char s, completion-lift-char s))

\func prodCF {X Y : CoverSpace} (F : CauchyFilter X) (G : CauchyFilter Y) : CauchyFilter (X ⨯ Y) \cowith
  | F W => ∃ (U : Set X) (F U) (V : Set Y) (G V) ∀ {x : U} {y : V} (W (x,y))
  | filter-mono p (inP (U,FU,V,GV,f)) => inP (U, FU, V, GV, \lam Ux Vy => p $ f Ux Vy)
  | filter-top => inP (top, filter-top, top, filter-top, \lam _ _ => ())
  | filter-meet (inP (U,FU,V,GV,f)) (inP (U',FU',V',GV',f')) => inP (U ∧ U', filter-meet FU FU', V ∧ V', filter-meet GV GV', \lam (Ux,U'x) (Vy,V'y) => (f Ux Vy, f' U'x V'y))
  | isProper (inP (U,FU,V,GV,f)) => \case isProper FU, isProper GV \with {
    | inP (x,Ux), inP (y,Vy) => inP ((x,y), f Ux Vy)
  }
  | isCauchyFilter => ClosurePrecoverSpace.closure-filter \this $ later \case __ \with {
    | inP (true, Dc) => \case F.isCauchyFilter Dc \with {
      | inP (V, inP (U,CU,q), FV) => inP (U, CU, inP (V, FV, top, filter-top, \lam Vx _ => q Vx))
    }
    | inP (false, Dc) => \case G.isCauchyFilter Dc \with {
      | inP (V, inP (U,CU,q), GV) => inP (U, CU, inP (top, filter-top, V, GV, \lam _ Vy => q Vy))
    }
  }

\instance PrecoverSpaceHasProduct : HasProduct PrecoverSpace
  | Product => ProductPrecoverSpace

\instance ProductPrecoverSpace (X Y : PrecoverSpace) : PrecoverSpace (\Sigma X Y)
  | isCauchy => isCauchy {Prod X Y}
  | cauchy-cover => cauchy-cover {Prod X Y}
  | cauchy-top => cauchy-top {Prod X Y}
  | cauchy-refine => cauchy-refine {Prod X Y}
  | cauchy-glue => cauchy-glue {Prod X Y}
  \where {
    \private \meta Prod X Y => PrecoverTransfer {\Sigma X Y} {X} __. ∨ PrecoverTransfer {\Sigma X Y} {Y} __.

    \func proj1 {X Y : PrecoverSpace} : PrecoverMap (Prod X Y) X \cowith
      | func s => s.
      | func-cover Dc => join-left {PrecoverLattice (\Sigma X Y)} $ func-cover {PrecoverTransfer-map {\Sigma X Y} __.} Dc

    \func proj2 {X Y : PrecoverSpace} : PrecoverMap (Prod X Y) Y \cowith
      | func s => s.
      | func-cover Dc => join-right {PrecoverLattice (\Sigma X Y)} $ func-cover {PrecoverTransfer-map {\Sigma X Y} __.} Dc

    \lemma prodCover {X Y : PrecoverSpace} {C : Set (Set X)} (Cc : X.isCauchy C) {D : Set (Set Y)} (Dc : Y.isCauchy D)
      : isCauchy {X ⨯ Y} \lam W => ∃ (U : C) (V : D) (W = \lam s => \Sigma (U s.) (V s.))
      => cauchy-subset {Prod X Y} (cauchy-inter {Prod X Y} (proj1.func-cover Cc) (proj2.func-cover Dc))
          \lam (inP (U, V, inP (U',CU',p1), inP (V',DV',p2), q)) => inP $ later (U', CU', V', DV', q *> pmap2 (∧) p1 p2)
  }

\lemma completion-lift-neighborhood2 {X Y : CoverSpace} {Z : CompleteCoverSpace} (g : CoverMap (X ⨯ Y) Z) (F : Completion X) (G : Completion Y) (W : Set Z)
  : single (dense-lift (prod completion completion) (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding) g (F,G)) <=< W <->
    ∃ (W' : Set Z) (W' <=< W) (V1 : Set X) (F V1) (V2 : Set Y) (G V2) (∀ {x : V1} {y : V2} (W' (g (x,y))))
  => <->trans (dense-lift-neighborhood (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding) (F,G) W) $ later
      (\lam (inP (W',W'<=<W,V,p,FG<=<V)) => \case prod-neighborhood. FG<=<V \with {
        | inP (V1,V2,F<=<V1,G<=<V2,g) => inP (W', W'<=<W, pointCF ^-1 V1, pointCF_^-1_<=< F<=<V1, pointCF ^-1 V2, pointCF_^-1_<=< G<=<V2, \lam V1x V2y => p $ g V1x V2y)
      }, \lam (inP (W',W'<=<W,V1,FV1,V2,GV2,h)) => inP (W', W'<=<W, Set.Prod (mkSet V1) (mkSet V2), \lam s => h (<=<_<= s. idp) (<=<_<= s. idp), prod-neighborhood. $
          inP (mkSet V1, mkSet V2, mkSet_<=<-point. FV1, mkSet_<=<-point. GV2, \lam p q => (p,q))))
  \where \open Completion