I previously showed a single proof in logic, type theory, and category theory, and some fun classical logic proofs in Haskell, thanks to the Curry-Howard correspondence.

This post will go a bit further than that and show the type theoretic equivalents of existential and universal quantifiers. I’ll then explore some interesting properties of these types. This post will not go into the category theory part of this, although I may do that in a future post.

Forall (∀) is the universal quantifier and is generally written as

```
∀ x. P x
```

where `x`

is a variable and `P`

is a predicate taking such a variable. A basic
example of such a proposition could be: *“For all numbers x, if you add one to
x, you get a greater number than x”*, or:

```
∀ x. x + 1 > x
```

Similarly, exists (∃) is the existential quantifier and is written as

```
∃ x. P x
```

where `x`

is a variable and `P`

is a predicate, for example: *“there exists a
number that is greater than 10”*, or:

```
∃ x. x > 10
```

Please note that in classical logic, you can prove an existential proposition by
either finding an `x`

for which `P(x)`

is *true*, or by assuming there does not
exist such an `x`

and reaching a contradiction
(proof by contradiction).
In *intuitionistic* logic, the latter is not possible: we have to find the `x`

.
One could then say that an existential quantifier in intuitionistic logic is
described by a pair of `x`

and `P(x)`

.

In the next chapter, we will look at dependent sum and I will say it’s the
Curry-Howard correspondent of existential quantifiers. Most theorem provers that
rely on this correspondence will use make use of
proof irrelevance
which essentially means that it should not matter whether one picks `11`

or `12`

in order to to prove `∃ x. x > 10`

: the proofs should be equivalent. We will not
look into this, nor will we make use of proof irrelevance in this post.

Dependent sums (Σ) are the type theoretic equivalent of existential quantifiers. In Agda, we can define the dependent sum type as:

```
data Σ {A : Set} (P : A → Set) : Set where
Σ_intro : ∀ (a : A) → P a → Σ P
```

The ∑ type is a higher-kinded type which takes a higher-kinded type,
`P : A → Set`

– `P`

takes an `A`

and gives us a new type (`Set`

, in Agda). The
nice part about this is that `P`

holds information about both the type of the
existential variable (`A`

) as well as the type of the resulting type (`P A`

).

Constructing such a term requires a term of the existential type (*evidence* for
`A`

), and a term of the predicate type (*evidence* for `P A`

). For example, the
example above could be written as `∑_intro 11 (11 > 10)`

, assuming there
exists a type `>`

which expresses the greater-than relationship.

Please note that the above example is a simplification and going into the
details of how an inductive type for `>`

works is beyond the scope of this post.

Dependent products (∏) are the type theoretic equivalent of universal quantifiers. In Agda, we can define the dependent product type as:

```
data Π {A : Set} (P : A → Set) : Set where
Π_intro : (∀ (a : A) → P a) → Π P
```

The ∏ type is also a higher-kinded type. Note that this definition is almost
identical to the Σ definition, except for the parantheses used in the
constructor (`Π_intro`

). This lines up with the intuition that `∀x. P(X)`

can
be described by a function `A -> P(x)`

, where `x : A`

.

Constructing a ∏ type takes a function from the quantified variable to the type described by the predicate.

Constructing a term would, for example be `∏_intro (λn. n + 1 > n)`

.

We will first need to define a `constT`

function:

```
constT : ∀ (X : Set) (Y : Set) → Y → Set
constT x _ _ = x
```

This takes two types, `X`

and `Y`

. It then takes a value of type `Y`

, and
ignores it, returning the type `X`

.

So, if we take `P`

to *not* depend on the quantified item and define it using
`constT`

, then we can obtain tuples in the case of ∑ types:

```
Σ-pair : ∀ (A B : Set) → Set
Σ-pair a b = Σ (constT b a)
```

Note that `Σ-pair`

is a type-level function that takes two types and returns the
type of pairs.

We can then define a simple pair constructor using the constructor above:

```
Σ-mkPair : ∀ {A : Set} {B : Set} → A → B → Σ-pair A B
Σ-mkPair a b = Σ_intro a b
```

And we can have the two projections by simple pattern match, returning the appropriate value:

```
Σ-fst : ∀ {A B : Set} → Σ-pair A B → A
Σ-fst (Σ_intro a _) = a
Σ-snd : ∀ {A B : Set} → Σ-pair A B → B
Σ-snd (Σ_intro _ b) = b
```

This works because Σ types are defined as `a -> P a -> Σ P`

