record Point : Set where
  field
    x : Nat
    y : Nat

makePoint : Nat @$\rightarrow$@ Nat @$\rightarrow$@ Point
makePoint a b = record { x = a ; y = b }