module Functions.Functions_vs_Sets where

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

Now, that we have seen sets and functions, it may make sense to compare them and discuss the observed differences.

Negation as a relation

Recall how the logical negation can be represented as a relation between values of the Bool and Bool sets:

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

Note that this will create 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

Now consider the representation of the negation as a function:

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

Relations vs. functions

Benefits of using relations:

Benefits of using functions:

Specification vs. implementation


Functions with a Boolean value (predicates)

An A → B → C function corresponds to the specification A → B → C → Set according the previous remarks. That is, _≤?_ : ℕ → ℕ → Bool would correspond to ℕ → ℕ → Bool → Set, but actually it is easier to define Boolean-valued functions, so we have _≤_ : ℕ → ℕ → Set as specification.