8 ms·

Can someone give me an absolute layman explanation to homotopy type theory (and why it's so interesting)? I'm hearing about it everywhere, but most of the intr

Can someone give me an absolute layman explanation to homotopy type theory (and why it's so interesting)? I'm hearing about it everywhere, but most of the introductions to the subject assume the reader is already familiar with either type theory or category theory.

j2kun 11y ago
I'll try to keep it short and skip the details of the mathematical framework itself. Back in the early 1900's there was a school of mathematical logic that denied a certain axiom called the law of the excluded middle, that !!p <=> p. They said that if you used this axiom (roughly) your proof was not "constructive," whereas if you avoided it your proof was "constructive." They went as far as to deny all math that was not constructive (which I think is silly). Their ideas faded out of popularity among mainstream mathematicians, but their goal was to rewrite the foundations of all mathematics using only constructive proofs, and to their credit they got pretty damn far in certain subjects like real analysis (calculus). Today, their ideas are seeing a resurgence in the homotopy type theorists (HTTs). Their goal is also to rewrite all of mathematics in a constructive way, but now they have the hindsight of these great tools like category theory and homology and computers and all these great things developed in the mid to late 20th century. So they are working on building this framework and seeing what it can prove. The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive) and one of their main selling points is that their work will eventually lead to "computer assisted mathematics," not in the sense of Stephen Wolfram but rather in the sense that a computer will check your proofs as you prove them and find stupid mistakes. I personally am not all that excited about HTT, due to what I see as misguided hype around it. My preferred way to view it is as logicians studying a really fascinating new logical system and seeing how far they can push it. Saying things like "I deny all mathematics that's not constructive" and "computers will start doing our proofs for us," makes me cringe. But it is what it is :)
- mafribe 11y ago
  j2kun's characterisation of HoTT is misleading. Their goal is also to rewrite all of mathematics in a constructive way, This is not the goal of HoTT, and also not possible as some mathematics is intrinsically non-constructive. HoTT allows non-constructive reasoning, see section 3.4 "Classical vs. intuitionistic logic" of the HoTT book http://homotopytypetheory.org/book/ http://homotopytypetheory.org/book/. You can say that HoTT derives non-constructive mathematics on top of constructive foundations. The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive) No. Whether a proof can be logically checked by a computer has nothing to do with whether it is constructive or not. A proof is just a syntactic object. It's just as easy to check if a proof step uses excluded middle or double negation as it is to check whether it uses a construtive principle like /\-introduction. There are many proof assitants that work with classical logic, e.g. Mizar, HOL, HOL light, Isabelle/HOL ... All of SAT-solving works classically. The novelty of HoTT, and only extension over intensional Martin-Loef type-theory, is the univalence axiom.
  - kazinator 11y ago
    A proof in mathematics is not purely syntactic because it's not purely logical. For instance, in some steps of a proof, we do something to both sides of an equation and argue that it is still balanced, based on rules that are outside of logic. Such a step can have a nonconstructive element.
    - mafribe 11y ago
      A proof in mathematics is not purely syntactic because it's not purely logical. This is confusing constructive reasoning with the decision problem for proof validity. They are different things. The very point of logic, constructive or otherwise, or at least one of the key points for having a logic is to be able to decide whether a given proof object is indeed a valid proof. Valid proofs of course typically also make use of non-logical axioms of the ambient theory. If proof-hood is not decidable, it's not a logic. Reasoning is constructive if it avoids certain proof principle like LEM (law of excluded middle) or double negation.
