```------------------------------------------------------------------------
-- Operations on nullary relations (like negation and decidability)
------------------------------------------------------------------------

-- Some operations on/properties of nullary relations, i.e. sets.

module Relation.Nullary where

open import Data.Product
open import Data.Sum
open import Data.Empty
open import Data.Function
open import Data.Bool

open import Relation.Nullary.Core public
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

------------------------------------------------------------------------
-- Equivalence

infix 4 _⇔_

_⇔_ : Set → Set → Set
P ⇔ Q = (P → Q) × (Q → P)

------------------------------------------------------------------------
-- Negation

contradiction : ∀ {P whatever} → P → ¬ P → whatever
contradiction p ¬p = ⊥-elim (¬p p)

contravariant : ∀ {P Q} → (P → Q) → ¬ Q → ¬ P
contravariant f ¬q p = contradiction (f p) ¬q

-- Note also the following use of flip:

private
note : ∀ {P Q} → (P → ¬ Q) → Q → ¬ P
note = flip

-- And the following use of contradiction:

private
¬¬-add : {P : Set} → P → ¬ ¬ P

¬¬-map : ∀ {P Q} → (P → Q) → ¬ ¬ P → ¬ ¬ Q
¬¬-map f = contravariant (contravariant f)

¬¬-push : {P : Set} {Q : P → Set} →
¬ ¬ ((x : P) → Q x) → (x : P) → ¬ ¬ Q x
¬¬-push ¬¬P⟶Q P ¬Q = ¬¬P⟶Q (λ P⟶Q → ¬Q (P⟶Q P))

¬¬-drop : {P : Set} → ¬ ¬ ¬ P → ¬ P
¬¬-drop ¬¬¬P P = ¬¬¬P (λ ¬P → ¬P P)

¬¬-drop-Dec : {P : Set} → Dec P → ¬ ¬ P → P
¬¬-drop-Dec (yes p) ¬¬p = p
¬¬-drop-Dec (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p)

-- A double-negation-translated variant of excluded middle.

excluded-middle : {P : Set} → ¬ ¬ Dec P
excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))

-- Double-negation is a monad (if we assume that all elements of ¬ ¬ P
-- are equal).

; _>>=_  = λ x f → ¬¬-drop (¬¬-map f x)
}

-- Call with current continuation in the double-negation monad, or, if
-- you will, a double-negation translation of Peirce's law.

call/cc : ∀ {P whatever} →
((P → ¬ ¬ whatever) → ¬ ¬ P) → ¬ ¬ P
call/cc hyp ¬p = hyp (λ p _ → ¬p p) ¬p

∃⟶¬∀¬ : {A : Set} {P : A → Set} →
∃ P → ¬ (∀ x → ¬ P x)
∃⟶¬∀¬ = flip Σ-uncurry

∀⟶¬∃¬ : {A : Set} {P : A → Set} →
(∀ x → P x) → ¬ ∃ λ x → ¬ P x
∀⟶¬∃¬ ∀xPx (x , ¬Px) = ¬Px (∀xPx x)

¬∃⟶∀¬ : {A : Set} {P : A → Set} →
¬ ∃ (λ x → P x) → ∀ x → ¬ P x
¬∃⟶∀¬ = Σ-curry

∀¬⟶¬∃ : {A : Set} {P : A → Set} →
(∀ x → ¬ P x) → ¬ ∃ (λ x → P x)
∀¬⟶¬∃ = Σ-uncurry

∃¬⟶¬∀ : {A : Set} {P : A → Set} →
∃ (λ x → ¬ P x) → ¬ (∀ x → P x)
∃¬⟶¬∀ = flip ∀⟶¬∃¬

------------------------------------------------------------------------
-- Decidable relations

decToBool : ∀ {P} → Dec P → Bool
decToBool (yes _) = true
decToBool (no  _) = false

True : ∀ {P} → Dec P → Set
True Q = T (decToBool Q)

False : ∀ {P} → Dec P → Set
False Q = T (not (decToBool Q))

witnessToTruth : ∀ {P} {Q : Dec P} → True Q → P
witnessToTruth {Q = yes p} _  = p
witnessToTruth {Q = no  _} ()

------------------------------------------------------------------------
-- Injections

-- I cannot be bothered to generalise to an arbitrary setoid.

Injective : ∀ {A B} → (A → B) → Set
Injective f = ∀ {x y} → f x ≡ f y → x ≡ y

_LeftInverseOf_ : ∀ {A B} → (B → A) → (A → B) → Set
f LeftInverseOf g = ∀ x → f (g x) ≡ x

record Injection A B : Set where
field
to        : A → B
injective : Injective to

record LeftInverse A B : Set where
field
to           : A → B
from         : B → A
left-inverse : from LeftInverseOf to

injective : Injective to
injective {x} {y} eq = begin
x            ≡⟨ ≡-sym (left-inverse x)  ⟩
from (to x)  ≡⟨ ≡-cong from eq ⟩
from (to y)  ≡⟨ left-inverse y ⟩
y            ∎

injection : Injection A B
injection = record { to = to; injective = injective }
```