\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Arith.Rat
\import Arith.Real.UpperReal
\import Function.Meta
\import Logic
\import Order.Biordered
\import Order.Lattice
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Topology.MetricSpace
\import Topology.UniformSpace.Product

\instance ManhattanProductPseudoMetricSpace (X Y : ExPseudoMetricSpace) : ExPseudoMetricSpace (\Sigma X Y)
  | UniformSpace => ProductUniformSpace X Y
  | dist s t => dist s. t. + dist s. t.
  | dist-refl => pmap2 (+) dist-refl dist-refl *> zro-left
  | dist-symm => pmap2 (+) dist-symm dist-symm
  | dist-triang => transport (_ <=) (+-assoc *> pmap (_ +) (inv +-assoc *> pmap (`+ _) +-comm *> +-assoc) *> inv +-assoc) $ <=_+ dist-triang dist-triang
  | dist-uniform => (\lam (inP (D,Du,E,Eu,r)) => \case dist-uniform. Du, dist-uniform. Eu \with {
    | inP (eps,eps>0,h1), inP (delta,delta>0,h2) => inP (eps ∧ delta, <_meet-univ eps>0 delta>0, \lam s => \case h1 s., h2 s. \with {
      | inP (V,DV,g1), inP (W,EW,g2) => \case r (inP (V,DV,W,EW,idp)) \with {
        | inP (U,CU,p) => inP (U, CU, \lam d => p (g1 $ transport (`<= _) zro-right (<=_+ <=-refl dist>=0) (ExUpperReal.U_<= d meet-left),
                                                   g2 $ transport (`<= _) zro-left (<=_+ dist>=0 <=-refl) (ExUpperReal.U_<= d meet-right)))
      }
    })
  }, \lam (inP (eps,eps>0,h)) => inP (_, X.metricUniform $ RatField.half>0 eps>0, _, Y.metricUniform $ RatField.half>0 eps>0,
       \lam {_} (inP (_, inP (x,idp), _, inP (y,idp), idp)) => \case h (x,y) \with {
         | inP (W,CW,g) => inP (W, CW, \lam {s} (d1,d2) => g $ ExUpperReal.+_U_<=. $ inP (_, d1, _, d2, linarith))
       }))