- baddox 11y ago
  If you limit yourself to only constructive proofs, do you even get the real numbers? I'm not very clear on the definition of "constructive," but given that almost all real numbers are non-computable (i.e. most likely, the set of all real numbers you have ever encountered outside of computability theory has the same cardinality as the integers), it doesn't feel very constructive to me. I've always found it odd that we learn early on in discrete mathematics about how the cardinality of the reals is larger than that of the integers and rationals, and yet it seems like you'll never deal with anything from this larger set of reals unless you're studying computability.
  - mafribe 11y ago
    Rest assured that (contrary to j2kun's misleading claims) if some of the world's top mathematicians and computer scientists propose a new foundation of mathematics, they don't forget real numbers. You need to distinguish between non-computable and non-constructive. The proof that the cardinality of the reals is non-countable is perfectly constructive, see [1] for a discussion of these and related issues. [1] https://en.wikipedia.org/wiki/Cantor%27s_first_uncountability_proof#Constructive_or_non-constructive_nature_of_Cantor.27s_proof_of_the_existence_of_transcendentals https://en.wikipedia.org/wiki/Cantor%27s_first_uncountabilit...
    - igravious 11y ago
      Eh? Your very own link says that there is debate within the mathematical community about whether Cantor's uncountability proof is constructive or not. I just realised that in my mind uncountable (not in a one-to-one correspondence with the natural numbers) means non-constructive. For me countability just says that we have a (constructive) method for generating a sequence of what would be all the terms in the sequence (if it were ever to terminate which it doesn't) and no term outside the sequence in a non-repeating fashion that is unbounded. Clearly if some sequence is uncountable it means that one of these criteria fails to hold. Which one? Not the non-repeating stipulation. Not the no term outside the sequence stipulation. It must be the stipulation that every term will be encountered during the generation. So there isn't a (constructive) method for generating uncountable sequences. The reals are uncountable, ergo there is no constructive method for generating the reals. Where am I going wrong? NB: I am not saying that you can't have a method for constructing individual reals like e and pi and so on.
