------------------------------------------------------------------------
-- The Agda standard library
--
-- Recomputable types and their algebra as Harrop formulas
------------------------------------------------------------------------
{-#
OPTIONS
--cubical-compatible
--safe
#-}
module
Relation.Nullary.Recomputable
where
open
import
Data.Empty
using
(
⊥
)
open
import
Data.Irrelevant
using
(
Irrelevant
;
irrelevant
;
[_]
)
open
import
Data.Product.Base
using
(
_×_
;
_,_
;
proj₁
;
proj₂
)
open
import
Level
using
(
Level
)
open
import
Relation.Nullary.Negation.Core
using
(
¬_
)
private
variable
a
b
:
Level
A
:
Set
a
B
:
Set
b
------------------------------------------------------------------------
-- Re-export
open
import
Relation.Nullary.Recomputable.Core
public
------------------------------------------------------------------------
-- Constructions
-- Irrelevant types are Recomputable
irrelevant-recompute
:
Recomputable
(
Irrelevant
A
)
irrelevant
(
irrelevant-recompute
[
a
]
)
=
a
-- Corollary: so too is ⊥
⊥-recompute
:
Recomputable
⊥
⊥-recompute
=
irrelevant-recompute
_×-recompute_
:
Recomputable
A
→
Recomputable
B
→
Recomputable
(
A
×
B
)
(
rA
×-recompute
rB
)
p
=
rA
(
p
.
proj₁
)
,
rB
(
p
.
proj₂
)
_→-recompute_
:
(
A
:
Set
a
)
→
Recomputable
B
→
Recomputable
(
A
→
B
)
(
A
→-recompute
rB
)
f
a
=
rB
(
f
a
)
Π-recompute
:
(
B
:
A
→
Set
b
)
→
(∀
x
→
Recomputable
(
B
x
))
→
Recomputable
(∀
x
→
B
x
)
Π-recompute
B
rB
f
a
=
rB
a
(
f
a
)
∀-recompute
:
(
B
:
A
→
Set
b
)
→
(∀
{
x
}
→
Recomputable
(
B
x
))
→
Recomputable
(∀
{
x
}
→
B
x
)
∀-recompute
B
rB
f
=
rB
f
-- Corollary: negations are Recomputable
¬-recompute
:
Recomputable
(
¬
A
)
¬-recompute
{
A
=
A
}
=
A
→-recompute
⊥-recompute