------------------------------------------------------------------------
-- 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4