- IngoBlechschmid 11y ago
  Your comment is a good first approximation to the motivation for HoTT! However, let me add a couple of remarks. Firstly, HoTT can also be used with classical logic, i.e. where you freely use the law of excluded middle. This does not impact the ability to check proofs with the computer in any way. Secondly, HoTT is the first foundation with which computer-formalized proofs of nontrivial theorems in a subject called "homotopy theory" are possible. In theory, this is possible with any foundational theory; but in practice, the necessary encodings to, for instance, Zermelo--Fraenkel set theory, are too involved for computer formalization. In HoTT, one can define (and reason about) the basic concepts of homotopy theory straight from "day one". In contrast, with a more traditional foundation, one needs to setup a host of intermediate concepts first (like the real numbers, topological spaces, homotopies, ...). This is no problem for a trained mathematician, but becomes a nuisance when working with proof assistants. Thirdly, one intriguing aspect of HoTT is that it might be possible to "run" proofs (this is the objective of current research). For example, if you prove that some group contains finitely many elements, the vision is that you could run this proof to find out how many elements it contains. This "computational interpretation" is not unique to HoTT; in fact, this is what the linked nLab article is about. But because of the second point, many more theorems are amenable to such an approach. A last remark, not pertaining to HoTT but constructive mathematics. A simple reason why one might be interested in restricting oneself to constructive arguments is that thereby they are applicable to more general situations. There is a metatheorem to the effect that "a statement with a constructive proof holds in any topos", where "topos" is a precise formulation of "alternative mathematical universe". Such universes are routinely used in several subjects of mathematics, for instance algebraic geometry (after Grothendieck's revolution). There are also other reasons for why it's fun to argue constructively. See for instance these slides: https://github.com/iblech/talk-constructive-mathematics/raw/master/negneg-translation-notes.pdf https://github.com/iblech/talk-constructive-mathematics/raw/... (PDF pages 8ff.)
  - mafribe 11y ago
    Very nice descriptions. While constructive reasoning is has many advantages, it has one disadvantage that is rarely pointed out, but sometimes causes real trouble. Let's say we have a formula A which is classically and constructively true. It may be the case that constructive proofs of A are longer and more complicated than classical proofs of A. If you are working with an interactive proof assistant, this may be the difference between the proof automation being able to deal with A automatically or not. This explosion in proof size is the reason why the (perfectly constructive) nominal techniques of Pitts et al have been implemented to a high standard in Isabelle/HOL are are used frequently, but are not really in Coq.
- deleted 11y ago
  [deleted]
- deleted 11y ago
  [deleted]
- igravious 11y ago
  Careful! Here is LEM: ⊢. ~p ∨ p (one of either p or p's inverse must be true -- and thus the other false -- with no third (truth) value allowed), hence also called principle of bivalence. What you wrote is the principle of double negation. In general: (~p ∨ p) ⇒ (¬¬p ⇔ p) but not the other way around if I not mistaken? Please correct me if I am wrong.
  - igravious 11y ago
    In other words, what you wrote is that every value when negated twice returns to itself. Here's a truth table of 3 values for the negation operator v | 0 | 1 | 2 -------------- ¬v | 1 | 0 | 2 So ¬¬0 ⇔ 0 and ¬¬1 ⇔ 1 and ¬¬2 ⇔ 2 which satisfies the principle of double negation but not LEM. Correct?
    - IngoBlechschmid 11y ago
      Your counterexample could work, but it is not obvious that it does so. This is because you also have to give definitions of ∧, v, and ==>, and then check that your definitions satisfy the axioms of intuitionistic logic. As stated, your example only shows that one can define a function f on a set which contains more than two elements such that f . f = id. But this by itself is a trivial statement.
      - igravious 11y ago
        Once those definitions are given then my trivial example holds though, correct? Which are you saying; that it is, or, it is not possible to give those definitions?
        IngoBlechschmid 11y ago
        I didn't check it. If you want to do it (the key step being to verify that the axioms of intuitionistic logic holds for your definitions of AND and OR), you can check Wikipedia for the list of axioms to verify: https://en.wikipedia.org/wiki/Heyting_algebra https://en.wikipedia.org/wiki/Heyting_algebra
mafribe 11y ago
Typing systems (at least some of them) are also logics. This is called the Curry-Howard correspondence (CHC). At first the CHC was made to work for propositional logic only, i.e. logic without for-all and existential quantification. Later typing systems were developed which correspond to logic with quantification. This requires dependent types. However, early typing systems with dependent types had an inelegant handling of equality. Logic needs equality to express things like forall x. x = 3 => x > 2. To overcome this problem, Per Martin-Loef introduced a dependent type-theory (MLTT) with "identity-types" which enables an elegant handling of equality. MLTT and all other extant formalisations of mathematics still suffered from another problem, in that many mathematical constructs are 'morally' the same, but formally distinct. For example you can define a group to be a triple ( G, 1, * ) where G is a set, 1 the neutral element and * the binary operation, or you can define it as ( G, *, 1 ). The former and the latter are not the same thing, but we don't really want to say that they formalise different concepts. This is similar to how in many programming languages certain types are formally distinct but somehow capture the same content. Homotopy type theory (HoTT) overcomes this problem (or parts of this problem) by adding a single axiom to MLTT, called the "univalence axiom" which can informally be rendered as: Things that are 'morally' the same, really are identical. The key idea behind the univalence axiom is that MLTT (and hence HoTT) restricts the mathematical objects that can be constructed such that whenever you have objects O1 and O2 that are morally the same, then there is a function that transforms any construction involving O1 automatically into a construction involving O2 or vice versa, but in a truth preserving way. It turns out that proofs in HoTT are formally similar to certain aspects of geometry/topology. Much of current research on HoTT is about the consequences of the univalence axiom and the similarity between logic and geometry/topology. The key hope in all this is that HoTT will streamline formalised mathematics.
- igravious 11y ago
  Wonderfully accessible synopsis. One ever so _minor_ point. Did you really mean to say "The former and the latter are not the same thing" or "The former and the latter are not _formally_ the same thing" ??? Here's a fun fact for you, you might enjoy this. I picked up a copy of a 1943, second edition, hardback copy of Bertrand Russell's An Inquiry into Meaning and Truth. (In an antiquarian bookstore for €25, as one does... the colophon even states BOOK PRODUCTION WAR ECONOMY STANDARD) Anyway, chapter XX is titled "The Law of The Excluded Middle" and in it Russell states, "[…] As everyone knows, Brouwer has challenged the law, and has done so on epistemological grounds. He, in common with many others, holds that “truth” can only be defined in terms of “verifiability”, which is obviously a concept belonging to the theory of knowledge. If he is right, it follows that the law of the excluded middle, and the law of contradiction also, belong to epistemology, and must be reconsidered in the light of whatever definition of truth and falsehood epistemology permits." What strikes me about this (apart from the fact that I did not know previously that Russell tackled the question of constructivism/intuitionism so directly) is that he claims that everyone! knows this. If we are being charitable by everyone he means mathematicians, and perhaps logicians, maybe even philosophers, I still think it's quite a broad statement. It shows that the school of the logical positivists springs from Brouwer -- which firstly I was never taught, and which secondly does not appear in, for instance, Language, Truth, and Logic[1] by A.J. Ayer. Finally I can see how the law of double negation becomes an epistemological matter, but not the law of what he calls here contradiction (noncontradiction?). He goes on to disprove the verifiability claim over many pages, and thus constructivism. There's a swipe at Wittgenstein further on still. It's a fascinating text. Russell grapples with mathematical and logical issues in a clear fashion using everyday language. Kind of like what you might get if you took the intro to HoTT and lengthened it and made it more philosophical. [1] https://archive.org/stream/AlfredAyer/LanguageTruthAndLogic_djvu.txt https://archive.org/stream/AlfredAyer/LanguageTruthAndLogic_... ps: is there markup for blockquote on HN? EDIT: clarity, markup, prose style
Kutta 11y ago
Another addendum to the discussion, from an angle more relevant to computer programmers: if we find a computational meaning for the univalence axiom, then it'll be a crazy nuclear weapon of generic programming and code generation. The univalence axiom says that two types are equal if we can convert their values back and forth (without loss of information). For example, one Boolean type may be defined as an enum containing True and False. But we could rename the values to Foo and Bar and it would be still a fine implementation, because it's easy to convert between the two representations. We can imagine more far-fetched representations too, with more complicated conversion functions. But in type theory, if two types are equal, then we can freely substitute one for another in any context! For example, if we have a function "Bool -> Bool", and we know that Bool is equal to Bool2, then we can coerce the function to type "Bool2 -> Bool2". Imagine a complex program that uses a complex piece of data type. If we can provide a correct conversion function to another type (i. e. prove that the type is equivalent to another one), then the univalence axiom can take the conversion function and our program as input, and spits out a new program that uses the new data type, and also preserves all properties of the program. By our current standards of generic programming, this is just insane! Now, the issue is that currently we don't actually have a computational interpretation for the univalence axiom, so the above magic doesn't yet work. But there is meaningful progress towards that, and there are already some experimental implementations that can do some magic, for example this one: https://github.com/mortberg/cubicaltt https://github.com/mortberg/cubicaltt
- YorkshireSeason 11y ago
  What is the state of the art of the research on the computational interpretation of univalence? What's working, what's not working? I seem to remember that A Jeffrey said not too long ago that he had a working interpretation.
  - gallabytes 11y ago
    A lot of work was going into the cubical model, but IIRC they realized it was a dead end about a month and a half ago. Right now the most promising work looks to be formalizing the set theoretic model in NuPRL.
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.
kylebrown 11y ago
In the comments of a recent mathematics-without-apologies blog post[1], there was a back-and-forth between Jacob Lurie and Urs Schreiber (the author of the OP article on nLab). I've been trying to parse the material on nLab for years, good to know I'm not the only one who seems to have trouble with it. A refreshingly blunt discussion, not to be missed! 1. https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-224 https://mathematicswithoutapologies.wordpress.com/2015/05/13...
solomatov 11y ago
Homotopy type theory formalizes informal reasoning style when things which have "the same structure" are considered equal in a constructive type theory setting. Another achievement is formulation of synthetic homotopy type theory, i.e. axiomatic as opposed to based on geometric type theory.
- mafribe 11y ago
  I don't think synthetic homotopy type theory is known to cover all of conventional homotopy theory, so it's work in progress.
ericbb 11y ago
Check out this Scientific American article[1], especially the video of a presentation given by Voevodsky. Edit: Here's a more direct page[2] if you just want the video. [1] http://blogs.scientificamerican.com/guest-blog/voevodskye28099s-mathematical-revolution/ http://blogs.scientificamerican.com/guest-blog/voevodskye280... [2] http://www.heidelberg-laureate-forum.org/blog/video/lecture-thursday-september-26-vladimir-voevodsky/ http://www.heidelberg-laureate-forum.org/blog/video/lecture-...

j2kun 11y ago

I'll try to keep it short and skip the details of the mathematical framework itself. Back in the early 1900's there was a school of mathematical logic that denied a certain axiom called the law of the excluded middle, that !!p <=> p. They said that if you used this axiom (roughly) your proof was not "constructive," whereas if you avoided it your proof was "constructive." They went as far as to deny all math that was not constructive (which I think is silly). Their ideas faded out of popularity among mainstream mathematicians, but their goal was to rewrite the foundations of all mathematics using only constructive proofs, and to their credit they got pretty damn far in certain subjects like real analysis (calculus). Today, their ideas are seeing a resurgence in the homotopy type theorists (HTTs). Their goal is also to rewrite all of mathematics in a constructive way, but now they have the hindsight of these great tools like category theory and homology and computers and all these great things developed in the mid to late 20th century. So they are working on building this framework and seeing what it can prove. The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive) and one of their main selling points is that their work will eventually lead to "computer assisted mathematics," not in the sense of Stephen Wolfram but rather in the sense that a computer will check your proofs as you prove them and find stupid mistakes. I personally am not all that excited about HTT, due to what I see as misguided hype around it. My preferred way to view it is as logicians studying a really fascinating new logical system and seeing how far they can push it. Saying things like "I deny all mathematics that's not constructive" and "computers will start doing our proofs for us," makes me cringe. But it is what it is :)

