Axes of the lambda cube

Can't see the math behind the greek? For reference, here are the appropriate greek letters for each abstraction mechanism introduced in each axis of the lambda cube. For completeness, lambda abstraction is also included on its own, even though it appears in all axes.

Each cell begins with an example type, followed by an example term of that type. Either the term, the type, or both (...or neither!) will feature a new greek abstraction letter, introducing a variable that can be used on the right of the period.

These new symbols extend the syntax of the calculus, in a way that is made precise in the last lines of the cell. Those lines extend the basic grammar using a functional notation which models variable introductions more precisely than a context-free grammar could.

Even though some cells introduce more than one new abstraction symbol, each cell only introduces one new kind of application. The syntax for application is always just juxtaposition; the syntactic types of the juxtaposed constructs should make it clear which application is meant. The last line of each cell extends the grammar to support this new kind of application, with a bold fragment highlighting what makes the axis unique.

function types
(A → B) →
  A → B
λf:(A → B).
  λx:A. f x

(→) : type → type → type
λ : type → (term → term) → term
(•) : term → term → term

dependent types
(Πx:Nat. P x) →
  Πy:Nat. P y
λf:(Πx:Nat. P x).
  λy:Nat. f y

Π : type → (term → type) → type
(•) : type → term → type

polymorphic types
(∀A. Nat → A) →
  ∀B. Nat → B
λf:(∀A. Nat → A).
  ΛB. λy:Nat. f B y

∀ : (type → type) → type
Λ : (type → term) → term
(•) : term → type → term

parametric types
(A → B → (P : * → * → *) A B) →
  A → B → P A B
λf:(A → B → P A B).
  λx:A. λy:B. f a b

(→) : kind → kind → kind
(•) : ∀⟨type⟩:kind. (type → ⟨type⟩) → type → ⟨type⟩