```\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.1) (V : Y.isOpen) (V s.2) ∀ {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.1
| 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.2
| 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}).2 \lam Uo Uxy => \case Uo Uxy \with {
| inP (U1,U1o,U1x,U2,U2o,U2y,h) => \case f.embedding-char.1 fd U1o U1x, g.embedding-char.1 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.1 gd.1, isEmbedding fd.2 gd.2)
}
}

\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))```