mafribe 11y ago
j2kun's characterisation of HoTT is misleading. Their goal is also to rewrite all of mathematics in a constructive way, This is not the goal of HoTT, and also not possible as some mathematics is intrinsically non-constructive. HoTT allows non-constructive reasoning, see section 3.4 "Classical vs. intuitionistic logic" of the HoTT book http://homotopytypetheory.org/book/ http://homotopytypetheory.org/book/. You can say that HoTT derives non-constructive mathematics on top of constructive foundations. The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive) No. Whether a proof can be logically checked by a computer has nothing to do with whether it is constructive or not. A proof is just a syntactic object. It's just as easy to check if a proof step uses excluded middle or double negation as it is to check whether it uses a construtive principle like /\-introduction. There are many proof assitants that work with classical logic, e.g. Mizar, HOL, HOL light, Isabelle/HOL ... All of SAT-solving works classically. The novelty of HoTT, and only extension over intensional Martin-Loef type-theory, is the univalence axiom.
- kazinator 11y ago
  A proof in mathematics is not purely syntactic because it's not purely logical. For instance, in some steps of a proof, we do something to both sides of an equation and argue that it is still balanced, based on rules that are outside of logic. Such a step can have a nonconstructive element.
  - mafribe 11y ago
    A proof in mathematics is not purely syntactic because it's not purely logical. This is confusing constructive reasoning with the decision problem for proof validity. They are different things. The very point of logic, constructive or otherwise, or at least one of the key points for having a logic is to be able to decide whether a given proof object is indeed a valid proof. Valid proofs of course typically also make use of non-logical axioms of the ambient theory. If proof-hood is not decidable, it's not a logic. Reasoning is constructive if it avoids certain proof principle like LEM (law of excluded middle) or double negation.
