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.

## Quantifiers in Logic

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 Sum

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
: ∀ (a : A) → P a → Σ P Σ_intro
```

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 Product

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
: (∀ (a : A) → P a) → Π P Π_intro
```

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)
```

.

## Tuples - Special Case of Dependent Sum

We will first need to define a `constT`

function:

```
: ∀ (X : Set) (Y : Set) → Y → Set
constT = x constT 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`

.

## Functions - Special Case of Dependent Product

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`

.

## What About Sum Types?

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`

:

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

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:

```
: ∀ (A B R : Set) → Set
prodPredicate = (a → r) → (b → r) → r prodPredicate a b 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 Π
```

## Conclusions

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.