Questions about Homotopy Type Theory
Catarina today posted a link to the newly published very interesting work (joint work) on Homotopy Type Theory, largely initiated by my MCMP colleague Steve Awodey and Vladimir Voevodsky a short while ago, and developed with a group of other workers, during a year-long seminar at Princeton. So, let $\mathsf{HoTT}$ be Homotopy Type Theory.
The philosophical claim, which seems a pretty strong one, is that $\mathsf{HoTT}$ is some radically new "foundation for mathematics". Because I've been wondering about this for about a year in relation to $\mathsf{HoTT}$, and have just been teaching Frege's foundations of arithmetic at Oxford, I've got two quick questions.
First, is the following true?
UPDATE (22 June): Ulrik Buchholtz in the comments has kindly answered these for me, both positively. $\mathsf{HoTT}$ extends Martin-Löf's type theory with the Univalence axiom. Because Martin-Löf's type theory contains its own theory of arithmetic (essentially equivalent to Peano arithmetic) it also proves $0 \neq 1$, and the proof carries over.
$\mathsf{HoTT}$ still seems to me a bit unsatisfying as a foundation, both conceptually and epistemologically, because (at least if I understand it right) axioms/rules for arithmetic are assumed, rather than proved -- which is what Frege does in Grundlagen, using second-order comprehension and Hume's Principle.]
The philosophical claim, which seems a pretty strong one, is that $\mathsf{HoTT}$ is some radically new "foundation for mathematics". Because I've been wondering about this for about a year in relation to $\mathsf{HoTT}$, and have just been teaching Frege's foundations of arithmetic at Oxford, I've got two quick questions.
First, is the following true?
$\mathsf{HoTT} \vdash 0 \neq 1$Second, it's not clear to me what the proof is.
UPDATE (22 June): Ulrik Buchholtz in the comments has kindly answered these for me, both positively. $\mathsf{HoTT}$ extends Martin-Löf's type theory with the Univalence axiom. Because Martin-Löf's type theory contains its own theory of arithmetic (essentially equivalent to Peano arithmetic) it also proves $0 \neq 1$, and the proof carries over.
$\mathsf{HoTT}$ still seems to me a bit unsatisfying as a foundation, both conceptually and epistemologically, because (at least if I understand it right) axioms/rules for arithmetic are assumed, rather than proved -- which is what Frege does in Grundlagen, using second-order comprehension and Hume's Principle.]
Yes, it's true. Martin-Löf gives a proof in “Intuitionistic Type Theory”. Since HTT extends Martin-Löf type theory, the proof carries over.
ReplyDeleteThe proof goes as follows: By recursion you can define a function from the natural numbers to the first universe, sending O to the empty type and any successor to the unit type. If you now assume that O is equal to SO (i.e., that there's an element of the corresponding identity type), then by congruence the empty type equals the unit type. Now transport the element of the unit type to the empty type to derive the desired contradiction.
Note that you need a universe for this proof to go through! (See, e.g., Jan Smith 1988: The independence of Peano's fourth axiom from Martin-Löf's type theory without universes.) However, a tiny universe consisting of just the empty type and the unit type will do.
Ulrik,
ReplyDeleteMany thanks!
I was just going to have another look at Martin-Löf's papers to see how he does this. Yes, I see how it goes. In a sense, though, Martin-Löf's system assumes as axioms/rules,
0 in N
0 in N / 0' in N
etc.
These are basically the Peano axioms. But these axioms aren't themselves proved in Martin-Löf's system, or in HTT. So, the worry is that this contrasts with what Frege did in 1884: i.e., Frege proved the Peano axioms, from comprehension along with the cardinality axiom (HP).
This is why I'm worried that HTT isn't a foundation; but more like a reformulation.
But, probably (I"m guessing), one can take HTT, and simply replace the axioms/rules for N that Martin-Löf gives, and use something close to (HP) along with some type machinery, and get the Peano axioms out as theorem.
Cheers,
Jeff
Jeff,
ReplyDeleteWhen studying type theory formally, it is often convenient to add the rules for the natural numbers as an inductive type explicitly. That way, for instance, we can study how much strength is gained by adding rules for other inductive types.
But it's perfectly coherent to go straight to a formulation where a whole range of inductive types are introduced schematically. That brings us closer to the foundational level, I think.
It's interesting that HTT proposed a new kind of inductive types, higher inductive types, that are also generated by paths, paths-of-paths, etc. With higher inductive types (and coinductive types) you have something that suffices for most of mathematics.
Frege's approach requires full-on impredicativity, if I'm not mistaken? So it's a far less parsimonious foundational system in terms of proof-theoretical strength.
There are of course type theories with impredicative function types, and those allow you to code, say, the naturals impredicatively, but I don't know whether this is compatible with univalence.
It may be a matter of taste as to what one wants in a foundation, but I think for instance something like Martin-Löf meaning explanations are worth having. And it's kind of a problem that so far the univalence axiom has eluded attempts to justify it via meaning explanations! This issue is probably related to the question of a proper computational interpretation of univalence.
Ulrik,
ReplyDeleteGreat, thanks. Yes, Frege's second-order system has fully impredicative comprehension, so it's powerful. It interprets full $Z_2$. But people have studied what one gets with predicative comprehension. Richard Heck and Oystein Linnebo know more about this stuff than I do. I don't know if anyone studied the intuitionistic version of Frege's system.
Adding rules/axioms for N is ok, I guess; but part of the foundational and conceptual attractiveness of Frege's theory is the derivation of everything from the SO logic, plus just an abstraction principle for cardinals. One can of course go up through a type hierarchy - this is more-or-less what Russell and Whitehead did, and Church later. Predicativity issues certainly arise here.
Perhaps part of the trouble with "meaning explanations" was that some things were postulated as really "just explaining meanings" and then turned out inconsistent! This happened with Frege's Basic Law V; and Quine gave an inconsistent theory; and, something similar happened with Martin-Löf as well, with Girard's paradox. This was one of Godel's (and Quine's) points against Carnap's views on logicism, that mere meaning stipulations couldn't guarantee consistency.
I wonder if there is some sort of canonical, category-theoretic, model defined for HTT?
Cheers,
Jeff
Jeff,
ReplyDeleteI agree that it is amusing (and troubling) that we have these examples you mentioned where the theories turned out to be inconsistent, even though they had a “meaning explanation”. I haven't actually seen Martin-Löf's 1970 “explanation” of type:type, but I should think it can't have been anything like the explanations for the other terms in type theory, where it is laid down what a canonical element of a type is, etc.
Anyway, what we are after, that is more than consistency, is a nice computational behavior: canonicity (e.g., every closed term of type nat should reduce to a numeral). I think there's a connection between having “good” meaning explanations, and canonicity, but I'm not sure how to say that precisely.
For HTT with the propositional univalence axiom, there are as far as I know only Voevodsky's model in simplicial sets, and other homotopy-theoretic models, but no computational model. Of course there is a classifying category, which is the initial model, but it's not canonical in the sense you're asking, I think.
Ulrik,
ReplyDelete(Are you Ulrik Buchholz ...? )
I guess there's a lot of proof-theoretic work on Martin-Löf's type theory, MLTT. I know Church's type theory, but that's it, and haven't kept up with all the other bells and whistles!
Now I check a bit -- I hope I understand which type theory Rathjen means! -- CZF (constructive ZF) can be interpreted into MLTT.
But, with Univalence added, HTT could be stronger than MLTT; maybe HTT is conservative over MLTT. So, perhaps if uses of Univalence can always be eliminated in proofs (e.g., of arithmetic sentences), then conservation would follow.
Cheers,
Jeff
Jeff,
ReplyDelete(yes, that's me, but with a ‘t’ before the ‘z’ – I've updated my Google Blogger profile to display my full name.)
Yes, Aczel showed how to interpret constructive set theory in type theory. For CZF you need one universe and the inductive type of ‘iterative sets‘. These form the type-theoretical version of the cumulative hierarchy, so to speak. A stronger type theory can interpret a stronger set theory, e.g., the Calculus of Inductive Constructions interprets IZF.
As far as I know, it's still unknown whether univalence is conservative over the rest of type theory (for statements of arithmetic, say), but it is believed to be. The idea is that there should be a constructive version of simplicial sets that allow you to build the Voevodsky model internally in type theory. But Kan complexes are not well-behaved constructively (we want function to give horn fillers, but then we need coherence conditions on the fillers, etc.).
Cheers,
Ulrik Buchholtz
Ulrik,
ReplyDelete(Apologies for the missing "t"!)
Thanks for the background on constructive set theories.
Here's a wild stab at a proof-theoretic approach on conservation.
How does an application of Univalence work in a proof? Intuitively, it seems like we have two things, A and B; we know they're isomorphic. Univalence then says $A = B$. So, we can just reason with A from now on, to conclude "A has property P", after, say, 200 further proof steps. And we get "B has property P", by one further proof step, by substitution.
But my guess is that, instead of using Univalence, each subsequent proof step with A (having used Univalence) can be "copied" with a corresponding step for B. And if we got "A has property P" after 200 steps, then we shall also get "B has property B" with a corresponding 200 steps.
Does that sound plausible?
Cheers,
Jeff
Jeff,
DeleteHoTT has a very interesting view of equality. Every type $A$ (including universes) comes with identity types $x =_A y$ for $x,y$ of type $A$. An element $p:x =_A y$, often called a path by analogy with topology, is a reason to identify $x$ and $y$. Such paths can be inverted and composed to give symmetry and transitivity of these motivated identifications. In a HoTT proof of these paths are always present. Univalence is (in part) an introduction rule for paths of type $A =_U B$, where $U$ is a universe containing $A$ and $B$. Informally, univalence says that $U$-paths $A =_U B$ are equivalences $A \simeq B$.
The meaning of equivalence $A \simeq B$ (which is not quite the same as isomorphism) does give a way to transform statements relative to $A$ into statements relative to $B$ but there are many layers to this. I suspect that there is a conservation argument of the type you suggest at least for some restricted properties P. This would be fun to investigate further but I don't think it will be straightforward task.
Best,
François
Many thanks, François
DeleteI'd appreciated the equivalences are more complicated beasties. I was thinking of some very schematic way of how the proof-reduction might work.
Univalence lets us introduce $A =_{U} B$ when we've got equivalence of $A$, $B$. We can then reason about $A$ and transfer to $B$ at the end by an elimination rule, analogous to the usual rule for $=$.
Sounds tricky though!
Cheers,
Jeff
Jeff,
ReplyDeleteI think your conservation proof idea might work for univalence formulated as a rule of inference for closed terms. In that case, we should be able to do as you propose by induction on derivations. But with a term implementing univalence, it's much harder, I think. Compare the situation for function extensionality (in $\mathrm{HA}^\omega$, say). The extensionality rule is pretty innocuous, while the axiom is serious business.
Cheers,
Ulrik
Ulrik, I see what you mean, yes. Sounds like a proof reduction is going to be highly non-trivial ...!
DeleteThe model conversion method, I guess, would try and show how to convert an MLTT model $\mathcal{M}$ to a "Voevodsky model" $\mathcal{M}^{V}$ that is still an MLTT model, and somehow has the required paths added, so it satisfies Univalence. I guess this is all kind of obvious for people who have thought about the consistency/conservation problem for Univalence though, so it must be quite hard to work out.
Cheers,
Jeff
Thanks for your interest in our book.
ReplyDeleteWe decided not to address meta-theory in the book, but these are interesting questions:
A conservativity result for univalence (for groupoids) is here:
http://arxiv.org/abs/1203.3253
A constructive model for univalent type theory in constructive set theory (or type theory) is here:
http://uf-ias-2012.wikispaces.com/file/view/semi.pdf
This model gives a computational interpretation for univalence by reducing it to type theory without this axiom.
A more operational approach can be found in the work of Harper and Licata.
Finally, Peter Dybjer has started to work on meaning explanations for univalence.
Bas Spitters
Many thanks, Bas.
ReplyDeleteBoth papers contain good answers!
(I'd seen an earlier version of Schulman's paper before, but admittedly, I find it vary hard going - thanks for linking to it.)
Cheers,
Jeff
At least Martin-Löf's type theory is essentially based on the idea of "propositions as types" (a proposition is identified with the type of its proofs) - which in turn takes for granted the intuitionistic notion of absolute provability. (And I, for one, have always found that notion deeply unclear...)
ReplyDeleteIs HoTT founded on the same idea?
Thanks, Panu,
ReplyDeleteI don't know the answers to these things. I know Russell's and Church's, but not Martin-Löf's type theory. However, the "propositions-as-types" view does seem to play a role in the HoTT book, yes. (This isn't how I'd use the word "proposition", so it takes getting used to.)
Cheers,
Jeff