{-
`fold` is essentially the same as `if`/`then`/else` except as a function

Examples:

```
./fold True Natural 0 1 = 0

./fold False Natural 0 1 = 1
```
-}
    let fold
        : ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool
        =   λ(b : Bool)
          → λ(bool : Type)
          → λ(true : bool)
          → λ(false : bool)
          → if b then true else false

in  fold