Homotopy Type Theory

Since fidotron has been piled on, let me defend the point in his/her post. Good mathematics has come out of being worried that what other mathematicians have done isn't quite right, and I think the perspective of the article doesn't acknowledge that.

For example: Cantor's theorem is quite true, only cranks doubt it [1]. But many mathematicians take it to have the corollary that cardinalities greater than that of the natural numbers exist, which does not follow: it is perfectly coherent to say that constructions such as the power set of natural numbers do not exist as a definite whole, and so do not have a cardinality. These kinds of doubt have driven constructivism which has led to interesting work in topology, measure theory, and type theory, and led to such useful applications as calculators for exact real arithmetic.

Cantor's paradise seems to be coherent (likewise I would be deeply surprised if large parts of mathematics turned out to be misconstrued) but the assumptions of large cardinal set theory are grandiose and poorly justified, and yet for a long time those people who wondered if it was wise to embrace the whole edifice were marginalised. It seems that now there are many more mathematicians who are interested in revisiting this perspective [2].

To put Wiles' metaphor in perspective, it is good if some mathematicians step outside the mansion from time to time, to see if the superstructure is up to all the crashing about that happens in the dark rooms.

[1]:…

> The overlap of mathematicians who care about category theory [...] and mathematicians who program [...] is pretty much zero. You probably won't find your algebraic topology professor programming

Well, unless perhaps s/he has some involvement in a project like this one http://comptop.stanford.edu/ ("The overall goal of this project is to develop flexible topological methods which will allow the analysis of data which is difficult to analyze using classical linear methods"; first named person in left sidebar is an algebraic topologist).

Or this one http://www.esf.org/index.php?id=8764 ("Applied and Computational Algebraic Topology"; first named person on steering committee is an algebraic topologist).

Or this one http://munkres.us.es:8080/groups/catam/ ("Computational Applied Topology and Applied Mathematics"; directory is an algebraic topologist).

Or, turning away from algebraic topology as such to mathematics inspired by algebraic topology and involving both category theory and programming: http://homotopytypetheory.org/ ("... new program for a comprehensive, computational foundation for mathematics based on the homotopical interpretation of type theory. [...] currently being implemented with the help of the automated proof assistant Coq"; note that in practice doing nontrivial things in Coq is a matter of functional programming).

For sure there are plenty of mathematicians (in algebraic topology and elsewhere) who don't program, but I think the intersection between…

This is fascinating to me. A couple comments and links.

Here is a course on proof theory that uses Coq [1]. It is actually the course that Vladimir Voevodsky took when he was trying to understand proof and type theory [2], [3]. While writing the midterm paper, he discovered homotopy type theory [4]. More details on the bitcoin scripting language can be found in the excellent blog post by Michael Nielsen[5].

If the escrow model is implemented, you can actually imagine the mathematical proof market maker acting like a bank, loaning out or otherwise investing bitcoins while the world waits for a verified proof; say, of the abc conjecture [6a] or the goldbach conjecture [6b]. This might be one small way to disrupt Wall St [7a], [7b]. In particular, such a market, when more highly developed, provides skilled mathematicians and scientists incentives to work on math and ( computer ) science problems in an open source format that benefits everyone - since everyone can look at and learn from their proofs - rather than quantitative trading in a closed format that actually causes long term social harm and political instability [IMHO]. I am thinking here of Goldman Sachs and Renaissance Technology founded by James Simons. Imagine if an incentive structure existed that encouraged all these smart folks to work on what is essentially verifiable open source software [8].

[1] http://www.cs.princeton.edu/courses/archive/fall09/cos441/index.php
[2]…

This is a very good thought. Some current projects are trying to develop computable mathematical foundations in a more structured way. Homotopy type theory (http://homotopytypetheory.org/) is one example that has a lot of buzz around it just now, but automated theorem proving has been trying to work with higher-order concepts for ages now.

In the classical approach of "compiling" everything into sets/logic/etc., you end up with just the assembly language problem that's being discussed, where all the high-level structure vanishes. In order to do your bottom-up approach instead, one of the things that needs to happen is to make the theory really compositional, so that once you've defined some abstraction or higher-level concept, you can use it in constructions and proofs without having to break the abstraction. You don't need to know - and in fact you shouldn't be able to find out - just how the natural numbers were constructed, as long as they work by the right rules. This motivates the use of type theory to describe mathematical objects, and say which operations are allowed. We want to be able to add two numbers and get another number, but we don't want to be able to intersect two numbers as if they were sets, even if they happen to have been built out of sets.

So I think you are right - or at least, there are plenty of people who agree with you that this is a good idea. It is difficult to actually do, of course, but that's life.

>>So I wonder what he thinks of this new univalent foundation.

The Homotopy Type Theory (HoTT) book[1] puts forth a possible interpretation of Conway's thoughts about univalent foundations in section 11.6 (look at the bottom of the page for the following very selective and paraphrased quote):

"[...] Conway's point was not to complain about ZF in particular, but to argue against all foundational theories at once [...] One might respond that, in fact, univalent foundations is not one of the "standard foundational theories" which Conway had in mind, but rather the metatheory in which we may express our ability to create new theories, and about which we may prove Conway's metatheorem."[2]

[1] http://homotopytypetheory.org/book/

[2] http://www.math.ntnu.no/~stacey/documents/HoTT-online/main126.xhtml

EDIT: I forgot to mention that Voevodsky's definition of "Univalent Foundations" seems to be used interchangeably with the term "Homotopy Type Theory", but in Voevodsky's mind there is a sharp distinction[3]. Voevodsky tried to make this clear in an HoTT Google Groups email thread with the following statement: "HoTT is the study of the type-theoretic approach to the meta-theory of the Univalent Foundations."[4]

[3] http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalent_foundations

[4] https://groups.google.com/forum/#!topic/homotopytypetheory/zEixM1M3ZDQ%5B1-25%5D

> Prop vs Decidable - I vaguely understand the distinction, but can use more examples. Also would like to know does this relate to the noncomputable property.

My path to this subject was tortured, so sorry if I don’t account for Polysemy etc.

With Prop, I think what you need to dig into is ‘non-computational’ not ‘non-computable’.

Mere propositions is probably best viewed with Homotopy Type Theory[0]

Two proofs (t1,t2) of the same proposition (p:Prop) which are definitionally equal are proof irrelevant, meaning that all they carry is the proof p is true.

This paper [1] may be helpful but the difference between groupoids and subsingletons with classical mathematics is challenging for many of us.

Hopefully this helps in your journey.

Also remember that with classical set theory the internal and external proposition truths are different, the Curry–Howard correspondence is to constructivist from lambda calculus, you don’t have PEM etc…

Remember DGM[2] shows that finite indexing or projection is PEM

Good luck and I hope you continue to share your journey.

[0] https://homotopytypetheory.org/wp-content/uploads/2013/03/hott-online-323-g28e4374.pdf

[1] https://jesper.sikanda.be/files/definitional-proof-irrelevance-without-K.pdf

[2] https://ncatlab.org/nlab/show/Diaconescu-Goodman-Myhill+theorem