Quick Homotopy Type Theory

Posted on March 1, 2020

Tags: typetheory

1 Prelude

First we motivate how type theory is connected with proofs.

2 Curry howard

2.1 Proof are terms inhabiting Types

Let’s say \(N \rightarrow A\) represents implication: “If night falls then it is awesome”
Let’s say \(A \rightarrow B\) represents implication: “If it is awesome then it is beautiful”
We attempt to prove \(N \rightarrow B\) representing implication: “If night falls then it is beautiful”

\[\cfrac{\cfrac{f: A\rightarrow B \qquad \cfrac{p : N \rightarrow A \qquad x : [N]}{p\ x : A}}{f\ ( p\ x ) : B}}{\lambda x . f\ (p\ x) : N \rightarrow B }\]

2.2 Programmer example

Using the same logic as above, we can consider \(List\ A\) as a proposition and \(nil\) is a term that proves \(List\ A\).

\[ \cfrac{}{nil : List\ A} \qquad \cfrac{x : A \qquad xs : List\ A}{cons\ x\ xs : List\ A}\]

Below we give an example of a “proof” of a \(List\ Nat\)

\[\cfrac{4: Nat \qquad \cfrac{5: Nat \qquad nil: List\ Nat}{cons\ 5\ nil : List\ Nat} }{cons\ 4\ (cons\ 5\ nil): List\ Nat} \]

If you can “Prove” it, then you can “Construct” it programmatically (as shown with the cons and nil constructors)
If you cannot “Prove” it, then you cannot “Construct” it programmatically

2.3 Monadic example

Reminder of a monad bind function

\[ bind:\ \{S\ T : Type\} [Monad\ {\color{green}{M}}]\ {\color{green}{M}}\ S \rightarrow (S \rightarrow {\color{green}{M}}\ T) \rightarrow {\color{green}{M}}\ T\]

A parser is

\[ {\color{green}Parser}\ (A: Type) : String \rightarrow List\ ( String \times A)\]

A monadic parser requires it’s own bind function

\[ bind_{parser}:\ \{S\ T : Type\}\ (String \rightarrow List\ (String \times S)) \rightarrow (S \rightarrow (String \rightarrow List\ (String \times T))) \rightarrow (String \rightarrow List\ (String \times T))\]

Let’s see if we can “prove” and “construct” a monadic parser bind, thus proving that the parser is a monad.

3 Syntax

Here is an example, we give a general form and an example with Identity dependent type:

\[ \underset{x: A}{\prod} B(x) \qquad \underset{x: Type}{\prod} Identity(x) \]

inductive Identity (x: Type) := 
  | mkId (x: Type): Identity x

If B is just a constant then it is just a function Type

\[ \underset{x: A}{\prod} B \qquad \underset{x: Type}{\prod} Identity \]

inductive Identity :=
  | mkId (x: Type): Identity
  | mkId : Type -> Identity  --equivalent term constructor, notice function type

4 Type formation

\[ \cfrac{\vdash A: Type \qquad \vdash x,y: A}{\vdash x=_{A}y : Type} \tag{type formation}\]

forming a type like \(\vdash 0 = 1 : Type\) is not asserting that \(0 = 1\) , it is more like it is asking whether \(0 = 1\) which is only true if a term inhabits this type \(0 = 1\)
\(\vdash x = y : Type\) means there are many prove \(x = y\) similarly a function from \(Int -> Bool\) there are many functions that satisfy the typing.
- A single path between \(x\) and \(y\) represents a single proof of equality.
- The path between aka connect 2 paths aka the proof that connects two proof of equality is called a homotopy.

\[ cfrac{\vdash x: A}{\vdash refl_{x} : x=_{A}x} \tag{term intro}\]

\(x,y: A , p : x =_{A} y \vdash B(x,y,p)\) , to produce a term of type B(x,y,p) it suffices to assume y is x and p is refl_{x}