\data UoM
   | unit
   | m | kg | s | A | K | mol | cd
   | mul UoM UoM
   | inv UoM
   | comm (x y : UoM) (i : I) \elim i {
      | left => mul x y
      | right => mul y x
   }
   | inv-inv (x : UoM) (i : I) \elim i {
      | left => inv (inv x)
      | right => x
   }
   | inv-mul (x : UoM) (i : I) \elim i {
      | left => mul x (inv x)
      | right => unit
   }
   | unit-left (x : UoM) (i : I) \elim i {
      | left => mul unit x
      | right => x
   }
   | assoc (x y z : UoM) (i : I) \elim i {
      | left => mul x (mul y z)
      | right => mul (mul x y) z
   }
   \where {
      \func div (x y : UoM) : UoM => mul x (inv y)
      \func sqr (x : UoM) : UoM => mul x x
   }

\record MyNat (unit : UoM) (val : Nat)
   \where {
      \func mk {u : UoM} (x : Nat) : MyNat u => \new MyNat u x

      \func \infixl 6 + {u : UoM} (x y : MyNat u) : MyNat u
         => mk (Nat.+ x.val y.val)

      \func \infixl 7 * {u v : UoM} (x : MyNat u) (y : MyNat v) : MyNat (UoM.mul u v)
         => mk (Nat.* x.val y.val)

      \func \infixl 7 / {u v : UoM} (x : MyNat u) (y : MyNat v) : MyNat (UoM.div u v)
         => mk (Nat.div x.val y.val)
   }

-- examples
\open MyNat

\func test1 : MyNat UoM.m => mk 5
\func test2 : MyNat UoM.s => mk 2

\func test3 : MyNat (UoM.div UoM.m UoM.s) => test1 / test2
-- \func test4 : MyNat {?} => test1 + test2 -- ???

\func N => UoM.mul UoM.kg (UoM.div UoM.m (UoM.sqr UoM.s))