4 ms·

First the type theory part of homotopy type theory. Mathematicians have been doing logic for a long time, but mathematical statements and proofs were not themse

by jules 11y ago

First the type theory part of homotopy type theory. Mathematicians have been doing logic for a long time, but mathematical statements and proofs were not themselves mathematical objects. They were just human language text with some math notation thrown in. Around 1900 Brouwer, Heyting and Komolgorov came up with a cool idea: treat proofs as first class mathematical objects. Then giving a proof is equivalent to constructing a mathematical object. * A proof of `P and Q` is a pair of proofs (a,b) where a is a proof of P and b is a proof of Q * A proof of `P implies Q` is a function that takes a proof of P and returns a proof of Q * A proof of `P or Q` is a pair (x,c) where either x=0 and c is a proof of P or x=1 and c is a proof of Q In modern terms; to give a proof of `P and Q` is to give a value of the pair type `(P, Q)`. To give a proof of `P or Q` is to give a value of the disjoint sum type `P + Q`. To give a proof of `P implies Q` is to give a value of the function type `P -> Q`. Take the theorem `(A and B) implies (B and A)`. A proof of this is, in Haskell notation: proof :: (A,B) -> (B,A) proof (a,b) = (b,a) So a proof of `(A and B) implies (B and A)` is a function that swaps the order of a pair. An interesting property of this way of doing things is that statements are not merely true or false, but statements can in general be true in more than one way. For example the statement `(A and A) implies A` has two different proofs: proof1 :: (A,A) -> A proof1 (a1,a2) = a1 proof2 :: (A,A) -> A proof2 (a1,a2) = a2 The proof1 of `(A and A) implies A` is a function that returns the first component of a pair, and proof2 a function that returns the second component. I'll skip over dependent types. That's the type theory part. Now the homotopy part. For a long time there was a problem with type theory. There was no really good way to do equality in it. To do math you want to use equality all the time. Since we've defined what the proofs of `P and Q`, `P or Q`, `P implies Q` are, what are the proofs of `x = y`? There has existed some notion of equality in type theory for a long time, but it wasn't satisfactory for various reasons. You couldn't prove two functions equal even though they gave the same outputs for the same inputs. Homotopy type theory fixes equality in type theory. The idea is that a proof of `x = y` depends on the type of x and y. * Two pairs c,d are equal if their first components are equal and their second components are equal. * Two functions f,g are equal if for all x, f x is equal to g x. * etc. More precisely, the proofs of equality on the type (A,B) is a pair of a proof of equality on A and a proof of equality on B. Just like previously a statement can be true in more than one way (have more than one proof), things can now also be equal in more than one way (have more than one proof of equality). Another extension that homotopy theory theory does is with user defined types. When you define a type you are allowed to define its type of equality proofs at the same time. This allows you to define things like integers modulo k ((i mod k) is equal to (i+k mod k)), unordered sets (a set S is equal to any permutation of S), and more. I've brushed over a lot of details and presented only a very narrow way of looking at type theory: 1. A type itself is a value. 2. Full dependent types. 3. When are two types equal? 4. When are two proofs of equality equal? 5. What exactly is a function, what is a pair, etc.? This leads us into category theory, which gives an abstract description of functions and pairs. Hopefully this still made some amount of sense. Two line summary: 1. Type theory: using conventional mathematical objects like pairs and functions as proof objects. 2. Homotopy type theory: extends type theory with proofs of equality in a proper way.