, so if we take a
`P`

such that `P a`

always is `b`

, then we get `a -> b -> Σ`

which is
essentially a tuple of `a`

and `b`

.

We can now say `Σ_snd (Σ_mkPair 1 2)`

and get the result `2`

.

Similarly, if we take `P`

to be `const B A`

, we can obtain functions out of
∏ types:

```
Π-function : ∀ (A B : Set) → Set
Π-function a b = Π (constT b a)
Π-mkFunction : ∀ {A B : Set} → (A → B) → Π-function A B
Π-mkFunction f = Π_intro f
Π-apply : ∀ {A B : Set} → Π-function A B → A → B
Π-apply (Π_intro f) a = f a
```

As with sum types, this works because Π types are defined as `(a -> P a) -> Π P`

,
so if we take `P`

such that `P a`

always is `b`

, then we get `(a -> b) -> Π`

,
which is essentially a function from `a`

to `b`

.

We can now write `Π-apply (Π-mkFunction (λx. x + 1)) 1`

and get the result `2`

.

We can obtain sum types from ∑ types by using `Bool`

as the variable type, and
the predicate *returning* type `A`

for `true`

, and type `B`

for `false`

:

```
bool : ∀ (A B : Set) → Bool → Set
bool a _ true = a
bool _ b false = b
```

Note that `a`

and `b`

are types! We can now write:

```
Σ-sum : ∀ (A B : Set) → Set
Σ-sum a b = Σ (bool a b)
```

Now, in order to construct such a type (via *left* or *right*), we just need
to pass the appropriate boolean value along with an item of the correct type:

```
Σ-sum_left : ∀ {A : Set} (B : Set) → A → Σ-sum A B
Σ-sum_left _ a = Σ_intro true a
Σ-sum_right : ∀ {B : Set} (A : Set) → B → Σ-sum A B
Σ-sum_right _ b = Σ_intro false b
```

Eliminating is just a matter of pattern matching on the boolean value and applying the correct function:

```
Σ-sum_elim : ∀ {A B R : Set} → (A → R) → (B → R) → Σ-sum A B → R
Σ-sum_elim f _ (Σ_intro true a) = f a
Σ-sum_elim _ g (Σ_intro false b) = g b
```

As an example, `Σ-sum_elim (const "left") (const "right") (Σ-sum_left Bool 1)`

,
and get the result `"left"`

.

Interestingly, we can also obtain sum types from ∏ types: the idea is to encode the eliminator right into our type! For that we will need the following predicate:

```
prodPredicate : ∀ (A B R : Set) → Set
prodPredicate a b r = (a → r) → (b → r) → r
```

This means that given two types `A`

and `B`

, we get a type-level function from
`R`

to `(A -> R) -> (B -> R) -> R`

, which is exactly the eliminator type. Don’t
worry about `Set₁`

or `Π'`

for now:

```
Π-sum : ∀ (A B : Set) → Set₁
Π-sum a b = Π' (prodPredicate a b)
```

This means that in order to build a sum type, we need to pass a type `R`

and
a function `(A -> R) -> (B -> R) -> R`

. So, the constructors will look like:

```
Π-sum-left : ∀ {A : Set} (B : Set) → A → Π-sum A B
Π-sum-left _ a = Π'_intro (\_ f _ → f a)
```

The lambda is the only interesting bit: we construct a function that given a
type `R`

(first `_`

) and a function `A -> R`

(named `f`

), we can return an `R`

by calling `f a`

(the third `_`

parameter is for the function `g : B -> R`

,
which is not required for the *left* constructor).

Similarly, we can write a constructor for *right*:

```
Π-sum-right : ∀ {A : Set} (B : Set) → B → Π-sum A B
Π-sum-right _ b = Π'_intro (\_ _ g → g b)
```

As for the eliminator, we simply require the two functions `A -> R`

and `B -> R`

in order to pass to our dependent product and get an `R`

:

```
Π-sum-elim : ∀ {A B R : Set} → (A → R) → (B → R) → Π-sum A B → R
Π-sum-elim f g (Π'_intro elim) = elim _ f g
```

We’ve used three type-level functions to generate a few interesting types:

Function | Σ-type | Π-type |
---|---|---|

constT | tuple | function |

bool | either | tuple |

prodPredicate | - | either |

What other interesting type-level functions can you find for Σ and/or Π types?

You can find the source file here.

Questions? Comments? Tweet them,
or post an issue on this
blog's github repo.