```
module Functions.Views where

open import Data.Nat using (ℕ; zero; suc; _<_; _>_; s≤s; z≤n; _+_; _*_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)```

# Definition

Let `A` be a type.
Let `P : A → Set` a disjunction (parameterized on `A`).

A view on `A` is a function with type `(a : A) → P a`.

# Example

Assume the following definitions.

```
data Even : ℕ → Set
data Odd  : ℕ → Set

data Even where
zero : Even zero
odd  : ∀ {n} → Odd n → Even (suc n)

data Odd where
even : ∀ {n} → Even n → Odd (suc n)```

The parity view:

```
parity : ∀ n → Even n ⊎ Odd n
parity zero = inj₁ zero
parity (suc n) with parity n
parity (suc n) | inj₁ x = inj₂ (even x)
parity (suc n) | inj₂ y = inj₁ (odd y)```

# Exercise

The ordering view is a view on `ℕ × ℕ` (in curried form):

```
ordering : ∀ n m →  n < m  ⊎  n ≡ m  ⊎  n > m```

Define the ordering view!

# Individual constructors

The disjunction of the view can be replaced by an individual data type:

`Even n ⊎ Odd n` ~ `Parity n` where

```
data Parity : ℕ → Set where
even : ∀ n → Parity (n * 2)
odd  : ∀ n → Parity (1 + n * 2)```

`n < m ⊎ n ≡ m ⊎ n > m` ~ `Ordering n m` where

```
data Ordering : ℕ → ℕ → Set where
less    : ∀ m k → Ordering m (suc (m + k))
equal   : ∀ m   → Ordering m m
greater : ∀ m k → Ordering (suc (m + k)) m```

# Exercises

Define the functions

```
parity′ : ∀ n → Parity n```

```
compare : ∀ m n → Ordering m n```

# Usage of views

If we pattern match on `parity n` we learn not only whether `n` is even or odd but we also get a proof of it. From the proof we can get additional information too (like what is the half of `n`).

Views are very handy with the `with` construct.

# Exercises

1. Define division by 2 with the help of `Parity`:

```
⌊_/2⌋ : ℕ → ℕ      -- half (⌊ 1 /2⌋ = 0)```

1. Define congruence classes of 4 as a view on natural numbers!
Hint: use `Parity` when implementing the view function.