------------------------------------------------------------------------
-- 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 _∙_
  }