\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Function.Meta
\import Logic
\import Meta
\import Operations
\import Paths
\import Paths.Meta
\import Set.Subset
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.CoverSpace.Product
\import Topology.TopAbGroup
\import Topology.TopSpace
\import Topology.TopSpace.Product
\import Topology.UniformSpace.Product

\instance ProductTopAbGroup (X Y : TopAbGroup) : TopAbGroup (\Sigma X Y)
  | UniformSpace => ProductUniformSpace X Y
  | zro => (, )
  | + s t => (s. + t., s. + t.)
  | zro-left => ext (zro-left, zro-left)
  | +-assoc => ext (+-assoc, +-assoc)
  | negative s => (negative s., negative s.)
  | negative-left => ext (negative-left, negative-left)
  | +-comm => ext (+-comm, +-comm)
  | +-cont => \new ContMap {
    | func-cont {W} f {(s,t)} Wst => \case f Wst \with {
      | inP (U,Uo,Ust,V,Vo,Vst,g) => \case +-cont.func-cont Uo {s.,t.} Ust, +-cont.func-cont Vo {s.,t.} Vst \with {
        | inP (U1,U1o,U1s1,V1,V1o,V1t1,f1), inP (U2,U2o,U2s2,V2,V2o,V2t2,f2) => inP (Set.Prod U1 U2, Prod-open U1o U2o, (U1s1,U2s2), Set.Prod V1 V2, Prod-open V1o V2o, (V1t1,V2t2), \lam c d => g (f1 c. d.) (f2 c. d.))
      }
    }
  }
  | negative-cont => \new ContMap {
    | func-cont {W} f {(s,t)} Wst => \case f Wst \with {
      | inP (U,Uo,Us,V,Vo,Vt,g) => inP (_, negative-cont.func-cont Uo, Us, _, negative-cont.func-cont Vo, Vt, g __ __)
    }
  }
  | neighborhood-uniform => (
    \case \elim __ \with {
      | inP (D,Du,E,Eu,r) => \case neighborhood-uniform. Du, neighborhood-uniform. Eu \with {
        | inP (U,Uo,U0,f), inP (V,Vo,V0,g) => inP (Set.Prod U V, Prod-open Uo Vo, (U0,V0), \lam (x,y) => \case f x, g y \with {
          | inP (U',DU',h1), inP (V',EV',h2) => \case r $ inP (U',DU',V',EV',idp) \with {
            | inP (W,CW,p) => inP (W, CW, \lam c => p (h1 c., h2 c.))
          }
        })
      }
    }, \case \elim __ \with {
      | inP (W,Wo,W0,h) => \case Wo W0 \with {
        | inP (U,Uo,U0,V,Vo,V0,g) => inP (_, X.makeUniform Uo U0, _, Y.makeUniform Vo V0, \lam {_} (inP (_, inP (x,idp), _, inP (y,idp), idp)) => \case h (x,y) \with {
          | inP (W',CW',h') => inP (W', CW', \lam {s} (c,d) => h' $ g c d)
        })
      }
    })

\instance TopAbGroupHasProduct : HasProduct TopAbGroup
  | Product => ProductTopAbGroup

\lemma negative-uniform {X : TopAbGroup} : TopAbGroupMap X X negative \cowith
  | func-+ => X.negative_+ *> +-comm
  | func-cont => negative-cont.func-cont

\lemma +-uniform {X : TopAbGroup} : TopAbGroupMap (X ⨯ X) X \lam s => s. + s. \cowith
  | func-+ => equation
  | func-cont => +-cont.func-cont

\lemma BigSum-cover {X : CoverSpace} {Y : TopAbGroup} (fs : Array (CoverMap X Y))
  : CoverMap X Y \lam x => Y.BigSum \lam j => fs j x \elim fs
  | nil => CoverMap.const 
  | f :: fs => +-uniform CoverMap.∘ ProductCoverSpace.tuple f (BigSum-cover fs)