I want to define operation `(+)`

on types like `X -> ℕ`

or `X -> Y -> ℕ`

etc. where `X Y : Type`

. I want to use typeclasses for this but I’m not sure how to approach this correctly.

The current approach is problematic, here is what I have done:

I have defined typeclass `WithPlus X`

that contains a proof that addition can be and is defined on the type X. However, this brings the problem of proving `x+y = x+y`

if the plus on the left and right does not have the same proof `WithPlus X`

. I can prove uniqueness of this proof, i.e. `∀ (P Q : WithPlus X), P ≡ Q`

. However, I still have to manually rewrite all proofs to a single one and that is tedious.

I think that `SProp`

is exactly for this purpose, but I could not figure out how to use it in my case.

How can I deal with this problem? Is there a better way how to define addition on types like `X -> Y -> ℕ`

?

In this example, I just state the uniqueness of the proof as an axiom. I’m not sure if it can be proven here, but this is just a toy example and in my actual code I have proven the uniqueness.

**Full Code:**

```
Require Import MathClasses.interfaces.abstract_algebra.
Require Export MathClasses.implementations.NType_naturals.
Set Allow StrictProp.
Inductive CanHavePlus : Type -> Type :=
| nat_has_plus : CanHavePlus nat
| arrow_has_plus : forall X {Y}, CanHavePlus Y -> CanHavePlus (X -> Y).
Axiom CanHavePlus_uniq : forall {X : Type} (P Q : CanHavePlus X), P ≡ Q.
Fixpoint plus_rec `(P : CanHavePlus X) : X -> X -> X :=
match P with
| nat_has_plus => (fun n m : nat => n + m)
| @arrow_has_plus X' Y' P' => (fun f g : (X' -> Y') =>
fun x => plus_rec P' (f x) (g x))
end.
Class WithPlus (X : Type) := can_have_plus_proof : CanHavePlus X.
Instance RecPlus `{P : WithPlus X} : Plus X := plus_rec can_have_plus_proof.
Lemma problem `{P : WithPlus X} {Q : WithPlus X} : forall (x y : X), (@RecPlus _ P x y) ≡ (@RecPlus _ Q x y).
assert (P ≡ Q) by apply CanHavePlus_uniq.
rewrite H.
reflexivity.
Qed.
```