Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
How would HoTT fare? Do people think this way of assessing complexity is illuminating? I don’t see why judging something as a ’hack’ is tied tightly to complexity in his sense.
I think there is a precise sense in which HoTT is “more primitive” and hence more fundamental than Set theory, and that explaining this to set theorists would be an important task of homotopy type theorists.
When I once tried to explain this at homotopy type theory FAQ it resulted in a strange exchange that puzzles me to this day (here), and in the end I bowed out and replaced the proposed explanation (still visible in revision 19 here) by the small paragraph that is now here.
Perhaps with the resources of Mike’s 3-theory account there could be a less puzzling conversation.
Re #2: From Wiedijk’s PDF:
A reader comments: After Thorsten Altenkirch read this paper his reaction was:
I can’t help making the obvious comment that simplicity can’t be measured by size. Actually, I often find that the contrary is the case that simpler systems are slightly longer than more complicated ones.
E.g. if you look at some of these obfuscated C-programs which are very short but doing something very subtle (people sometimes put them into their sigs), would you call them ‘simple’? Are those not precisely what people call a ‘hack’?
I mean I think it is a good idea to look for something which short and simple. And obviously length can be more easily measured than simplicity. It is just that you say we measure the size to find out which one is simplest.For the record: I agree with Thorsten that simple and short are not the same thing. (I had a remark about this, but somehow it did not survive my editing the paper.) So I now put Thorsten’s comment in, to address the point.
So no, no one really believes this is measuring simplicity or assessing complexity, except in a computer’s opinion.
(I read it to find out about this “LF/P” system. XD)
So no, no one really believes this
I suspect that if you’d ask for opinions on FOM, you’d surely find that several people there do believe just this. The exposition of “the point of structural foundations for classical set theorists” that would help them see the light has not been written yet, it seems.
I think the question of whether encoded system size is a useful measure of a foundation is a separate issue than structural vs traditional foundations. Even if you’re right that several people take these measurements seriously, I would personally conclude just that those several people are silly.
Certainly a system that takes dramatically longer to spell out has a disadvantage. (Which might be made up for in other ways.) But in Wiedijk’s examples, the differences are not dramatic. (ZFC is unexpectedly short, Martin-Löf type theory is expectedly longer, but only by a factor a little over 2. I actually expected a bigger difference, which I still would not consider a huge problem. Now cubical type theory… hoo boy, they might have a problem.)
Re #3,4: I read the old “For foundationalists” section. It says:
Now type theory is a foundational system that is at that same “lower” level of foundations as first-order logic.
As David suggests in #4, this assertion can probably be understood in terms of Mike’s notion of n-theories. A particular dependent type system, as well as first-order logic itself, are both supposed to be 2-theories in this approach. Meanwhile, set theories are 1-theories.
(But I’m skeptical that it’s useful to regard dependent type systems as 2-theories, rather than 1-theories, for foundational purposes.)
I would personally conclude just that those several people are silly.
Absolutely so. It is not out of the ordinary in academia that one group of researchers eventually discovers that another group is being silly, I’d have more contemporary examples on offer…
What I keep trying to say is that, in such a situation – while it is tempting to just lean back, arms crossed, feeling smug – the right thing to do is to write that review (and be it a quick FAQ) which explains it all to the non-initiated, making them see the light.
Here, I would be surprised if it is necessary to invoke a novel proposal for a concept of “$n$-theories” to explain something standard that has been clear to the experts all along; but maybe it makes the question gain enough novel interest to make it seem worth expanding on again.
to explain something standard that has been clear to the experts all along
I’ve lost track of what the ’something’ is here. I brought up Mike’s $n$-theories in #4 as a way of casting light on whatever it was that was unclear in discussions amongst HoTT experts (e.g., Mike, Bas and you).
Where you say in #72 of that old discussion “I am checking with an expert on what the politically correct way is to say that FOL is part of type theory”, I now have a much clearer idea of what you can say, and a key part of this is saying what you mean by ’FOL’ and by ’type theory’. Unqualified, both are ambiguous, especially the latter, which can mean a 1-, 2- or 3-theory.
It’s changed how I see the space of logical systems. As Mike writes
the $n$-theories perspective leads us to a different view of its relationship to FOL and DTT: instead of placing the three on an equal footing as foundational choices to be compared, FOL and HOL are placed in one group that is distinguished much more sharply from DTT than from each other. Kind of like how biologists sometimes have to reshuffle their division of species into genera and families upon learning from genetic evidence that different-looking species are actually closely related.
It also makes sense of how modalities express a ’metatyping’ of types.
I must say that I am with Urs on this one. I think that the edit which Urs proposed, that he linked to in #3, is perfectly fine as a summary/introduction/overview. Experts in anything have a tendency to pedantry, but I think the basic point that Urs was making, namely that first order logic is at a lower level than set theory, and that type theory is at a lower level than first order logic, is perfectly valid. There is no need of any notion of $n$-theory to express that.
namely that first order logic is at a lower level than set theory, and that type theory is at a lower level than first order logic
…and finally that homotopy type theory is at a lower level than type theory, in that again we remove an axiom from the latter (uniqueness of identity proofs) to arrive at the former.
It’s sheer beauty.
Well, I’ll continue to thank Mike for giving me a way to disambiguate when people say “type theory”.
I am not leaning back feeling smug. Maybe you didn’t realize, but we probably don’t agree on many points in this debate. I was keeping cool, not wanting to look like a troublemaker.
First, I guess I should address the “puzzling exchange” about your old “For foundationalists” section. I think Mike and Bas were just trying to correct technical inaccuracies in what you wrote, while keeping the intuitive point the same. (That DTT is more fundamental than set theory in a sense. As I’ll explain below, I don’t agree with this, so do not expect much help from me improving the argument.) I think it was your behavior that’s puzzling. In the face of these technical corrections, you retracted the whole argument.
I am mostly a traditional foundationalist, to the extent that I’m a foundationalist at all. John Baez said that mathematics really needs “entrances” not “foundations”. Maybe so; but foundationalists study foundations anyway. Foundations are not the same as foundational theories. Many foundational theories are getting at the same foundational ideas in a different way. That’s a different entrance, not a different foundation. If someone proposes Foo as a new foundation, traditionalists cannot be blamed for taking this proposal seriously. Beware that proposed foundations are judged quite differently than proposed foundational theories.
So maybe you should think twice before proposing any new foundation. This may not be what you’re really trying to do. The whole debate may very well be a big misunderstanding. “Yes, Foo is a new [entrance]!” “No, it’s obviously not a new foundation.”
I’m going to give my belief, which I bet is pretty unpopular around here. I probably will not be winning any points for this, despite the warning above to not misinterpret this. Things like type theory and structural set theory are not fundamentally different from traditional set theory. They’re good. Great, even. And they’re new in other ways. But not as a foundation of math. (Actually, there may be forms of constructivism based fundamentally on type theory. These would not be the usual one, of not assuming LEM or AC. Anyway, HoTT is not fundamentally constructive.)
I say that to contrast with Univalent Foundations (UF), which is fundamentally new. (And HoTT itself is not, though it helps make the point that UF is.) I don’t think anyone would deny that equality is fundamental in math. UF proposes that equality is path spaces. From a traditional perspective, this is not a legitimate explanation of equality.
I spent years liking HoTT, but being grumpy because people were calling paths equality, and I thought that was fundamentally wrong. But I changed my mind: it might be OK. And if it is, then this new understanding of equality is absolutely providing a new foundation, in my opinion.
If you can convince the real traditional foundationalists (whoever they are) that UF is a truly new and legitimate explanation of equality, I bet they will agree that it’s a new foundation. Then the question is whether it’s actually good. But by then you’ve gotten further with them than you probably ever will about type theory or structural set theories.
So I can give dilettante advice about how to try convincing them about that. That’s the way in which I think we’re on the same side. (Other than the original thing about Wiedijk’s measurements. That’s a different argument. That argument is not worth developing because it’s no big deal.)
From a foundational perspective, things like typed vs untyped, and whether to work up to isomorphism, are pragmatic, technical issues. They are important in practice, but not fundamental. You can change all that stuff; it doesn’t take any soul searching; you just need to handle the technicalities correctly.
HoTT is an “entrance” to UF via dependent type theory. One could step back and ask if that’s even the best approach to it. I suspect that, in the short term, it’s not. And I say that as someone who likes dependent type theory way better than higher-dimensional math, with its coherence problems.
Trying to put myself in homotopy theorists’ shoes, I do not see why it’s not superior to simply regard HoTT notation as informal notation for model category-like presentations. This can be done on top of traditional set theories. My impression is that this is what HoTTists are in fact doing, because the technology for rigorously interpreting formal HoTT is currently so lacking.
But I see no need (just for the sake of UF) to change that. Remember: a foundation is not a foundational theory, so you don’t actually need to replace the foundational theory; you can just build on top. Set theory builds on top of syntax. Syntax is more fundamental than (infinite) set theory. That is no reason to deny the foundational legitimacy of sets. So UF can build on set theory. This realization is how I accepted UF as (potentially) foundational. Because building on DTT is not really avoiding the foundational priority of set theory. So it needs to be OK that set theory is more fundamental.
Building on a traditional set theory would be just a technical decision. And it seems like a smarter move than making foundationally irrelevant changes to the set layer at the same time as you push UF. In addition to being technically easier, it would combat false associations with other foundational proposals, like constructivism and invariant-but-not-univalent type theories.
…and finally that homotopy type theory is at a lower level than type theory, in that again we remove an axiom from the latter (uniqueness of identity proofs) to arrive at the former.
This is false. There is no (consistent) type theory that you can remove UIP from to get HoTT, because univalence contradicts UIP. This was one of Mike and Bas’s points: from ITT, you can extend to either ETT or HoTT.
This is false. There is no (consistent) type theory that you can remove UIP from to get HoTT, because univalence contradicts UIP
It’s usually called HoTT before adding UV, because it’s about homotopy even without UV. The UV axiom makes it be about homotopy toposes.
The point I am making is not false but trivial. You can choose to add axiom K, to your ML type theory, or you can omit it.
It was the historical route that Martin-Löf first had that axiom, and then removed it because it interfered with some decideability. But after removing it people were puzzled as to the resulting meaning of the identity types.
HoTT is the resolution of this puzzlement: The understanding that MLTT without that axiom is a type theory with homotopy theoretic interpretation.
It’s usually called HoTT before adding UV, because it’s about homotopy even without UV.
I don’t think that’s the usual terminology. What you’re calling HoTT sounds like what I call ITT. ITT is potentially about homotopy, but also potentially not about homotopy, due to the ETT extension.
It was the historical route that Martin-Löf first had that axiom, and then removed it because it interfered with some decideability.
Actually, at first MLTT did not prove UIP. Then extensional type theory (ETT) added “equality reflection”, which combines with J to prove UIP. It’s equality reflection, not UIP, that interferes with decidability. So equality reflection was removed again. Axiom K was later proposed (I think by Hofmann and Streicher) to get back UIP, and most implementations of derivatives of MLTT use K by default.
But after removing it people were puzzled as to the resulting meaning of the identity types.
HoTT is the resolution of this puzzlement: The understanding that MLTT without that axiom is a type theory with homotopy theoretic interpretation.
That all sounds right to me.
Regarding #14: the following part of Mike et al’s work is clearly significant, new, and valuable.
Now I can finally describe the programme that Dan, Mitchell, and I are undertaking. Given a particular 3-theory, we aim to describe a particular deductive system for syntactic 2-theories in that 3-theory, and associate to any such syntactic 2-theory D a specific deductive system for syntactic 1-theories in D, such that the latter (1) indeed has the correct semantics, i.e. it presents the correct semantic 1-theories, and (2) has the good meta-theoretic properties that type theorists want, such as cut-elimination, normalization, and canonicity. For a particular syntactic 1-theory, the deductive system that we get is not usually identical to any existing deductive system for that 1-theory, but it is almost always related to it by a fairly direct translation (in general, rules of the existing system tend to translate into the successive applications of two or more “more basic” rules in our system).
But I don’t think the notion of n-theory here provides any significant insight into distinguishing type theories syntatically, and I don’t think Mike was claiming that. It is, and always has been, evident that there is a distinction between fixing rules and fixing generating types and terms once one has fixed rules, and also that the boundary between these is fluid (e.g.. one can always move a certain generator into the fixed rules). Mike et al’s work does not say anything new in that respect (i.e. about differences in type theoretic syntax), it is rather about treating meta-properties of certain type theories generically.
distinguishing type theories syntatically
I’m having to guess what you mean by “type theories”. It’s like a discussion of animals where we don’t specify whether we’re talking about species, genus, family, order, class, etc.
What are simple type theory and dependent type theory examples of? What are extensional ML type theory and HoTT examples of? You’re surely not got to say they’re all type theories.
I don’t think the meaning of ’type theories’ is relevant here: animals are animals regardless of what species etc they are, and type theories are type theories. As an aside, there need not be one single definition: my favourite definition of a type theory or animal might differ in particulars from yours, but it is obvious that there is a sufficiently universal concept which we are talking about.
There are a million ways to categorise things, and it is perfectly possible to formulate in simple terms flavours of type theories into which the examples you list fall. As I say, the new terminology of ’n-theories’ can be helpful for the particular purposes Mike et al have in mind, e.g. in allowing a concise/precise formulation of their theorems, but I don’t think it expresses anything new with regard to saying how one particular type theory differs from another, and nor, to the extent it matters, do I get the impression that Mike was in fact claiming this.
1 to 21 of 21