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

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