Let&#x27;s say you&#x27;re creating a new programming language. You think it&#x27;s a good idea to use static types, but which ones? Well, everyone uses booleans, so let&#x27;s include them:<p><pre><code>    True : Boolean
    False : Boolean
</code></pre>
(&quot;foo : bar&quot; means &quot;foo has type bar&quot;, or &quot;foo is a bar&quot;). OK, that seemed pretty easy. But wait, you&#x27;ve not given a type to &quot;Boolean&quot;. For the sake of completeness:<p><pre><code>    Boolean : Type
</code></pre>
Uh oh, now you need to give a type to &quot;Type&quot;. What should it be? It turns out (via Girard&#x27;s paradox) that simply saying &quot;Type : Type&quot; would make things inconsistent, ie. we would be able to trick the compiler into accepting incorrect programs.<p>Instead, we use a series of &quot;levels&quot;:<p><pre><code>    Boolean : Type 0

    Type n : Type (n+1)
</code></pre>
So far so good. Now let&#x27;s say we want function types, for example:<p><pre><code>    identity : Boolean -&gt; Boolean
    identity x = x

    not : Boolean -&gt; Boolean
    not True  = False
    not False = True
</code></pre>
So what&#x27;s this &quot;-&gt;&quot; thing? We can think of it as a type-level operator: it takes two types and returns a function type. In the syntax of natural deduction, we can say:<p><pre><code>    a : Type n         b : Type m
    -----------------------------
     a -&gt; b : Type (1 + max n m)
</code></pre>
ie. given &quot;a&quot; of type &quot;Type n&quot;, and &quot;b&quot; of type &quot;Type m&quot;, then &quot;a -&gt; b&quot; has type &quot;Type (1 + max n m)&quot;. Because the type &quot;a -&gt; b&quot; somehow &#x27;contains&#x27; the types &quot;a&quot; and &quot;b&quot;, we need to ensure it&#x27;s at a higher level than either of them, which is why we do &quot;1 + max n m&quot;.<p>In fact, there&#x27;s no reason for the identity function to <i>only</i> work on Booleans. We can replace it with an &quot;identity function factory&quot;, which accepts a type and returns an identity function for that type:<p><pre><code>    identity : (t : Type n) -&gt; t -&gt; t
    identity x y = y
</code></pre>
Here we&#x27;ve re-used the &quot;foo : bar&quot; notation: rather than just giving the <i>type</i> of the first argument, we&#x27;ve also introduced a variable &quot;t&quot; representing its <i>value</i> (this is known as a <i>dependent function</i>). Notice that the definition of &quot;identity&quot; actually ignores the type it&#x27;s been given (&quot;x&quot;); the <i>implementation</i> doesn&#x27;t care what it is, it&#x27;ll just return the second argument no matter what; yet we need that argument in order to type-check. When we compile this program, we can &quot;erase&quot; the first argument, since it has no &quot;computational content&quot;.<p>We can recover our original identity function, of type &quot;Boolean -&gt; Boolean&quot;, by applying this &quot;identity&quot; function to the &quot;Boolean&quot; type:<p><pre><code>    identity Boolean : Boolean -&gt; Boolean
</code></pre>
OK, what next? Well, since we have functions, we might as well have function composition:<p><pre><code>    compose : (a : Type x) -&gt; (b : Type y) -&gt; (c : Type z) -&gt; (a -&gt; b) -&gt; (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
    compose t1 t2 t3 g f x = f (g x)
</code></pre>
It would also be useful to have equality. Here it is for Booleans:<p><pre><code>    equal : Boolean -&gt; Boolean -&gt; Boolean
    equal True  x = x
    equal False x = not x
</code></pre>
However, just like the identity function, this isn&#x27;t very satisfying. We&#x27;d like an &quot;equality function factory&quot;, with this type:<p><pre><code>    equal : (t : Type n) -&gt; t -&gt; t -&gt; Boolean
</code></pre>
Except, how would we ever implement such a &quot;factory&quot;? It was easy for identity: we just return whatever we&#x27;re given. In the case of equality, we need to <i>inspect</i> our arguments, to see whether they&#x27;re actually equal or not. We can&#x27;t do this in a way which works for all types (eg. what if we allow user-defined types?).<p>However, there&#x27;s a trick. By returning a Boolean, we&#x27;re defining equality (True) <i>and</i> disequality (False). That&#x27;s hard. Instead, we can ignore the disequality, and only focus on equality, using a different return type; let&#x27;s call it &quot;Equal x y&quot;.<p>What does it mean for two things to be equal? It means that they&#x27;re the same thing. In which case, we don&#x27;t need both of them! Every value is equal to itself (a property known as &quot;reflexivity&quot;), so that&#x27;s all we need!<p><pre><code>    refl : (t : Type n) -&gt; (x : t) -&gt; Equal x x
</code></pre>
For example, here&#x27;s equality for the Booleans:<p><pre><code>    refl Boolean True : Equal True True

    refl Boolean False : Equal False False
</code></pre>
Note that &quot;refl&quot; isn&#x27;t actually a function, it&#x27;s a data constructor. You can think of a value like &quot;refl Boolean True&quot; as being a piece of data, similar to something like &quot;pair Int String 10 &#x27;foo&#x27;&quot;; it doesn&#x27;t reduce to anything, it just gets passed around as-is. (These are often called &quot;proof objects&quot;, but that&#x27;s a bit arbitrary; a value like &quot;pair Int String 10 &#x27;foo&#x27;&quot; is a &quot;proof&quot; of &quot;Int AND String&quot;).<p>If we allow computation in our types, then two <i>different</i> values which compute (technically: beta reduce) to the same thing are still equal by reflexivity:<p><pre><code>    refl Boolean True : Equal True (not False)
</code></pre>
Here, the &quot;not False&quot; will compute to &quot;True&quot;, and reflexivity will work. Different values, eg. &quot;False&quot; and &quot;True&quot;, are never equal, since they don&#x27;t reduce to the same thing. We can make our computations as complex as we like, for example:<p><pre><code>    refl Boolean True : Equal (identity Boolean True) (compose Boolean Boolean not not True)
</code></pre>
We can even have equality between functions and equality between types:<p><pre><code>    -- &quot;identity&quot; is equal to &quot;identity&quot;
    refl ((t : Type n) -&gt; t -&gt; t) identity : Equal identity identity

    -- &quot;Boolean&quot; is equal to &quot;Boolean&quot;
    refl (Type 0) Boolean : Equal Boolean Boolean
</code></pre>
We can even have equalities between equalities!<p><pre><code>    -- &quot;refl Boolean True&quot; is equal to &quot;refl Boolean True&quot;
    refl (Equal True True) (refl Boolean True) (refl Boolean True) : Equal (refl Boolean True) (refl Boolean True)
</code></pre>
Most of this predates Homotopy Type Theory, so what are the points being made in the slides?<p>One point is to give a topological perspective for types: a type is like a space, values in the type are like points in the space. Equalities between values are paths in the space (eg. &quot;refl Boolean True&quot; is a trivial path from the point &quot;True&quot; to itself, in the &quot;Boolean&quot; space). Interestingly, equalities between equalities are homotopies (smooth transformations between paths).<p>One question we might ask is whether all equality values are the same; ie. are they all just &quot;refl&quot;? That&#x27;s known as the &quot;Uniqueness of Identity Proofs&quot; (UIP), and it&#x27;s an assumption that many people have been making for decades. However, if we think of equalities as paths through a space, then UIP says that all those paths can be transformed into each other. Yet that&#x27;s <i>not</i> the case if the space contains a hole! Consider two paths going from a point X back to itself; if one of those paths loops around a hole, and the other doesn&#x27;t, then there&#x27;s no way to smoothly transform between the two (without &quot;cutting and sticking&quot;).<p>The topological perspective also gives us some intuition about the &quot;levels&quot; of types: &quot;Type 0&quot; contains spaces with distinct points, eg. &quot;Boolean&quot; containing &quot;True&quot; and &quot;False&quot;. These are essentially sets, from Set Theory. Although HoTT doesn&#x27;t assume UIP for all types, those which do just-so-happen to &quot;collapse&quot; down to one value (ie. there are equalities between every point) actually occupy a level <i>below</i> sets; ie. they end up at &quot;Type -1&quot; (there&#x27;s no significance to the negative number; it&#x27;s just a historical accident caused by definitions like &quot;Boolean : Type 0&quot;). Likewise, those which add more structure occupy higher levels.<p>One important question is how function equality behaves. It&#x27;s useful to have equality for, say, Booleans, since we can compute their value and check whether they&#x27;re the same. Functions are trickier: we have <i>intensional</i> equality (eg. Equal identity identity) but we&#x27;d like <i>extensional</i> equality (eg. that &quot;identity&quot; and &quot;not . not&quot; are equal, ie. Equal (identity Boolean) (compose Boolean Boolean Boolean not not)). This is tricky. If we assume extensionality as an axiom (((x : t) -&gt; Eq (f x) (g x)) -&gt; Eq f g), like in NuPRL, then we lose the ability to execute our programs (axioms are basically &quot;built in primitives&quot;; we don&#x27;t know how to implement such an extensionality primitive). Observational Type Theory gets us most of the way there, but relies on UIP, which would collapse all of the higher-level structure in HoTT.<p>Univalence is also a nice feature of HoTT. It&#x27;s incompatible with UIP, but allows us to reason &quot;up to isomorphism&quot;. For example, in set theory the sets {foo, bar} and {x, y} are isomorphic: eg. we can switch foo with x and bar with y. However, results concerning {foo, bar} may be invalid for {x, y}, since set theory lets us say things like &quot;is foo a member of S?&quot;, which is true when S = {foo, bar} but false when S = {x, y}. HoTT doesn&#x27;t let us say things like &quot;is foo a member of type T?&quot;, hence we don&#x27;t get these kind of &quot;abstraction leaks&quot;, so our programs and proofs can be automatically lifted from one representation to another. For example, if you define a fast, distributed datastructure which is isomorphic to a linked-list, then you can automatically lift every linked-list program to your new datastructure using univalence. Unfortunately, we haven&#x27;t figured out how to implement univalence yet (but many people think it&#x27;s possible).<p>Some of the results listed at the end of the slides concern the use of HoTT to prove topological results, eg. that the integers are isomorphic to paths around a hole (you can go around the hole any number of times, clockwise or anticlockwise).<p>Girard&#x27;s paradox: <a href="http:&#x2F;&#x2F;mathoverflow.net&#x2F;questions&#x2F;18089&#x2F;what-is-the-manner-of-inconsistency-of-girards-paradox-in-martin-lof-type-theor" rel="nofollow">http:&#x2F;&#x2F;mathoverflow.net&#x2F;questions&#x2F;18089&#x2F;what-is-the-manner-o...</a>
Natural deduction: <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Natural_deduction" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Natural_deduction</a>