{-# OPTIONS --cubical-compatible #-}
module Class.HasAdd.Core where
 
open import Class.Prelude
 
record HasAdd (A : Type ℓ) : Type ℓ where
  infixl  _+_
  field _+_ : A → A → A
 
open HasAdd ⦃...⦄ public