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