------------------------------------------------------------------------
-- 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