------------------------------------------------------------------------
-- The Agda standard library
--
-- Propositional (intensional) equality - Algebraic structures
------------------------------------------------------------------------

{-# 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

------------------------------------------------------------------------
-- Any operation forms a magma over _≡_

isMagma : (_∙_ : Op₂ A) → IsMagma _≡_ _∙_
isMagma _∙_ = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _∙_
  }

magma : (_∙_ : Op₂ A) → Magma _ _
magma _∙_ = record
  { isMagma = isMagma _∙_
  }