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