baddox 11y ago
If you limit yourself to only constructive proofs, do you even get the real numbers? I'm not very clear on the definition of "constructive," but given that almost all real numbers are non-computable (i.e. most likely, the set of all real numbers you have ever encountered outside of computability theory has the same cardinality as the integers), it doesn't feel very constructive to me. I've always found it odd that we learn early on in discrete mathematics about how the cardinality of the reals is larger than that of the integers and rationals, and yet it seems like you'll never deal with anything from this larger set of reals unless you're studying computability.
- mafribe 11y ago
  Rest assured that (contrary to j2kun's misleading claims) if some of the world's top mathematicians and computer scientists propose a new foundation of mathematics, they don't forget real numbers. You need to distinguish between non-computable and non-constructive. The proof that the cardinality of the reals is non-countable is perfectly constructive, see [1] for a discussion of these and related issues. [1] https://en.wikipedia.org/wiki/Cantor%27s_first_uncountability_proof#Constructive_or_non-constructive_nature_of_Cantor.27s_proof_of_the_existence_of_transcendentals https://en.wikipedia.org/wiki/Cantor%27s_first_uncountabilit...
  - igravious 11y ago
    Eh? Your very own link says that there is debate within the mathematical community about whether Cantor's uncountability proof is constructive or not. I just realised that in my mind uncountable (not in a one-to-one correspondence with the natural numbers) means non-constructive. For me countability just says that we have a (constructive) method for generating a sequence of what would be all the terms in the sequence (if it were ever to terminate which it doesn't) and no term outside the sequence in a non-repeating fashion that is unbounded. Clearly if some sequence is uncountable it means that one of these criteria fails to hold. Which one? Not the non-repeating stipulation. Not the no term outside the sequence stipulation. It must be the stipulation that every term will be encountered during the generation. So there isn't a (constructive) method for generating uncountable sequences. The reals are uncountable, ergo there is no constructive method for generating the reals. Where am I going wrong? NB: I am not saying that you can't have a method for constructing individual reals like e and pi and so on.
