These are draft notes and are not intended to be a complete reference.

Axiomatic foundations

Foundations of Mathematics should tell us what are true mathematical statements. The last layer of this is the most familiar, the axioms that we know are true in advance. But before we use, or even state, these, we must

• Understand how we can build valid mathematical objects, and what are the ones we start with - the language of mathematics.
• Which of these are statements - is $1 + 2$ true? makes no sense – types of mathematical objects.
• Specify how to make a judgement that one statement is true from knowing other statements are...

This is a list of the main topics, sometimes with corresponding examples, for the type theory we study.

• Recursive definitions: e.g. summing a list.
• First-class functions: e.g. $\sum_{k=1}^{n} f(k)$.
• Fibonacci numbers: indirect recursion
• Currying: Ackermann function (illustrates not only primitve recursize)
  • A(0, n) = n + 1
  • A(m, 0) = A(m -1, 1)
  • A(m, n) = A(m - 1, A(m, n -1))
• Type Families:
  • e.g. tuples
  • e.g. reversing tuples, including searching by type
• Propositions as types:
  • e.g. subtraction
  • propositional combinations
  • quantification
  • basic examples as inductive types
  • Decidable...

The identity inductive type family is one of the most subtle parts of Type Theory, and is core of the link to topology. Here we clarify the definition and some basic properties. Note that there is no additional rule required for this - instead its rich structure depends on the power of induction for indexed types.

The definition

Fix a type $A$. We define $Id_A : A \to A \to \mathcal{U}$ as follows:

Definition: $Id_A : A \to A \to \mathcal{U}$ is the indexed inductive type family freely generated by

• $refl_A : \prod_{a : A} Id_A (a)(a)$

In this note we discuss what we have illustrated that we can do - parsing and interpretation, and show how this leads to results about what is impossible.

The Setup

Functional languges

The languages we use are functional languages, i.e., langauges where functions are first-class objects, so we can have functions of functions and so on, and where definitions can be recursive. Indeed recursion is the only form of looping we have. Idris is certainly a functional langauge, but so is the HackyLang that we have created.

Note: We have extending HackyLang adding expressions for pairs...