\import Logic
\import Logic.Meta
\import Operations
\import Order.Lattice
\import Set.Subset
\import Topology.TopSpace
\open Bounded(top)

\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 isEmbedding {X X' Y Y' : TopSpace} {f : ContMap X Y} {g : ContMap X' Y'} (fd : f.IsEmbedding) (gd : g.IsEmbedding) : ContMap.IsEmbedding {prod f g}
          => (embedding-char {prod f g}). \lam Uo Uxy => \case Uo Uxy \with {
            | inP (U1,U1o,U1x,U2,U2o,U2y,h) => \case f.embedding-char. fd U1o U1x, g.embedding-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.IsDenseEmbedding) (gd : g.IsDenseEmbedding) : ContMap.IsDenseEmbedding {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))