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