@MISC{MEASUR14.MIZ,
  AUTHOR = {Endou, Noboru and Shidama, Yasunari},
  TITLE = {Universality of Measure Space},
  DAY = {9},
  MONTH = {December},
  YEAR = {2024},
  ADDRESS1 = {National Institute of Technology, Gifu College\\2236-2 Kamimakuwa, Motosu, Gifu, Japan},
  ADDRESS2 = {Karuizawa Hotch 244-1 Nagano, Japan},
  SECTION1 = {Universality of Cartesian Product Type Sets and Tuple Type Sets},
  SECTION2 = {Integral on a Tuple Type Set (one-dimensional)},
  SECTION3 = {Integral over Tuple Type Sets ($n$-dimensional)},
  SECTION4 = {Lebesgue Type Measure and Lebesgue Integral on REAL n},  
  SUMMARY = {In this paper, we prove the interconversion between 
  Cartesian product types and tuple types and their integration for measures in higher dimensional spaces.
  In Mizar, two types of representations are mainly used for higher-dimensional sets: 
  those using direct products and those using tuples. The direct product type is suitable for 
  recursively extending from lower dimensions to higher dimensions, but is not suitable for 
  representations of general orders such as $n$-dimensional. The tuple type compensates for 
  this disadvantage and is also used as the domain of multivariable functions. 
   However, the direct relationship (universality) between Cartesian product type 
  and tuple type has not yet been demonstrated.\par
  In this paper, we prove the universality between Cartesian product type and tuple 
  type, and construct a measure on the set of tuple types \cite{Leinster:2014} and 
  \cite{aliprantis2006infinite}. We then show that the integral over the Cartesian product 
   type coincides with the integral over the set of tuple types.},
  ACKNOWLEDGEMENT = {This work was supported by JSPS KAKENHI 23K11242.}}
  
@BOOK{Leinster:2014,
 AUTHOR = {Leinster, Tom},
 TITLE = {Basic Category Theory},
 PUBLISHER = {Cambridge University Press},
 YEAR = {2014}}
