------------------------------------------------------------------------
-- 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.Core
where
open
import
Level
using
(
Level
)
import
Relation.Binary.Core
as
B
using
(
Rel
;
REL
;
_⇒_
)
------------------------------------------------------------------------
-- Indexed binary relations
-- Heterogeneous types
IREL
:
∀
{
i₁
i₂
a₁
a₂
}
{
I₁
:
Set
i₁
}
{
I₂
:
Set
i₂
}
→
(
I₁
→
Set
a₁
)
→
(
I₂
→
Set
a₂
)
→
(
ℓ
:
Level
)
→
Set
_
IREL
A₁
A₂
ℓ
=
∀
{
i₁
i₂
}
→
A₁
i₁
→
A₂
i₂
→
Set
ℓ
-- Homogeneous types
IRel
:
∀
{
i
a
}
{
I
:
Set
i
}
→
(
I
→
Set
a
)
→
(
ℓ
:
Level
)
→
Set
_
IRel
A
ℓ
=
IREL
A
A
ℓ
------------------------------------------------------------------------
-- Generalised implication.
infixr
4
_=[_]⇒_
_=[_]⇒_
:
∀
{
a
b
ℓ₁
ℓ₂
}
{
A
:
Set
a
}
{
B
:
A
→
Set
b
}
→
B.Rel
A
ℓ₁
→
((
x
:
A
)
→
B
x
)
→
IRel
B
ℓ₂
→
Set
_
P
=[
f
]⇒
Q
=
∀
{
i
j
}
→
P
i
j
→
Q
(
f
i
)
(
f
j
)