IngoBlechschmid 11y ago
Your comment is a good first approximation to the motivation for HoTT! However, let me add a couple of remarks. Firstly, HoTT can also be used with classical logic, i.e. where you freely use the law of excluded middle. This does not impact the ability to check proofs with the computer in any way. Secondly, HoTT is the first foundation with which computer-formalized proofs of nontrivial theorems in a subject called "homotopy theory" are possible. In theory, this is possible with any foundational theory; but in practice, the necessary encodings to, for instance, Zermelo--Fraenkel set theory, are too involved for computer formalization. In HoTT, one can define (and reason about) the basic concepts of homotopy theory straight from "day one". In contrast, with a more traditional foundation, one needs to setup a host of intermediate concepts first (like the real numbers, topological spaces, homotopies, ...). This is no problem for a trained mathematician, but becomes a nuisance when working with proof assistants. Thirdly, one intriguing aspect of HoTT is that it might be possible to "run" proofs (this is the objective of current research). For example, if you prove that some group contains finitely many elements, the vision is that you could run this proof to find out how many elements it contains. This "computational interpretation" is not unique to HoTT; in fact, this is what the linked nLab article is about. But because of the second point, many more theorems are amenable to such an approach. A last remark, not pertaining to HoTT but constructive mathematics. A simple reason why one might be interested in restricting oneself to constructive arguments is that thereby they are applicable to more general situations. There is a metatheorem to the effect that "a statement with a constructive proof holds in any topos", where "topos" is a precise formulation of "alternative mathematical universe". Such universes are routinely used in several subjects of mathematics, for instance algebraic geometry (after Grothendieck's revolution). There are also other reasons for why it's fun to argue constructively. See for instance these slides: https://github.com/iblech/talk-constructive-mathematics/raw/master/negneg-translation-notes.pdf https://github.com/iblech/talk-constructive-mathematics/raw/... (PDF pages 8ff.)
- mafribe 11y ago
  Very nice descriptions. While constructive reasoning is has many advantages, it has one disadvantage that is rarely pointed out, but sometimes causes real trouble. Let's say we have a formula A which is classically and constructively true. It may be the case that constructive proofs of A are longer and more complicated than classical proofs of A. If you are working with an interactive proof assistant, this may be the difference between the proof automation being able to deal with A automatically or not. This explosion in proof size is the reason why the (perfectly constructive) nominal techniques of Pitts et al have been implemented to a high standard in Isabelle/HOL are are used frequently, but are not really in Coq.
deleted 11y ago
[deleted]
deleted 11y ago
[deleted]
igravious 11y ago
Careful! Here is LEM: ⊢. ~p ∨ p (one of either p or p's inverse must be true -- and thus the other false -- with no third (truth) value allowed), hence also called principle of bivalence. What you wrote is the principle of double negation. In general: (~p ∨ p) ⇒ (¬¬p ⇔ p) but not the other way around if I not mistaken? Please correct me if I am wrong.
- igravious 11y ago
  In other words, what you wrote is that every value when negated twice returns to itself. Here's a truth table of 3 values for the negation operator v | 0 | 1 | 2 -------------- ¬v | 1 | 0 | 2 So ¬¬0 ⇔ 0 and ¬¬1 ⇔ 1 and ¬¬2 ⇔ 2 which satisfies the principle of double negation but not LEM. Correct?
  - IngoBlechschmid 11y ago
    Your counterexample could work, but it is not obvious that it does so. This is because you also have to give definitions of ∧, v, and ==>, and then check that your definitions satisfy the axioms of intuitionistic logic. As stated, your example only shows that one can define a function f on a set which contains more than two elements such that f . f = id. But this by itself is a trivial statement.
    - igravious 11y ago
      Once those definitions are given then my trivial example holds though, correct? Which are you saying; that it is, or, it is not possible to give those definitions?
      - IngoBlechschmid 11y ago
        I didn't check it. If you want to do it (the key step being to verify that the axioms of intuitionistic logic holds for your definitions of AND and OR), you can check Wikipedia for the list of axioms to verify: https://en.wikipedia.org/wiki/Heyting_algebra https://en.wikipedia.org/wiki/Heyting_algebra

mafribe 11y ago

Typing systems (at least some of them) are also logics. This is called the Curry-Howard correspondence (CHC). At first the CHC was made to work for propositional logic only, i.e. logic without for-all and existential quantification. Later typing systems were developed which correspond to logic with quantification. This requires dependent types. However, early typing systems with dependent types had an inelegant handling of equality. Logic needs equality to express things like forall x. x = 3 => x > 2. To overcome this problem, Per Martin-Loef introduced a dependent type-theory (MLTT) with "identity-types" which enables an elegant handling of equality. MLTT and all other extant formalisations of mathematics still suffered from another problem, in that many mathematical constructs are 'morally' the same, but formally distinct. For example you can define a group to be a triple ( G, 1, * ) where G is a set, 1 the neutral element and * the binary operation, or you can define it as ( G, *, 1 ). The former and the latter are not the same thing, but we don't really want to say that they formalise different concepts. This is similar to how in many programming languages certain types are formally distinct but somehow capture the same content. Homotopy type theory (HoTT) overcomes this problem (or parts of this problem) by adding a single axiom to MLTT, called the "univalence axiom" which can informally be rendered as: Things that are 'morally' the same, really are identical. The key idea behind the univalence axiom is that MLTT (and hence HoTT) restricts the mathematical objects that can be constructed such that whenever you have objects O1 and O2 that are morally the same, then there is a function that transforms any construction involving O1 automatically into a construction involving O2 or vice versa, but in a truth preserving way. It turns out that proofs in HoTT are formally similar to certain aspects of geometry/topology. Much of current research on HoTT is about the consequences of the univalence axiom and the similarity between logic and geometry/topology. The key hope in all this is that HoTT will streamline formalised mathematics.

igravious 11y ago
Wonderfully accessible synopsis. One ever so _minor_ point. Did you really mean to say "The former and the latter are not the same thing" or "The former and the latter are not _formally_ the same thing" ??? Here's a fun fact for you, you might enjoy this. I picked up a copy of a 1943, second edition, hardback copy of Bertrand Russell's An Inquiry into Meaning and Truth. (In an antiquarian bookstore for €25, as one does... the colophon even states BOOK PRODUCTION WAR ECONOMY STANDARD) Anyway, chapter XX is titled "The Law of The Excluded Middle" and in it Russell states, "[…] As everyone knows, Brouwer has challenged the law, and has done so on epistemological grounds. He, in common with many others, holds that “truth” can only be defined in terms of “verifiability”, which is obviously a concept belonging to the theory of knowledge. If he is right, it follows that the law of the excluded middle, and the law of contradiction also, belong to epistemology, and must be reconsidered in the light of whatever definition of truth and falsehood epistemology permits." What strikes me about this (apart from the fact that I did not know previously that Russell tackled the question of constructivism/intuitionism so directly) is that he claims that everyone! knows this. If we are being charitable by everyone he means mathematicians, and perhaps logicians, maybe even philosophers, I still think it's quite a broad statement. It shows that the school of the logical positivists springs from Brouwer -- which firstly I was never taught, and which secondly does not appear in, for instance, Language, Truth, and Logic[1] by A.J. Ayer. Finally I can see how the law of double negation becomes an epistemological matter, but not the law of what he calls here contradiction (noncontradiction?). He goes on to disprove the verifiability claim over many pages, and thus constructivism. There's a swipe at Wittgenstein further on still. It's a fascinating text. Russell grapples with mathematical and logical issues in a clear fashion using everyday language. Kind of like what you might get if you took the intro to HoTT and lengthened it and made it more philosophical. [1] https://archive.org/stream/AlfredAyer/LanguageTruthAndLogic_djvu.txt https://archive.org/stream/AlfredAyer/LanguageTruthAndLogic_... ps: is there markup for blockquote on HN? EDIT: clarity, markup, prose style

Kutta 11y ago

Another addendum to the discussion, from an angle more relevant to computer programmers: if we find a computational meaning for the univalence axiom, then it'll be a crazy nuclear weapon of generic programming and code generation. The univalence axiom says that two types are equal if we can convert their values back and forth (without loss of information). For example, one Boolean type may be defined as an enum containing True and False. But we could rename the values to Foo and Bar and it would be still a fine implementation, because it's easy to convert between the two representations. We can imagine more far-fetched representations too, with more complicated conversion functions. But in type theory, if two types are equal, then we can freely substitute one for another in any context! For example, if we have a function "Bool -> Bool", and we know that Bool is equal to Bool2, then we can coerce the function to type "Bool2 -> Bool2". Imagine a complex program that uses a complex piece of data type. If we can provide a correct conversion function to another type (i. e. prove that the type is equivalent to another one), then the univalence axiom can take the conversion function and our program as input, and spits out a new program that uses the new data type, and also preserves all properties of the program. By our current standards of generic programming, this is just insane! Now, the issue is that currently we don't actually have a computational interpretation for the univalence axiom, so the above magic doesn't yet work. But there is meaningful progress towards that, and there are already some experimental implementations that can do some magic, for example this one: https://github.com/mortberg/cubicaltt https://github.com/mortberg/cubicaltt

YorkshireSeason 11y ago
What is the state of the art of the research on the computational interpretation of univalence? What's working, what's not working? I seem to remember that A Jeffrey said not too long ago that he had a working interpretation.
- gallabytes 11y ago
  A lot of work was going into the cubical model, but IIRC they realized it was a dead end about a month and a half ago. Right now the most promising work looks to be formalizing the set theoretic model in NuPRL.

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.

kylebrown 11y ago

In the comments of a recent mathematics-without-apologies blog post[1], there was a back-and-forth between Jacob Lurie and Urs Schreiber (the author of the OP article on nLab). I've been trying to parse the material on nLab for years, good to know I'm not the only one who seems to have trouble with it. A refreshingly blunt discussion, not to be missed! 1. https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-224 https://mathematicswithoutapologies.wordpress.com/2015/05/13...

solomatov 11y ago

Homotopy type theory formalizes informal reasoning style when things which have "the same structure" are considered equal in a constructive type theory setting. Another achievement is formulation of synthetic homotopy type theory, i.e. axiomatic as opposed to based on geometric type theory.

mafribe 11y ago
I don't think synthetic homotopy type theory is known to cover all of conventional homotopy theory, so it's work in progress.

ericbb 11y ago

Check out this Scientific American article[1], especially the video of a presentation given by Voevodsky. Edit: Here's a more direct page[2] if you just want the video. [1] http://blogs.scientificamerican.com/guest-blog/voevodskye28099s-mathematical-revolution/ http://blogs.scientificamerican.com/guest-blog/voevodskye280... [2] http://www.heidelberg-laureate-forum.org/blog/video/lecture-thursday-september-26-vladimir-voevodsky/ http://www.heidelberg-laureate-forum.org/blog/video/lecture-...