------------------------------------------------------------------------
-- 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.Empty
open import Data.Product
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; sym; cong)
open PropEq.≡-Reasoning
import Relation.Nullary.Core as Core

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

open Core public using (¬_)

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

infix  _⇔_

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

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

open Core public using (Dec; yes; 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 }