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

makePoint : Nat -> Nat -> Point
makePoint a b = record { x = a ; y = b }