include "Universes.ma".

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

notation "(l,r)"
  non associative with precedence 90
  for @{ 'cartesian $l $r }.
  
interpretation "Cartesian product" 'cartesian l r = (mk_Cartesian ? ? l r).