YorkshireSeason 11y ago
It is wrong to say that it's key novelty is that "Homotopy type theory: extends type theory with proofs of equality in a proper way". This was done already with Martin Lof's type theory, as used in e.g. Agda. Homotopy type theory adds univalence!
- jules 11y ago
  I wouldn't call that a proper treatment of equality. It is unsatisfactory in several ways: no proper equality on functions (function extensionality), no proper equality on types (univalence), no quotient types (~= HITs), and since refl is the only proof of equality it doesn't even make much sense to talk about equality on equalities. More fundamentally the idea that refl is the only proof of equality just doesn't sit well in the philosophy of type theory. The whole idea of type theory is that things can have more than one proof and are not 'just true' as in conventional mathematics.
  - YorkshireSeason 11y ago
    This discussion goes way beyond an "absolute layman explanation to homotopy type theory" ... Anyway, I disagree that the "whole idea of type theory is that things can have more than one proof". UIP is about identity types and their proofs. Identity types are very special types. It is far from obvious that they should be inhabited by more than one proof. Indeed, it was a surprising breakthrough when Streicher/Hoffmann discovered that UIP does not hold in general and new axioms like Streicher's K or Univalence needed to be formulated to deal with this question.
    - jules 11y ago
      It's true that it was a discovery that Martin Lof identity types could have multiple inhabitants, but it's a general principle of type theory that types can have multiple inhabitants (unlike in set theory, where propositions are just true). That this also applies to identity types in HoTT is a sign that something is going right. Furthermore, from another perspective it's "obvious" that identity types should have multiple inhabitants. There were two approaches to equality in type theory. One is Martin Lof identity types, which follow naturally from Leibniz' principle that A and B are equal then they are indistinguishable. The other is defining equality for each type on a case by case basis (pairs are equal if their components are equal, functions are equal if they give equal outputs, etc.), like in section 2.4 Equality of this paper: http://www.andres-loeh.de/PiSigma/PiSigma.pdf http://www.andres-loeh.de/PiSigma/PiSigma.pdf In the latter approach it's obvious that equality has multiple inhabitants, because it's defined that way. For example we can define equality of unordered pairs as the type: id_unordered_pair : (A,A) -> (A,A) -> Type id_unordered_pair (a,b) (c,d) = (id_A a c)*(id_A b d) + (id_A a d)*(id_A b c) i.e. two unordered pairs (a,b) and (c,d) are equal if a=c and b=d or a=d and b=c. This has two inhabitants even if id_A has only a single inhabitant. This approach naturally accommodates quotient types. The problem with it is that the type system has no idea that this is equality. It's just another definition. The point of equality is that all functions respect equality (equal inputs to equal outputs). Not all functions respect equality on these unordered pairs (e.g. a function that extracts the first component). This approach to equality has the converse of Leibniz' rule: we can define equality so that if two things are indistinguishable then they are equal. I think a good view of HoTT is as unifying these two approaches to equality. We get both Leibniz' principle and its converse, and we get user defined equality types whose equality is respected by all functions, we get multiple inhabitants for equality types.

by jules 11y ago

YorkshireSeason 11y ago

It is wrong to say that it's key novelty is that "Homotopy type theory: extends type theory with proofs of equality in a proper way". This was done already with Martin Lof's type theory, as used in e.g. Agda. Homotopy type theory adds univalence!

jules 11y ago
I wouldn't call that a proper treatment of equality. It is unsatisfactory in several ways: no proper equality on functions (function extensionality), no proper equality on types (univalence), no quotient types (~= HITs), and since refl is the only proof of equality it doesn't even make much sense to talk about equality on equalities. More fundamentally the idea that refl is the only proof of equality just doesn't sit well in the philosophy of type theory. The whole idea of type theory is that things can have more than one proof and are not 'just true' as in conventional mathematics.
- YorkshireSeason 11y ago
  This discussion goes way beyond an "absolute layman explanation to homotopy type theory" ... Anyway, I disagree that the "whole idea of type theory is that things can have more than one proof". UIP is about identity types and their proofs. Identity types are very special types. It is far from obvious that they should be inhabited by more than one proof. Indeed, it was a surprising breakthrough when Streicher/Hoffmann discovered that UIP does not hold in general and new axioms like Streicher's K or Univalence needed to be formulated to deal with this question.
  - jules 11y ago
    It's true that it was a discovery that Martin Lof identity types could have multiple inhabitants, but it's a general principle of type theory that types can have multiple inhabitants (unlike in set theory, where propositions are just true). That this also applies to identity types in HoTT is a sign that something is going right. Furthermore, from another perspective it's "obvious" that identity types should have multiple inhabitants. There were two approaches to equality in type theory. One is Martin Lof identity types, which follow naturally from Leibniz' principle that A and B are equal then they are indistinguishable. The other is defining equality for each type on a case by case basis (pairs are equal if their components are equal, functions are equal if they give equal outputs, etc.), like in section 2.4 Equality of this paper: http://www.andres-loeh.de/PiSigma/PiSigma.pdf http://www.andres-loeh.de/PiSigma/PiSigma.pdf In the latter approach it's obvious that equality has multiple inhabitants, because it's defined that way. For example we can define equality of unordered pairs as the type: id_unordered_pair : (A,A) -> (A,A) -> Type id_unordered_pair (a,b) (c,d) = (id_A a c)*(id_A b d) + (id_A a d)*(id_A b c) i.e. two unordered pairs (a,b) and (c,d) are equal if a=c and b=d or a=d and b=c. This has two inhabitants even if id_A has only a single inhabitant. This approach naturally accommodates quotient types. The problem with it is that the type system has no idea that this is equality. It's just another definition. The point of equality is that all functions respect equality (equal inputs to equal outputs). Not all functions respect equality on these unordered pairs (e.g. a function that extracts the first component). This approach to equality has the converse of Leibniz' rule: we can define equality so that if two things are indistinguishable then they are equal. I think a good view of HoTT is as unifying these two approaches to equality. We get both Leibniz' principle and its converse, and we get user defined equality types whose equality is respected by all functions, we get multiple inhabitants for equality types.