include "logic/pts.ma".

nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝
{
  first: A;
  second: B
}.