------------------------------------------------------------------------
-- The Agda standard library
--
-- The basic code for equational reasoning with a single relation
------------------------------------------------------------------------
{-#
OPTIONS
--cubical-compatible
--safe
#-}
open
import
Level
using
(
_⊔_
)
open
import
Function.Base
using
(
case_of_
)
open
import
Relation.Binary.Core
using
(
Rel
;
_⇒_
)
open
import
Relation.Binary.Definitions
using
(
Reflexive
;
Transitive
;
Trans
)
open
import
Relation.Binary.PropositionalEquality.Core
as
≡
using
(
_≡_
)
open
import
Relation.Binary.Reasoning.Syntax
module
Relation.Binary.Reasoning.Base.Single
{
a
ℓ
}
{
A
:
Set
a
}
(
_∼_
:
Rel
A
ℓ
)
(
refl
:
Reflexive
_∼_
)
(
trans
:
Transitive
_∼_
)
where
------------------------------------------------------------------------
-- Definition of "related to"
-- This seemingly unnecessary type is used to make it possible to
-- infer arguments even if the underlying equality evaluates.
infix
4
_IsRelatedTo_
data
_IsRelatedTo_
(
x
y
:
A
)
:
Set
ℓ
where
relTo
:
(
x∼y
:
x
∼
y
)
→
x
IsRelatedTo
y
start
:
_IsRelatedTo_
⇒
_∼_
start
(
relTo
x∼y
)
=
x∼y
∼-go
:
Trans
_∼_
_IsRelatedTo_
_IsRelatedTo_
∼-go
x∼y
(
relTo
y∼z
)
=
relTo
(
trans
x∼y
y∼z
)
≡-go
:
Trans
_≡_
_IsRelatedTo_
_IsRelatedTo_
≡-go
x≡y
(
relTo
y∼z
)
=
relTo
(
case
x≡y
of
λ
where
≡.refl
→
y∼z
)
stop
:
Reflexive
_IsRelatedTo_
stop
=
relTo
refl
------------------------------------------------------------------------
-- Reasoning combinators
open
begin-syntax
_IsRelatedTo_
start
public
open
≡-syntax
_IsRelatedTo_
≡-go
public
open
∼-syntax
_IsRelatedTo_
_IsRelatedTo_
∼-go
public
open
end-syntax
_IsRelatedTo_
stop
public