record Num (A : Set) : Set where
  field
    +-id : A
    *-id : A
    _+_ : A -> A -> A
    _-_ : A -> A -> A
    _*_ : A -> A -> A


toFuncNum : ∀ {A : Set} (num : Num A) -> Num (A -> A)
toFuncNum record { +-id = +-id ; *-id = *-id ; _+_ = _+_ ; _-_ = _-_ ; _*_ = _*_ }
   = record { +-id = const +-id
            ; *-id = const *-id
            ; _+_ = \f g x -> f x + g x
            ; _-_ = \f g x -> f x - g x
            ; _*_ = \f g x -> f x * g x
            }