module Foo where

data Nat : Set where
  Z : Nat
  S : Nat → Nat

data _≡_ {A : Set} (a : A) : A → Set where
  Refl : a ≡ a

plus : Nat → Nat → Nat
plus Z n = n
plus (S n) m = S (plus n m)

record Addable (τ : Set) : Set where
 field
  _+_ : τ → τ → τ

open Addable {{...}}

record CommAddable (τ : Set) (a : Addable τ) : Set where
 field
  comm : (a b : τ) → (a + b) ≡ (b + a)

natAdd : Addable Nat
natAdd = record {_+_ = plus}

commAdd : CommAddable Nat natAdd
commAdd = record {comm = (λ a → λ b → ?)}

open CommAddable {{...}}

a : {x y : Nat} → (S (S Z) + (x + y)) ≡ ((x + y) + S (S Z))
a {x}{y} = comm (S (S Z)) (x + y)