module Functions.Functions_vs_Sets where

open import Sets.Enumerated using (Bool; true; false)

Negation as a relation

Representation of negation as a relation between Bool and Bool:


data Not : Bool  Bool  Set where
  n₁ : Not true false
  n₂ : Not false true

This creates four new sets of which two are non-empty.

Not a b is non-empty iff b is the negated value of a.

Negation as a function

Recall the representation of negation as a function:


not : Bool  Bool
not true  = false
not false = true

Relations vs. functions

Relation's advantages:

Function's advantages:

Specification vs. implementation

Relations are good for describing the problem/question (specification).

Functions are good for describing the solution/answer (implementation).

Notes

Functions with Boolean value

Remark

An A → B → C function corresponds to specification A → B → C → Set according our previous remark. So _≤?_ : ℕ → ℕ → Bool would correspond to ℕ → ℕ → Bool → Set, but Boolean valued functions can be specified easier so we have _≤_ : ℕ → ℕ → Set as specification.