Homotopy Type Theory notes

Let \(f: A\fun B\) and \(\Phi : B\) (the "function body"), then \[f(x) :\equiv \Phi \equiv f :\equiv\lambda x.\Phi \]

The uniqueness principle is analogue to the not dependent function type, with the difference that \(\Phi : B(x)\) possibly involves the variable \(x: A\).

A polymorphic function is one that takes a type as one of its arguments and then acts on elements of that type. Examples are:

1. The identity function :: \(id \Pi_{(A: \U)} A \fun A\) such that \(id(A,x) :\equiv x\). It's also written as \(id_A(x)\).
2. The \(swap\) function :: \(swap : \Pi_{(A:\U)}\Pi_{(B:\U)}\Pi_{(C:\U)} \left( A \fun B \fun C\right) \fun \left( B \fun A \fun C\right)\) such that \(swap(A,B,C,g) :\equiv \lambda a.\lambda b.g(b)(a)\), also written as \(swap_{A,B,C}(g)(a,b) :\equiv g(b,a)\).

If a multiparameter dependent function consists of independent elements of the same type, one may also write them in a condensed form. In the example of the \(swap\) function, one may write \(\Pi_{(A,B,C:\U)}\) since \(A,B,C\) do not depend on eachother.

Given \((a,b): A\times B\) and \(g: A \fun B \fun C\) one can always define a function \(f : A \fun B \fun C\) such that \[f((a,b)) :\equiv g(a)(b)\]

You can define a function called recursor for product types \[rec_{A\times B}:\left(A \fun B \fun C \right) \fun A \times B \fun C\] such function can be used to define the two projections \[pr_1 :\equiv rec_{A\times B}(A, \lambda a.\lambda b. a)\] \[pr_2 :\equiv rec_{A\times B}(B, \lambda a.\lambda b. b)\] On the contrary, one could define the recursor from the two projections

In order to introduce a new type, one needs to provide the following:

Formation rules

How to form the new types;

Construction rules

How to form elements of the new type; these are called constructors or intrduction rules;

Elimination rules (or eliminators)

How to use elements of that type;

Computation rule

How an eliminator acts on a constructor;

(Optional) Uniqueness principle

It may be proved from the rules above, thus it's optional. Expresses uniqueness of maps from or to that type:

Maps "going into" the type

Every element of the type is uniquely determined by the results when applying eliminators to it; moreover every element can be reconstructed from the results by applying a constructor. Essentially, there's a constructor-eliminator duality.

Maps "going out from" the type

Every function (map) from that type is uniquely determined by some data.

Uniqueness principle (if not defined)

how can I find which elements of a type are definitionally equal to eachother?

Recursor (or non-dependent eliminator)

a function that satisfies the recursion principle; special case of the induction principle

Induction (dependent eliminator)

a function that satisfies the induction principle, an "iteration of the elements of the type"