{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.PropositionalEquality.Algebra where
open import Algebra.Bundles using (Magma)
open import Algebra.Core using (Op₂)
open import Algebra.Structures using (IsMagma)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong₂)
open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence)
private
variable
a : Level
A : Set a
isMagma : (_∙_ : Op₂ A) → IsMagma _≡_ _∙_
isMagma _∙_ = record
{ isEquivalence = isEquivalence
; ∙-cong = cong₂ _∙_
}
magma : (_∙_ : Op₂ A) → Magma _ _
magma _∙_ = record
{ isMagma = isMagma _∙_
}