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.
I’m giving a talk tomorrow at the grand sounding World Congress of Philosophy. Slides are here. Comments are very welcome.
second sentence on slide 4 has no question mark (maybe it does not want one, just saying)
slide 8: maybe make the word “fewer” italic or even boldface, to bring out the message?
slide 9, first sentence: does this need some interpunctuation?
slide 10: not sure if I see how to read (?)
slide 11: this reminds me that we should condense and record some of the early history of the concept of cohomology that has been discussed on the AlgTop mailing list in the last days. That was interesting…
slide 13: for the newbie the headline may be hard to parse in the intended bracketing. Maybe make the first three words and the last three words italic, to indicate that they belong together?
slide 13, “wedded together”: maybe do something to the formatting that makes sure people see that this is a major punchline
Nice!
slide 21: “see later slide” – is there a later slide about this?
Only other thought is a quibble that if you use \uncover or \pause instead of \only, then the text that carries over won’t jump up on the page when new text appears below it. (-:
Thanks both!
Urs, I’ve implemented your suggestions, except for changing . It’s . Haven’t people gone over mostly to the notation?
I haven’t heard about the AlgTop discussion.
Mike, I meant slide 30, listing work which does maths in HoTT. Should add the HoTT book.
I always mean to look up this Beamer functionality - now I know.
What were you planning to say about Husserl?
is pretty common, but not universal. For instance, people in cubical type theory often write and to distinguish the path-type defined by abstracting over the cubical interval from the id-type defined in a sneaky way from it that satisfies definitional -reduction. It’s true that subscripting an equals sign gets hairy-looking and hard to parse when, as here, the subscript is any more complicated than a single letter.
Looking forward to hearing how the talk went!
Thanks, of course I know the “=”-notation for identity types, but somehow I completely misread the subscript. All clear now.
Todd, I’m just indicating there that we might want to check back on the philosophical precursors of Martin-Löaut;f. There’s quite an industry in commentary on Husserl, but very little of it deals with him as the student of Weierstrass. Gian-Carlo Rota took him as his philosophical master.
Well, at least there was one request for my slides, from a gentleman from Inner Mongolia Normal University. Given the city that’s situated in, Hohhot, it’s crying out for a homotopy type theory conference with an excursion to the steppes.
Since I’ve been asked, what should we make of the range of proofs about the existence of models for HoTT/UF? I know there’s the fiddly detail of substitution being strict unlike pullbacks, and that many attempts have been made to circumvent this. And accepting that it is very justifiably considered that some model has been rigorously constructed, is there some paper to point to which would satisfy a very stringent logician? The removal of Voevodsky’s name from the standard reference, The Simplicial Model of Univalent Foundations (after Voevodsky), didn’t help appearances.
How does your very stringent logician feel about the initiality conjecture/theorem? That’s the reason Voevodsky’s name was removed; the paper is fully rigorous about constructing a category with all the sufficiently strict structure that’s expected to figure in the initiality theorem, the issue is that the initiality theorem for the type theory in question hasn’t actually been written down completely.
the initiality theorem for the type theory in question hasn’t actually been written down completely.
so you hold it to be a theorem rather than a conjecture? I know that it is held to be a true result, but I gather Voevodsky didn’t want to consider a theorem.
Or is the work on this problem sufficiently far advanced (I guess Peter L’s recent work?) so that it is now just a matter of ’writing it down completely’?
How does your very stringent logician feel about the initiality conjecture/theorem?
You give the answer yourself
the initiality theorem for the type theory in question hasn’t actually been written down completely.
I was hunting about the nLab for comments on initiality. This section says most. Perhaps it deserves its own page.
There’s a link there to internal logic of an (infinity,1)-topos which is funny to read now – it’s like a time capsule.
With material so scattered it’s hard to keep relevant pages up to date.
Does your point come in here, Mike, that there’s a question of the value of working out initiality for one specific type theory? It might not even be quite the variant type theory people end up using. Much better to derive a general result for all type theories (of a certain kind).
The claim was put forward that working out where proofs get difficult and resolving these difficulties often leads to useful and important new techniques or concepts, in answer to which I aired my doubts as to any general principle. Sometimes resolving a proof can work with fiddles and tricks, and no great insight is gained. Strategic decisions can only be made by those on the ground.
But still, from what you’ve said, in the strictest sense, my interlocutor was right to say we don’t yet have a proof of consistency relative to ZFC.
David, in case you haven’t seen it yet, also check out the recent discussion on the HoTT mailing list here, trying to figure out what the problem even is. (No conclusion reached, it seems.)
Important seems to be not to get distracted by every red herring thrown. For most of what you and us here are interested in regarding interpretation of HoTT in -toposes, it matters that there is the one interpretation that we have in mind, but not whether that’s the unique interpretation possible. The latter statement is initiality. Should it fail, it would follow that there are in addition “exotic” interpretations. That wouldn’t invalidate most of what we care about here.
Urs, even weak initiality isn’t yet proven, which means there isn’t a general way to interpret syntax into any model at all. So even the “one interpretation we have in mind” isn’t completely rigorously established.
Thanks, Urs, I did read that with interest.
Re #14: yes, I think I’ve heard this point most from Peter Lumsdaine: no one wants to put in the tedious technical effort to prove initiality for only one particular type theory, no matter which, since there are so many different type theories with more always being invented. Clearly what is needed is a general theorem.
Re #12, you didn’t quote my first sentence in which I said “conjecture/theorem”. After that I abbreviated it. I’m not sure what I would call it, myself. It feels funny to call something a “theorem” when no one has actually written down a proof. But in my idiolect a “conjecture” has a great deal more uncertainty about its truth than I feel this statement does. Maybe we could hedge and talk about the “initiality property”.
I had an interesting conversation with Peter L the other day about the extent to which it’s allowable to regard type-theoretic syntax as “notation” for category-theoretic operations, even in the absence of an initiality theorem. On one hand, there’s an argument that it’s unproblematic: after all, mathematicians introduce lots of notations all the time (including variable-binding ones) without formally proving their correctness. (The situation for string diagrams is arguably even worse than that for type theory.) For meta-theoretic analysis we certainly need a formal treatment of notation, but for simple everyday use maybe we don’t.
On the other hand, when things scale up by orders of magnitude, it becomes harder to justify treating a syntax as merely “informal notation”. It’s one thing to write a line or two of type-theoretic syntax and call it notation for an operation in a topos; it’s something else to formalize the odd-order theorem in Coq and then conclude that it’s therefore true internally in any topos. Peter suggested a rule of thumb boundary as whether, if an annoying referee insisted on it, it would be feasible to rewrite all the type-theoretic notation by hand in ordinary category-theoretic syntax.
Regarding proofs of consistency relative to ZFC, it’s worth noting that there are also other ways to reach such a result. For instance, Simon Huber proved that cubical type theory satisfies canonicity for natural numbers, and it’s expected to satisfy more general normalization and canonicity properties. Canonicity at the empty type implies consistency, since there is (by definition) no canonical term belonging to the empty type, and hence (given canonicity) no such term at all.
Although I doubt that any real conceptual benefit would be gained by proving initiality for one particular type theory, such as Book HoTT, I think it’s possible that there are important insights to be gained by completing a general initiality theorem. One of those insights might be a sufficiently general definition of “type theory” to which one can apply the theorem.
The “initiality hypothesis”? Since it kind of also fits well with the homotopy hypothesis, but working with homotopy theories.
I initially felt when ’homotopy hypothesis’ was mentioned by John B. and others, that it was not a hypothesis as I understood things, but now I think it is in the sense that it is a proposed explanation for observed phenomena, i.e. that a certain categorical or algebraic model behave as if it was a homotopy type or as a model for one (although the use in the literature often seemed to be at variance with that sense). Here it seems that the use of ’hypothesis’ may be a good one but I do not understand enough to comment further.
The situation for string diagrams is arguably even worse than that for type theory.
I thoroughly agree with this! Even standard references like Joyal-Street are not, for me at least, entirely satisfactory.
I considered “initiality hypothesis” but I don’t think the role of this statement in type theory is similar to the role of the hypotheses of higher category theory. The latter are (or, nowadays, were) sort of “guiding principles” or “tests for definitions”: if a definition of higher category didn’t make these true, then it was probably the wrong definition. Moreover, they were not precise mathematical statements. The initiality principle (for a given type theory) is a precise statement, and there are no definitions we’re debating that might affect its truth. (In contrast, I have proposed to use “internal language hypothesis” for the relation of type theories in general to higher categories, which involves not only initiality, but design of type theories, definitions of things like elementary higher categories, and strictification/coherence theorems).
Regarding string diagrams, I don’t know of any problem with Joyal-Street; the problem I was referring to is that people (myself included) use string diagrams in other contexts where no such theorems have been proven.
Re #25: indeed, I thought that was what you had in mind, was just taking it a step further. I do not know of any mathematical issue as such with Joyal-Street, I just think the distance between the formalisation and how one actually manipulates the diagrams in practise is too large, so I don’t personally find that it convinces me that things are rigorous more than my own internal sense that they are.
I suppose the catch in #16 is the word “general”. Otherwise, where is the gap in the usual categorical semantics?
As far as I know, the only dependent type theory for which anything approaching a complete proof of even weak initiality has actually been written down is the calculus of constructions, in Streicher’s book. Note that this does not include any inductive types, even Nat. I’m not sure what you mean by “the usual categorical semantics”, but it’s true that in various places one can find statements like this asserted without proof, or “proven” without due attention to issues such as substitution; maybe that’s what’s given a different impression?
I’m not sure what you mean by “the usual categorical semantics”
If you weren’t Mike Shulman, I would suggest to google for “categorical models of type theory”. But since you are, I don’t know what to make of this.
I am wondering if we see the formalization success becoming its own victim. What used to be perfectly rigorous arguments are now being questioned on the basis that they fail to formally prove that they have formally proven something. Let’s try to prevent the glorious vision of fully mechanized mathematics from thwarting intellectual progress in the meantime.
Urs, I’m talking about theorems, not definitions. Our page categorical model of dependent types, which is the second hit for that google (the first hit is my own lecture slides from 6 years ago, before I was aware of the problem being discussed here, and only a general overview anyway), is about the strict categorical structures that are expected to be the context in which to prove an initiality theorem. But we’re talking about whether those expected theorems have actually been proven. The page is definitely somewhat misleadingly named (maybe we should rename it? not sure what to, though), since it’s only the hoped-for initiality theorem that would actually show that these things are “models” of dependent type theory.
If you believe there is a “perfectly rigorous argument” out there, then please point precisely to where that argument is given. I’m saying there is no argument in the literature, and never has been — only a general belief that an argument could be given along similar lines to arguments that do exist in the literature.
Well, it’s good to get this out into the open. Perhaps we could just add a clarifying note to the introduction. There’s plenty of warning there about the difficulties, but there might be something more precise about how these have not yet been overcome rigorously.
I like the sound of the approach via ’canonicity at the empty type implies consistency’ (#20). This is relative consistency? We don’t want to be running into second incompleteness theorem territory.
What does Martin-Löf himself have to say about all this? Is it all in terms of the meaning explanation.
From a technical/mathematical point of view, the meaning explanations give rise to a realizability model of type theory, where realizers are terms in some untyped notion of computation, such as an extended lambda calculus…
Yes, certainly, any proof of consistency is relative to that of the metatheory. In the case of the canonicity approach, the proof of canonicity/normalization generally involves an inductive argument, which can require a “very long” well-founded relation to show that it terminates.
Hmm, so Huber writes in Canonicity for Cubical Type Theory:
…the consistency of the calculus already follows from its model in cubical sets…This note presents a first step in this direction by proving canonicity for natural numbers…Canonicity in this form also gives an alternative proof of the consistency of cubical type theory
Corollary 4.22 (Consistency). Cubical type theory is consistent, i.e., there is a type in the empty context which is not inhabited.
Is he claiming more than he should?
Ah, there is a comment on proof-theoretic strength:
To prove canonicity we devised computability predicates (and relations) which, from a set-theoretic perspective, are constructed using the least fixpoint of a suitable operator. It is unlikely that this result is optimal in terms of proof-theoretic strength; we conjecture that it is possible to modify the argument to only require the existence of a fixpoint of a suitably modified operator (and not necessarily its least fixpoint);
What does Martin-Löf himself have to say about all this?
I think the section ’Consistency’ in the these notes is the most relevant passage that I have seen. He argues that a semantic and not syntactic justification is appropriate, and gives such a justification. I think that mathematicians typically struggle with this, but I think that it has a lot of merit. Indeed, Mike and I had a long discussion a few years ago on the n-category café where I was somewhat critical of the fact that the univalence axiom does not have the same rigorous philosophical justification that plain MLTT has, which means that the semantics of HoTT are much more unclear than those of plain MLTT. In particular, it is harder to argue semantically for consistency.
In general, while of course I have great respect for Mike’s expertises in this area, I am sympathetic to Urs’ point of view here. I would make the following suggestions.
That we make an nLab page on the initiality conjecture, and try to explain precisely what needs to be shown and where the existing literature is lacking.
That it is not good for HoTT that what the initiality conjecture is even precisely about is understood by only a few insiders, which means that questions from outsiders can tend to be treated in a “You don’t have enough knowledge to understand the issues” kind of way, even if unintentionally, which must be frustrating and offputting for the outsiders.
As in #26, for me, I think it unlikely that a 300 page formal proof of initiality in ZFC would convince me that HoTT is consistent. Whilst Voevodsky was one of the mathematicians who influenced me most and whose profound creativity I deeply respect, I disagree slightly with one aspect of his work/views on type theoretic foundations: I think that one of his aims around the initiality conjecture was to convince ’ordinary’ mathematicians of the validity of HoTT, which means that he was especially concerned with ZFC; whereas I do not think there is any real reason to take ZFC as primary, and I also am not convinced that it will make much difference sociologically.
Where did I say anything like “You don’t have enough knowledge to understand the issues”? I thought we were all clear on exactly what the conjecture is about: the statement that the structured category-with-families (or whatever) built out of syntax is the initial such.
Of course there’s nothing special about ZFC, but most mathematics is not written in ZFC anyway; it’s basically foundation-agnostic, and the same would be true of a pencil-and-paper proof of initiality. A computer-formalized proof of initiality would probably itself be written in type theory, depending on the system in which it were formalized.
David C, was the person you were talking to actually worried about whether HoTT is consistent? I’ve never met anyone who actually doubted that it was. For me the real purpose of initiality is not to prove consistency, but to have a variety of categorical models.
Re #33, I’m not sure whether or not the cubical model depends on initiality. I haven’t studied this issue in-depth; I think there may be some models (like, for instance, the set-theoretic model of MLTT) that are “so close to the syntax” that they can be constructed “by hand” without appealing to a general initiality principle, and the cubical model of cubical type theory might fall under that heading. Unfortunately, some of what was originally written about the cubical model uses language in ways that are hard for a mathematician like me to understand, mixing syntax and semantics in confusing ways.
Indeed, models in presheaves of sets are much better understood than general models. So much so, that they are the first part of Mark Bickford’s Nuprl formalization of the cubical model. (Slides from 2016, paper from June, 2018.)
This formalization also settles most questions about proof-theoretic strength: intentional type theory with univalence is conservative over extensional type theory (with the same number of universes, closed under the same (non-higher) inductive families), which in turn by Martin Hofmann’s result is conservative over intensional type theory with UIP and function extensionality. The latter theory in turn has the same proof-theoretic strength as pure intensional type theory, which I think so far has only been established via ordinal analysis + well-ordering proof rather than interpretation (at least Hofmann’s paper on the setoid model doesn’t cover universes; maybe it’s been worked out since?).
Re #37:
Where did I say anything like “You don’t have enough knowledge to understand the issues”?
I think you have been very patient in your replies, and it is great that you take the time to respond to Urs and the others! It was just an observation about the feeling that I think may sometimes unintentionally come across when the precise issues involved in a problem that is sometimes portrayed as fundamental are known only inside a community.
I thought we were all clear on exactly what the conjecture is about
As in 1. of #36, my impression is precisely that people do not know what the conjecture is really about today, i.e. it is unclear to outsiders what the difficulties in establishing it are exactly, it is unclear to outsiders where exactly the literature is deficient, and it is unclear to outsiders whether there is even a consensus within the HoTT community about what would count as a proof. As I say, this is my impression, maybe others disagree.
Of course there’s nothing special about ZFC
Though it is only of historical interest, my impression, as I wrote, was that it was very important to Voevodsky that the consistency should be relative to ZFC, or at least material set theory.
The first sentence of 3. in #36 was not particular to ZFC, I think it is true that I would find a formal proof in itself mostly irrelevant regardless of which foundations it is written in. If new ideas were introduced in the course of the proof, these would be interesting of course.
Re #37,
…was the person you were talking to actually worried about whether HoTT is consistent?
That wasn’t my sense. It was more about whether HoTT had been shown to be consistent, and the further concern that people weren’t being as clear about what has been achieved as they ought to be.
Both #38, #39 are interesting, but the waters seem still a little muddy.
I am also quite frustrated with the situation. As Urs noted, even within the community there is not a consensus on how important this problem is, whether it is even a problem at all, where the real obstacles lie to solving it, and what would count as a solution. I expected, back when this issue began to be discussed seriously, that someone would just do the community service of writing down the missing proofs, and within a year or two we wouldn’t be talking about it any more. But although people are working on it, progress seems to be very slow. I am wondering whether I should put some effort into it myself. (I do have some ideas on how to go about it, but I haven’t put much time into it because I figured there were enough people working on it already.)
Would it be an idea to try to work it out on the nLab? I mean if it’s expected to be fairly trivial but tedious, maybe it would be helpful to have many people chip in. Time permitting, I would probably be willing to help, for example. Could start with a baby case but where some of the issues that are not treated in Streicher’s work are present.
there is not a consensus on how important this problem is, whether it is even a problem at all, where the real obstacles lie to solving it, and what would count as a solution.
Just think how much of even mainstream mathematics must have seemed like this around 1900. But you’d hope now that the expertise and resources of the FOM community could provide for honest score-keeping in a case such as this.
I wonder how much this would be a case of merely hacking through details, or whether it might generate important new ideas or constructions. I believe the consensus was already that CH was independent of ZFC in the early 60s, but we got forcing out of the effort to establish it.
If by the fom community if you mean this, then most of them won’t be much help, since I find most of the vocal people there are so strongly pro-material (and classical) that it’s hard to get across the cultural divide.
Re #45: still addicted to Hilbert’s boxers fists hm? (-:
Re #43: Hmm, maybe that could be a fun and useful exercise. It wouldn’t solve the real problem that we need a general version of the theorem, but working out one or more particular cases in detail, publically, would at least help more people understand what the issues and choices are — and if we manage to get to a “real world” particular case like MLTT or even some fragment of Book HoTT, then it would at least supply a better answer to questions like the one posed to David C that began this conversation. But we’d need a fair number of people participating to make the workload manageable for all of us (and the activity pleasant). Maybe I’ll open a new thread to get people’s attention and find out if anyone else would be interested.
Re #45, I know the FOM-list sank to pretty low depths, particularly at the time of the Friedman-McLarty exchanges, but I hear they have since had pleasant conversations on Colin’s work on FLT.
1 to 47 of 47