\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Operations
\import Order.Directed
\import Order.Lattice
\import Order.PartialOrder
\import Paths.Meta
\import Set.Subset
\import Topology.TopSpace

\instance TopSpaceHasProduct : HasProduct TopSpace
  | Product => ProductTopSpace

\instance ProductTopSpace (X Y : TopSpace) : TopSpace (\Sigma X Y)
  | isOpen W => ∀ {s : W} ∃ (U : X.isOpen) (U s.) (V : Y.isOpen) (V s.) ∀ {x : U} {y : V} (W (x,y))
  | open-top _ => inP (top, open-top, (), top, open-top, (), \lam _ _ => ())
  | open-inter {W} {W'} f g (Ws,W's) => \case f Ws, g W's \with {
    | inP (U,Uo,Ux,V,Vo,Vy,h), inP (U',U'o,U'x,V',V'o,V'y,h') => inP (U ∧ U', open-inter Uo U'o, (Ux,U'x), V ∧ V', open-inter Vo V'o, (Vy,V'y), \lam (Ux,U'x) (Vy,V'y) => (h Ux Vy, h' U'x V'y))
  }
  | open-Union So (inP (W,SW,Ws)) => \case So SW Ws \with {
    | inP (U,Uo,Ux,V,Vo,Vy,h) => inP (U, Uo, Ux, V, Vo, Vy, \lam Ux Vy => inP (W, SW, h Ux Vy))
  }
  \where {
    \open ContMap

    \func proj1 {X Y : TopSpace} : ContMap (X ⨯ Y) X \cowith
      | func s => s.
      | func-cont Uo => \lam Ux => inP (_, Uo, Ux, top, open-top, (), \lam Ux _ => Ux)

    \func proj2 {X Y : TopSpace} : ContMap (X ⨯ Y) Y \cowith
      | func s => s.
      | func-cont Uo => \lam Uy => inP (top, open-top, (), _, Uo, Uy, \lam _ Uy => Uy)

    \func tuple {X Y Z : TopSpace} (f : ContMap X Y) (g : ContMap X Z) : ContMap X (Y ⨯ Z) \cowith
      | func x => (f x, g x)
      | func-cont {W} Wo => X.cover-open \lam w => \case Wo w \with {
        | inP (U,Uo,Ufx,V,Vo,Vgx,h) => inP (_, open-inter (f.func-cont Uo) (g.func-cont Vo), (Ufx,Vgx), \lam (Ufx,Vgx) => h Ufx Vgx)
      }

    \func prod {X X' Y Y' : TopSpace} (f : ContMap X Y) (f' : ContMap X' Y') : ContMap (X ⨯ X') (Y ⨯ Y')
      => tuple (f ∘ proj1) (f' ∘ proj2)
      \where {
        \lemma isDense {X X' Y Y' : TopSpace} {f : ContMap X Y} {g : ContMap X' Y'} (fd : f.IsDense) (gd : g.IsDense) : ContMap.IsDense {prod f g}
          => \lam Uo Ux => \case Uo Ux \with {
            | inP (U1,U1o,U1x,U2,U2o,U2y,h) => \case fd U1o U1x, gd U2o U2y \with {
              | inP (_, inP (x',idp), U1fx'), inP (_, inP (y',idp), U2gy') => inP (_, inP ((x',y'), idp), h U1fx' U2gy')
            }
          }

        \lemma isWeaklyDense {X X' Y Y' : TopSpace} {f : ContMap X Y} {g : ContMap X' Y'} (fd : f.IsWeaklyDense) (gd : g.IsWeaklyDense) : ContMap.IsWeaklyDense {prod f g}
          => \lam Uo c (y,Uy) => \case Uo Uy \with {
            | inP (U1,U1o,U1y,U2,U2o,U2y,h) => fd U1o (\lam (_, inP (x1,idp), U1fx1) => gd U2o (\lam (_, inP (x2,idp), U2gx2) => c (_, inP ((x1,x2), idp), h U1fx1 U2gx2)) (y.,U2y)) (y.,U1y)
          }

        \lemma isEmbedding {X X' Y Y' : TopSpace} {f : ContMap X Y} {g : ContMap X' Y'} (fd : f.IsTopEmbedding) (gd : g.IsTopEmbedding) : ContMap.IsTopEmbedding {prod f g}
          => (topEmbedding-char {prod f g}). \lam Uo Uxy => \case Uo Uxy \with {
            | inP (U1,U1o,U1x,U2,U2o,U2y,h) => \case f.topEmbedding-char. fd U1o U1x, g.topEmbedding-char. gd U2o U2y \with {
              | inP (V1,V1o,V1fx,p1), inP (V2,V2o,V2gy,p2) => inP (Set.Prod V1 V2, Prod-open V1o V2o, (V1fx,V2gy), \lam (q1,q2) => h (p1 q1) (p2 q2))
            }
          }

        \lemma isDenseEmbedding {X X' Y Y' : TopSpace} {f : ContMap X Y} {g : ContMap X' Y'} (fd : f.IsDenseTopEmbedding) (gd : g.IsDenseTopEmbedding) : ContMap.IsDenseTopEmbedding {prod f g}
          => (isDense fd. gd., isEmbedding fd. gd.)
      }
  }

\lemma Prod-open {X Y : TopSpace} {U : Set X} (Uo : isOpen U) {V : Set Y} (Vo : isOpen V) : isOpen (Set.Prod U V)
  => \lam {s} (Us,Vs) => inP (U, Uo, Us, V, Vo, Vs, \lam Ux Vy => (Ux,Vy))

\lemma contAt-tuple {X Y Z : TopSpace} {f : X -> Y} {g : X -> Z} {x : X} (fc : IsContAt f x) (gc : IsContAt g x) : IsContAt (\lam x => (f x, g x)) x
  => \lam {W} Wo W0 => \case Wo W0 \with {
    | inP (U,Uo,Ufx,V,Vo,Vgx,g) => \case fc Uo Ufx, gc Vo Vgx \with {
      | inP (U',U'o,U'x,p), inP (V',V'o,V'x,q) => inP (U' ∧ V', open-inter U'o V'o, (U'x,V'x), MeetSemilattice.meet-monotone p q <=∘ \lam s => g s. s.)
    }
  }

\lemma limit-tuple {I : DirectedSet} {X Y : TopSpace} {f : I -> X} {x : X} (fl : X.IsLimit f x) {g : I -> Y} {y : Y} (gl : Y.IsLimit g y)
  : TopSpace.IsLimit (\lam n => (f n, g n)) (x,y)
  => \lam Wo Wxy => \case Wo Wxy \with {
    | inP (U,Uo,Ux,V,Vo,Vy,e) => \case fl Uo Ux, gl Vo Vy \with {
      | inP (N,Ne), inP (M,Me) => \case isDirected N M \with {
        | inP (K,N<=K,M<=K) => inP (K, \lam K<=n => e (Ne $ N<=K <=∘ K<=n) (Me $ M<=K <=∘ K<=n))
      }
    }
  }

\lemma cont2-limit {I : DirectedSet} {X Y Z : TopSpace} {f : I -> X} {g : I -> Y} {lx : X} {ly : Y}
                   (px : X.IsLimit f lx) (py : Y.IsLimit g ly) (h : ContMap (X ⨯ Y) Z) : Z.IsLimit (\lam n => h (f n, g n)) (h (lx,ly))
  => cont-limit (limit-tuple px py) h

\lemma denseSet_<= {X : TopSpace} {Y : HausdorffTopSpace} {P : JoinSemilattice Y} (jc : ContMap (Y ⨯ Y) Y \lam s => s. ∨ s.)
                   {S : Set X} (Sd : IsDenseSet S) (f g : ContMap X Y) (p : \Pi {x : X} -> S x -> f x <= g x) {x : X} : f x <= g x
  => join-left <=∘ =_<= (denseSet-lift-unique Sd (jc ContMap.∘ ProductTopSpace.tuple f g) g \lam Sx => <=-antisymmetric (join-univ (p Sx) <=-refl) join-right)

\lemma dense_<= {X Y : TopSpace} {Z : HausdorffTopSpace} {P : JoinSemilattice Z} (jc : ContMap (Z ⨯ Z) Z \lam s => s. ∨ s.)
                (f : ContMap X Y) (fd : f.IsDense) (g h : ContMap Y Z) (p : \Pi (x : X) -> g (f x) <= h (f x)) (y : Y) : g y <= h y
  => denseSet_<= jc fd g h \lam (inP (x,q)) => rewriteI q (p x)

\lemma weaklyDenseSet_<= {X : TopSpace} {Y : StronglyHausdorffTopSpace} {P : JoinSemilattice Y} (jc : ContMap (Y ⨯ Y) Y \lam s => s. ∨ s.)
                         {S : Set X} (Sd : IsWeaklyDenseSet S) (f g : ContMap X Y) (p : \Pi {x : X} -> S x -> f x <= g x) {x : X} : f x <= g x
  => join-left <=∘ =_<= (weaklyDenseSet-lift-unique Sd (jc ContMap.∘ ProductTopSpace.tuple f g) g \lam Sx => <=-antisymmetric (join-univ (p Sx) <=-refl) join-right)

\lemma weaklyDense_<= {X Y : TopSpace} {Z : StronglyHausdorffTopSpace} {P : JoinSemilattice Z} (jc : ContMap (Z ⨯ Z) Z \lam s => s. ∨ s.)
                      (f : ContMap X Y) (fd : f.IsWeaklyDense) (g h : ContMap Y Z) (p : \Pi (x : X) -> g (f x) <= h (f x)) (y : Y) : g y <= h y
  => weaklyDenseSet_<= jc fd g h \lam (inP (x,q)) => rewriteI q (p x)

\lemma hausdorff-char {X : TopSpace} : (\Pi {x y : X} -> ∀ {U V : isOpen} (U x) (V y) ∃ (U ∧ V) -> x = y) <-> (ProductTopSpace X X).IsClosed (\lam s => s. = s.)
  => (\lam f {s} sl => f \lam Uo Vo Us Vs => TruncP.map (sl (Prod-open Uo Vo) (Us,Vs)) \lam (t,p,(Ut,Vt)) => (t., (Ut, rewrite p Vt)),
      \lam f {x} {y} c => f {x,y} \lam {W} Wo Wxy => \case Wo Wxy \with {
        | inP (U,Uo,Ux,V,Vo,Vy,h) => \case c Uo Vo Ux Vy \with {
          | inP (z,(Uz,Vz)) => inP ((z,z), idp, h Uz Vz)
        }
      })