------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------
-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Heterogeneous`.
{-#
OPTIONS
--cubical-compatible
--safe
#-}
open
import
Relation.Binary.Indexed.Heterogeneous.Core
module
Relation.Binary.Indexed.Heterogeneous.Structures
{
i
a
ℓ
}
{
I
:
Set
i
}
(
A
:
I
→
Set
a
)
(
_≈_
:
IRel
A
ℓ
)
where
open
import
Function.Base
using
(
id
;
_⟨_⟩_
)
open
import
Level
using
(
suc
;
_⊔_
)
open
import
Relation.Binary.Core
using
(
_⇒_
)
open
import
Relation.Binary.PropositionalEquality.Core
as
≡
using
(
_≡_
)
open
import
Relation.Binary.Indexed.Heterogeneous.Definitions
using
(
Reflexive
;
Symmetric
;
Transitive
)
------------------------------------------------------------------------
-- Equivalences
record
IsIndexedEquivalence
:
Set
(
i
⊔
a
⊔
ℓ
)
where
field
refl
:
Reflexive
A
_≈_
sym
:
Symmetric
A
_≈_
trans
:
Transitive
A
_≈_
reflexive
:
∀
{
i
}
→
_≡_
⟨
_⇒_
⟩
_≈_
{
i
}
reflexive
≡.refl
=
refl
record
IsIndexedPreorder
{
ℓ₂
}
(
_≲_
:
IRel
A
ℓ₂
)
:
Set
(
i
⊔
a
⊔
ℓ
⊔
ℓ₂
)
where
field
isEquivalence
:
IsIndexedEquivalence
reflexive
:
∀
{
i
j
}
→
(
_≈_
{
i
}
{
j
})
⟨
_⇒_
⟩
_≲_
trans
:
Transitive
A
_≲_
module
Eq
=
IsIndexedEquivalence
isEquivalence
refl
:
Reflexive
A
_≲_
refl
=
reflexive
Eq.refl