Source code on Github
{-# OPTIONS --cubical-compatible #-}
module Class.HasAdd.Core where

open import Class.Prelude

record HasAdd (A : Type ℓ) : Type ℓ where
  infixl 6 _+_
  field _+_ : A → A → A

open HasAdd ⦃...⦄ public