------------------------------------------------------------------------
-- The Agda standard library
--
-- Recomputable types and their algebra as Harrop formulas
------------------------------------------------------------------------
{-#
OPTIONS
--cubical-compatible
--safe
#-}
module
Relation.Nullary.Recomputable.Core
where
open
import
Agda.Builtin.Equality
using
(
_≡_
;
refl
)
open
import
Level
using
(
Level
)
open
import
Relation.Nullary.Irrelevant
using
(
Irrelevant
)
private
variable
a
:
Level
A
:
Set
a
------------------------------------------------------------------------
-- Definition
--
-- The idea of being 'recomputable' is that, given an *irrelevant* proof
-- of a proposition `A` (signalled by being a value of type `.A`, all of
-- whose inhabitants are identified up to definitional equality, and hence
-- do *not* admit pattern-matching), one may 'promote' such a value to a
-- 'genuine' value of `A`, available for subsequent eg. pattern-matching.
Recomputable
:
(
A
:
Set
a
)
→
Set
a
Recomputable
A
=
.
A
→
A
------------------------------------------------------------------------
-- Fundamental properties:
-- given `Recomputable A`, `recompute` is a constant function;
-- moreover, the identity, if `A` is propositionally irrelevant.
module
_
(
recompute
:
Recomputable
A
)
where
recompute-constant
:
(
p
q
:
A
)
→
recompute
p
≡
recompute
q
recompute-constant
_
_
=
refl
recompute-irrelevant-id
:
Irrelevant
A
→
(
a
:
A
)
→
recompute
a
≡
a
recompute-irrelevant-id
irr
a
=
irr
(
recompute
a
)
a