A note on syntax

The reason for the name “Pi types” (and the symbol Π ) is the following :

In math, it is common to use the notation $B^A$ to indicate the set of all functions from $A$ to $B$.

For simplicity let’s assume that $A$ is finite (and has cardinality $|A| = n$)

Then we can define:

$$B^A := \Pi_{a: A}\ B = \underbrace{B \times B \times \cdots \times B}_{|A|\ \mathrm{ times}}$$

and each element $f \in \Pi_{a: A}\ B$ has the form $(f_{a_1}, f_{a_2}, \dots, f_{a_n})$.

In other words, for each $a_i \in A$ we can find an element $f_{a_i}\in B$ at the position $i$.

Given such a tuple we can create a function $f: A \to B$ by the rule

$$f(a_i) := f_{a_i}$$

conversely, given a function $f: A \to B$ we can create the tuple $(f(a_1), f(a_2), \dots) \in \Pi_{a: A}\ B$

In a dependent function we let $B$ depend on $a \in A$ like so:

This is the motivation for the syntax:

Π (a: A), B a

When B does not depend on a: A this becomes

Π (_: A), B

and we can use the syntactic sugar

A -> B