------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------
-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Heterogeneous`.
{-#
OPTIONS
--cubical-compatible
--safe
#-}
module
Relation.Binary.Indexed.Heterogeneous.Definitions
where
open
import
Level
using
(
Level
)
import
Relation.Binary.Definitions
as
B
using
(
Reflexive
;
Symmetric
;
Transitive
;
Sym
;
Trans
)
open
import
Relation.Binary.Indexed.Heterogeneous.Core
using
(
IRel
)
private
variable
i
a
ℓ
:
Level
I
:
Set
i
------------------------------------------------------------------------
-- Simple properties of indexed binary relations
Reflexive
:
(
A
:
I
→
Set
a
)
→
IRel
A
ℓ
→
Set
_
Reflexive
_
_∼_
=
∀
{
i
}
→
B.Reflexive
(
_∼_
{
i
})
Symmetric
:
(
A
:
I
→
Set
a
)
→
IRel
A
ℓ
→
Set
_
Symmetric
_
_∼_
=
∀
{
i
j
}
→
B.Sym
(
_∼_
{
i
}
{
j
})
_∼_
Transitive
:
(
A
:
I
→
Set
a
)
→
IRel
A
ℓ
→
Set
_
Transitive
_
_∼_
=
∀
{
i
j
k
}
→
B.Trans
_∼_
(
_∼_
{
j
})
(
_∼_
{
i
}
{
k
})