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