A Synthetic Approach to Higher Equalities

April 24, 2015

A Synthetic Approach to Higher Equalities

Posted by Mike Shulman

$MathML-enabled post (click for more details).$

At last, I have a complete draft of my chapter for Elaine Landry’s book Categories for the working philosopher. It’s currently titled

Homotopy Type Theory: A synthetic approach to higher equalities. pdf

As you can see (if you read it), not much is left of the one fragment of draft that I posted earlier; I decided to spend the available space on HoTT itself rather than detour into synthetic mathematics more generally. Although the conversations arising from that draft were still helpful, and my other recent ramblings did make it in.

Comments, questions, and suggestions would be very much appreciated! It’s due this Sunday (I got an extension from the original deadline), so there’s a very short window of time to make changes before I have to submit it. I expect I’ll be able to revise it again later in the process, though.

Posted at April 24, 2015 4:06 AM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2819

84 Comments & 0 Trackbacks

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

“.. Minkowski spacetimes, corresponding to special rather than general relativity.” To me this slightly suggest a way in which those two relate, which is simpler than it actually is.

Posted by: NikolajK on April 24, 2015 10:01 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Can you elaborate? Do you mean that I didn’t mention the Einstein equation? I didn’t consider it my job to explain relativity theory really.

Posted by: Mike Shulman on April 24, 2015 7:46 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

What I meant is that I don’t feel Minkowski spacetime(s) don’t correspond to general relativity.

Posted by: NikolajK on April 24, 2015 8:49 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Well, it’s true that Minkowski spacetime is one model of general relativity, but general relativity can’t be restricted to Minkowski spacetimes.

Posted by: Mike Shulman on April 24, 2015 8:50 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I really enjoyed this article. I have a general comment and then a few insignificant notes on the text that I will add as a separate comment. This is the general comment.

The fact that UF=MLTT+U+UA (by UF I will mean intensional MLTT with (at least one) univalent universe) serves as a synthetic theory of infinity groupoids is, of course, a fascinating and surprising fact. Also, as you say in p.4, I completely agree with you that a synthetic theory of a certain mathematical object (e.g. an $\infty$ -groupoid) can be considered a foundation for mathematics even if the same object is described analytically in some other system (e.g. as Kan simplicial sets in ZFC.) If anyone wants to argue against the foundational aspirations of UF on those grounds then the argument can be turned on its head, since by the same token one can argue that UF provides an analytic description of a set (e.g. as a $0$ -type in UF) and that therefore ZFC (or any other set theory) cannot be a foundation for exactly the same reasons. I have heard this argument used against UF before and I’ve deflected it in this manner – I think it’s a bad argument and I’m glad someone finally dealt with it in print.

However, what I think is somewhat glossed over in your account is the fact that when UF is viewed as a foundation of mathematics (in addition to a synthetic theory of $\infty$ -groupoids) it is no longer true that these two aspects interact in the way in which people are sometimes led to believe. For example, you write

Thus, any mathematics that can be encoded into set theory can also be encoded into HOTT/UF, while we additionally have the other $\infty$ -groupoids to use whenever that is more natural.

this seems to suggest more than what is actually true. To use an example that I have used before. Suppose I am interested in proving that the topological circle $S^1$ is not homeomorphic to the topological sphere $S^2$ . I then define $S^1$ and $S^2$ as HITs (call them “synthetic $S^1$ and $S^2$ ”) and then calculate their fundamental groups in the now well-known way. Have I thereby proved that topological $S^1$ is not homeomorphic to topological $S^2$ ? Inside UF, I have not. It is not as simple as that (as far as I’m aware there is still no cohesive HoTT-type shape modality inside UF that would allow you to do something like this.)

The simple point here is of course that it does not even make sense to consider synthetic $S^1$ and $S^2$ “up to homeomorphism”. The very statement “ $S^1$ is not homeomorphic to $S^2$ ” cannot be stated in UF-regarded-as-a-synthetic-theory-of- $\infty$ -groupoids. It must be stated with $S^1$ and $S^2$ defined topologically, i.e. as $h-$ sets with appropriate extra properties and structure. As nice as these synthetic calculations of homotopy groups are, I see a barrier in using them in the way that they are normally used, e.g. to draw inferences about spaces up to homeomorphism. And since a foundation of mathematics should be able to express any inference that one makes in mathematical practice, UF should be able to do that too. Of course it is able to do just that, namely at the level of $h$ -sets. But when doing it this way, the synthetic definitions of the circle and the sphere play essentially no role.

Which leaves the obvious worry: if in order to draw conclusions about spaces up to homeomorphism you then have to repeat every classical proof (e.g. $\pi_1 (S^1) = \mathbb{Z}$ ) at the level of $h$ -sets, then how much is the synthetic side of UF adding to UF-regarded-as-a-foundation? I personally wouldn’t mind if it added nothing: the fact that it is a synthetic theory of $\infty$ -groupoids is itself an incredibly powerful mathematical tool. But perhaps this pushes towards an argument that one ought to consider adding shape modalities as in cohesive HoTT in order to be able to strengthen the interaction between the synthetic and the “analytic” side as described above. I’ve written too much already but can elaborate on any of these points if they are unclear.

Posted by: Dimitris on April 24, 2015 4:47 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

when UF is viewed as a foundation of mathematics (in addition to a synthetic theory > of $\infty$ -groupoids) it is no longer true that these two aspects interact in the way > in which people are sometimes led to believe

I agree with this. I made a similar point during an earlier discussion with Mike, towards the end of this comment, where I wrote of a ‘meta-type-mismatch’.

I also agree that the phrasing of the last paragraph is a little confusing at present. When I first read it, it sounded as though Mike was asserting that the fact that

HoTT/UF unifies the Erlangen and structuralist approaches to geometry

the central message of HoTT/UF

which would be a rather bizarre statement! I assume that Mike is rather referring to what comes after the colon.

On that point, I don’t actually see this ‘central message’ as suggested specifically by HoTT/UF. One could surely argue that ‘paying attention to identifications’ was at the heart of intensional Martin-Löf type theory from the beginning, before groupoid and higher groupoid semantics were suggested. An appreciation of the distinction between extensional and intensional notions of ‘equality’ goes back at least to Frege, and is a fundamental consideration in the semantics of natural languages.

Whilst higher inductive types are a post-HoTT idea, ‘paying attention to identifications when specifying new gadgets’ is surely necessary and indeed at the heart of any mathematics that is of a category theoretic (or higher category theoretic) nature, and there are of course foundations for mathematics of a category theoretic nature other than HoTT/UF.

Regarding HoTT/UF as a foundations, I may be in a minority of one, but I myself am not at all convinced by the univalence axiom, and always avoid it. I find Martin-Löf type theory very beautiful and natural as a foundations, and I find it it very beautiful that it admits a higher categorical/homotopical semantics. But the univalence axiom just seems like a hack to me.

This brings me to remark on the second paragraph in Dimitris’ comment. I agree entirely, of course, that synthetic theories of gadgets other than sets can be valid foundations for mathematics, and that the ability to work with those gadgets in a set theoretic foundations is irrelevant to this. I myself always work in a foundations of a category theoretic nature. But I would argue that a foundations for mathematics should be justified very carefully semantically. One of the beautiful things about Martin-Löf type theory is that Martin-Löf did exactly this.

In other words, I would argue that one cannot take any old synthetic theory and regard it as a foundations for mathematics. One should be able explain the meaning of the syntax of one’s foundations in a simple and clear way which does not require any degree of mathematical sophistication: one should be able justify it philosophically, one might say. This is one reason for my point of view on the univalence axiom: I have not seen any true justification of it, only arguments that are more or less appeals to convenience.

Posted by: Richard Williamson on April 24, 2015 7:19 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I assume that Mike is rather referring to what comes after the colon.

Ah, yes, I should reword that to clarify. Thanks!

On that point, I don’t actually see this ‘central message’ as suggested specifically by HoTT/UF. One could surely argue that ‘paying attention to identifications’ was at the heart of intensional Martin-Löf type theory from the beginning,

You omitted the crucial part of what I wrote:

whenever we define a collection of objects we must also pay attention to the identifications and higher identifications between them [emphasis added]

Perhaps I should add this emphasis to the paper itself.

Posted by: Mike Shulman on April 24, 2015 7:54 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Yes, I did so deliberately. My point was that many aspects of the ‘central message of HoTT/UF’ are not specific to it: all of it could be said of any categorical/higher categorical foundations, and at least some of it could be said of ordinary intensional Martin-Löf type theory.

I of course agree that a greater understanding of the ‘higher identifications’ that are ‘implicit’ in a type in Martin-Löf type theory has been reached since the semantical developments which begin with the groupoid model of Hofman and Streicher. But I think there is a possibility of conflating these semantical insights with foundational points that are of independent significance.

I would put things as follows.

1) It is a fundamental principle/message of category theory and higher category theory that one should pay attention to identifications and higher identifications.

2) It is a fundamental principle/message of intensional Martin-Löf type theory that one should pay attention to identifications. This implicitly includes paying attention to higher identifications.

3) It turns out, beautifully, that these two fundamental principles are related, in that higher category theory provides a semantics for intensional Martin-Löf type theory. This relation helps to show that we are implicitly paying attention to higher identifications in the latter.

So you see that I would argue that the two ‘central messages’ have nothing really to do with HoTT/UT, the latter is rather to do with the relationship between them.

Posted by: Richard Williamson on April 25, 2015 8:55 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Ah, I guess that my phrase “pay attention to” was confusing. What I meant was that the central message is that we should ensure that the identifications and higher identifications are correct. MLTT may tell us to “pay attention to” identifications in the sense of “noticing them”, but it lacks the tools (such as univalence and HITs) to ensure that those identifications are correct. Any other higher-categorical foundation for mathematics would indeed probably have similar tools, but I don’t know of any other higher-categorical foundation for mathematics.

Posted by: Mike Shulman on April 25, 2015 5:42 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

But I would argue that a foundations for mathematics should be justified very carefully semantically. […] One should be able explain the meaning of the syntax of one’s foundations in a simple and clear way which does not require any degree of mathematical sophistication: one should be able justify it philosophically, one might say.

I agree with the idea that “clarity of intended semantics” should be something that any foundations should aim for. I’m not sure if I’d agree that such clarity needs to be at the level where you could explain this intended semantics to people without “any degree of mathematical sophistication”. That would probably be too strong. We are spoiled in this regard by set theory because we feel that a set is such a simple concept that one could explain what it is even to a child. But that, in my mind, doesn’t prove that sets are objectively a clearer concept than $\infty$ -groupoids. What it proves, if anything, is that we have developed such a large network of discourse/explanations/examples around set theory so as to make its basic concepts appear like trivialities. But who is to say that a similar network will not eventually arise around $\infty$ -groupoids? And then, perhaps, the intended semantics of UF will appear to us just as philosophically perspicuous as those of MLTT or ZFC.

In tackling this issue Mike points out (bottom of p.4) something quite similar, i.e. that we should not be led astray by the primacy of our current intuitions in judging the fundamentality of a particular theory. I agree with this, though perhaps clarity doesn’t necessarily follow from fundamentality.

But important as Mike’s point may be it is likely that such a viewpoint may also leads us astray. As Mike himself suggests, pretty much any concept becomes intuitive after one acquires enough experience with it. But that surely doesn’t mean that every concept is (potentially) equally clear. (e.g. I would say that $\infty$ -groupoids are much clearer a concept than $\infty$ -categories from a purely intuitive standpoint.) I’m not sure if this is implied by the article, but I certainly think that the philosophical justification of UF should not stop at declaring “You have your own intuitions, we have our own, and time will tell that ours are just as robust as yours.” There is more to be said about the intuitive meaning of homotopy types as abstract shapes.

This is one reason for my point of view on the univalence axiom: I have not seen any true justification of it, only arguments that are more or less appeals to convenience.

What about the (variation of) the Leibniz principle: indiscernible objects are indistinguishable. You can see univalence as encoding this kind of principle. Is that not sufficient philosophical justification?

Posted by: Dimitris on April 24, 2015 8:14 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

What about the (variation of) the Leibniz principle: indiscernible objects are indistinguishable. You can see univalence as encoding this kind of principle. Is that not sufficient philosophical justification?

For me, the identity types in intensional Martin-Löf type theory already capture this principle.

The way that I see the univalence axiom is as follows.

1) We have a beautiful foundational system, namely intensional Martin-Löf type theory.

2) We make the beautiful observation that it has a homotopical/higher categorical semantics.

3) We would like a foundations that is based on homotopy theory or categories/higher categories/groupoids/higher groupoids, in which homotopy equivalence/equivalence of categories is the fundamental notion of sameness.

HoTT/UT is based on achieving 3) by hacking 1), informed by the semantical understanding from 2), to force this to be the case.

I really do think that the word ‘hack’ is appropriate here. We do not in any way attempt to think about what a higher categorical foundations should be in itself; we do not attempt to begin with categories, functors, etc, as primitive concepts, and build a foundations upon that. We just take an existing foundations (Martin-Löf type theory), ignore its semantical justification as a foundations, observe that it can be thought of to a certain extent as corresponding to homotopy theory, and force an axiom to hold which makes that correspondence closer.

We have no precise understanding of the primitive gadgets in the foundations: we have lost the original semantical justification of Martin-Löf, and we cannot claim that these primitive gadgets really are synthetic weak $\infty$ -groupoids. If that were the case, we would able to write down an a priori foundations built upon weak $\infty$ -groupoids, not one obtained by hacking an existing one. All we can claim is that the primitive gadgets are closer to being weak $\infty$ -groupoids according to one interpretation of them (i.e. semantics for them).

we feel that a set is such a simple concept that one could explain what it is even to a child. But that, in my mind, doesn’t prove that sets are objectively a clearer concept than ∞-groupoids. What it proves, if anything, is that we have developed such a large network of discourse/explanations/examples around set theory so as to make its basic concepts appear like trivialities. But who is to say that a similar network will not eventually arise around ∞-groupoids? And then, perhaps, the intended semantics of UF will appear to us just as philosophically perspicuous as those of MLTT or ZFC.

I agree with much of what you write. In particular, I certainly do not claim that the notion of a set is objectively clearer than that of an $\infty$ -groupoid, or that sets have any special status with regard to simplicity or clarity when it comes to foundations.

Indeed, a category is in my opinion just as clear a primitive notion as that of a set, and I feel that one could explain it just as well to a child as one could a set.

I would say that ∞-groupoids are much clearer a concept than ∞-categories from a purely intuitive standpoint.

I certainly do not agree! I think that you are assuming the homotopy hypothesis here, and thinking of weak $\infty$ -groupoids as homotopy types, which you feel you have intuition for.

Posted by: Richard Williamson on April 25, 2015 10:04 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

We do not in any way attempt to think about what a higher categorical foundations should be in itself; we do not attempt to begin with categories, functors, etc, as primitive concepts, and build a foundations upon that. We just take an existing foundations (Martin-Löf type theory), ignore its semantical justification as a foundations, observe that it can be thought of to a certain extent as corresponding to homotopy theory, and force an axiom to hold which makes that correspondence closer.

I see your point, but I think the history is more complicated than that. Voevodsky for example was certainly thinking of categorical foundations independently of MLTT in the beginning. I don’t know if this is widely known but he is pretty explicit in stating that he was very much influenced by Makkai’s work on FOLDS - at least initially. And Makkai was certainly someone who was thinking of categorical foundations independently of any pre-existing formal system like MLTT. Makkai’s (unfinished) foundations based on FOLDS were motivated by “purely metaphysical” considerations about what an $\infty$ -category would be like as an “intended semantics” to replace e.g. the cumulative hierarchy of sets. It was not motivated by the discovery of that a pre-existing formal system could have a new kind of semantics. And univalence is a syntactic enforcement of exactly the kind of principle that Makkai (for philosophical reasons) thought that a categorical foundation of mathematics should satisfy.

Two further quick points on this:

(1) I see HoTT/UF as motivated by an altogether different “problematic” than traditional foundations like set theory. Finding philosophically perspicuous semantics (though nice if it can happen) is not, as I see it, an issue on which HoTT/UF stands or falls. This is because the driving force behind HoTT/UF as a foundation is not necessarily for it to become the “ultimate” foundation e.g. like ZFC. The driving force, rather, is to provide foundations formalizable in a proof assistant so that the use of proof-assistants can actually become a tool for working mathematicians. From this perspective it is clearly preferable to rely on a formal system that was tailor-made to be implemented in computers. And for exactly the same reasons the original intended semantics of this system become less of a constraint when putting this pre-existing formal system to new use.

(2) The idea of a dependent type is so general as to transcend its formalization in MLTT-style systems even though this is where it was first formalized. It is really the notion of a dependent type as encoding syntactically the fact that in “higher” mathematical structures (e.g. $n$ -categories) the declaration of (names for) higher arrows depends on the previous declaration of (names for) lower arrows. It is essentially this feature that identity types possess that allows them to be interpreted as $\infty$ -groupoids and the fact that identity types in intensional MLTT possesed this feature independently of its original intended semantics does not mean, in my opinion, that employing this feature constitutes a hack of MLTT. Similarly, do you really want to say that ZFC is a hack of the predicate calculus of Frege?

We have no precise understanding of the primitive gadgets in the foundations: we have lost the original semantical justification of Martin-Löf, and we cannot claim that these primitive gadgets really are synthetic weak $\infty$ -groupoids.

My understanding is that no-one really understood the structure of identity types in intensional MLTT and all the higher structure was regarded as something of a curiosity. Indeed I believe that it was for some time an active open question whether axiom K was actually provable in MLTT. So HoTT/UF can equally well be understood as providing the missing explanation of the higher structure of identity types and as such providing the missing justification for the syntax of identity types in intensional MLTT.

If that were the case, we would able to write down an a priori foundations built upon weak ∞-groupoids, not one obtained by hacking an existing one. All we can claim is that the primitive gadgets are closer to being weak ∞-groupoids according to one interpretation of them (i.e. semantics for them).

I guess what you mean is that there ought to be a completely new formal calculus (i.e. not MLTT) constructed with $\infty$ -groupoids as its intended semantics?

Posted by: Dimitris on April 27, 2015 1:28 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Finding philosophically perspicuous semantics (though nice if it can happen) is not, as I see it, an issue on which HoTT/UF stands or falls.

Nor, in my opinion, is it an issue on which any foundation for mathematics stands or falls. Foundations for mathematics should be evaluated on their value to mathematics. If philosophers don’t like the semantics, that’s a problem for them to solve (perhaps by learning to like the semantics), not a reason for mathematicians to reject the theory.

This is because the driving force behind HoTT/UF as a foundation is not necessarily for it to become the “ultimate” foundation e.g. like ZFC. The driving force, rather, is to provide foundations formalizable in a proof assistant so that the use of proof-assistants can actually become a tool for working mathematicians.

I don’t think it is correct to claim that there is any single “driving force” behind HoTT/UF. The HoTT/UF community is diverse and people have many different goals. Voevodsky does seem to be motivated primarily to widen the use of proof assistants. Personally, while I think proof assistants are great, I also think they have many obstacles to overcome before they can become a tool for the average working mathematician, most of those obstacles are engineering problems rather than mathematical ones, and HoTT/UF is really only a relatively small step along that road. I am at least as powerfully motivated by HoTT/UF’s potential as a foundation for all of mathematics and also as an internal language for $(\infty,1)$ -categories. Other people may have other motivations.

the fact that identity types in intensional MLTT possesed this feature independently of its original intended semantics does not mean, in my opinion, that employing this feature constitutes a hack of MLTT. Similarly, do you really want to say that ZFC is a hack of the predicate calculus of Frege?

Nicely put!

Posted by: Mike Shulman on April 27, 2015 5:00 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Nor, in my opinion, is it an issue on which any foundation for mathematics stands or falls. Foundations for mathematics should be evaluated on their value to mathematics. If philosophers don’t like the semantics, that’s a problem for them to solve (perhaps by learning to like the semantics), not a reason for mathematicians to reject the theory.

It is certainly the case that mathematics is a human activity, beyond any particular foundations. It is remarkable that many mathematicians misunderstand the purpose of a formal foundations to such an extent that they will vehemently defend the point of view that mathematics is defined by ZFC!

But, in my view, what you have written goes too far the other way. One can, as Dimitris wrote, of course have a synthetic theory that one does not regard as an ‘ultimate foundations’. But I think that one has to accept that one’s foundations should be meaningful to at least a certain degree. One’s formalisation of a natural number should capture, in some sense, the way in which we understand the notion, one human to another. Now the ‘meaning’ of one’s synthetic theory can come from a formalisation in a second, more primitive, theory. But one has to stop somewhere: one has to somewhere reach a point where we can agree, one human to another, that we understand each other, and where this understanding comes from ‘beyond mathematics itself’.

Where we choose to stop, and what we wish to appeal to ‘beyond mathematics’, will vary from person to person. We may even differ in our opinions on the nature and meaning of mathematics, for instance between a constructive semantics as in Martin-Löf type theory, or a Platonic conception that allows non-constructive principles. But some meaning, i.e., some semantics, has to be offered somewhere along the line.

Posted by: Richard Williamson on April 28, 2015 2:02 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I didn’t say that it was okay to have no semantics; I said that mathematicians shouldn’t reject a theory because philosophers don’t like the semantics.

Posted by: Mike Shulman on April 30, 2015 12:40 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Well, you wrote that (my italics):

[Finding philosophically perspicuous semantics (though nice if it can happen) is not] an issue on which any foundation for mathematics stands or falls.

What I suggested, and which you seem to be agree with, is that it is necessary to have a clear semantics, beyond mathematics itself, somewhere along the line, i.e., for some foundations. In other words, a foundations which is intended to be ‘fundamental’ in this sense will stand or fall on this matter.

The question of such a semantics is not, for me, an abstruse matter which philosophers can form opinions about, but which is irrelevant to mathematics itself, i.e. the kind of matter that you are dismissing the value of philosophical reflection upon. I would argue that it is fundamental to mathematics as an activity that it should be meaningful, and thus that we have a clear semantics from beyond itself at some point. One might call the consideration of this kind of semantics ‘philosophy’, or one might not, but the semantics must come from beyond mathematics itself, and ‘philosophical justification’ seems as a good a choice of phrase as any other to me.

Posted by: Richard Williamson on April 30, 2015 9:20 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I don’t think it is correct to claim that there is any single “driving force” behind HoTT/UF. The HoTT/UF community is diverse and people have many different goals. Voevodsky does seem to be motivated primarily to widen the use of proof assistants.

Since what I said was used in the post on the “Mathematics without Apologies” blog and somehow from there I was led back to here and realized I had missed this response, let me just clarify (as I did there) that I did not mean to suggest at all that there is a single driving force behind UF (or that there ought to be). Though my phrasing is sloppy I was merely making the point to Richard that there are other reasons to pick MLTT+UA independent of thinking about the nature of $\infty$ -groupoids. Its relation to proof assistants is such a reason and UA arose (historically) with that kind of reason in mind. What came after is far wider in scope and exactly how HoTT/UF is being put to use now is of course not limited at all to building better proof-assistants. I never meant to suggest that.

Posted by: Dimitris on May 1, 2015 3:03 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Yes, I was aware of the influence of Makkai’s work on Voevodsky. Certainly categorical foundations have been explored before. But, whether univalence may be a desirable principle, or whether it may be expressible in some other syntactics whose intended semantics is that of weak $\infty$ -groupoids or homotopy types, is, in my view, not relevant to the point I am making.

I would guess that, ultimately, where my view principally differs from that of you and Mike is that I do not regard the syntactics of intensional Martin-Löf type theory as expressing directly and naturally what a weak $\infty$ -groupoid or homotopy type is, or what a (higher) category of such gadgets should be. If one agrees with this, then one has to, in my view, regard the univalence axiom as a hack.

Maybe I have not emphasised sufficiently so far that I am not at all convinced that HoTT/UF does exactly capture weak $\infty$ -groupoids or homotopy types, exactly because of the a posteriori modifying of syntactics according to semantical observations. Certainly HoTT/UF captures something of the nature of weak $\infty$ -groupoids or homotopy types, but who knows exactly what it captures? I would much rather work with a foundations in which we are absolutely clear about how we do wish to think of weak $\infty$ -groupoids or homotopy types and express this in the syntactics: we may later need to build further upon or modify our syntactics, but at least we know precisely how we are thinking of our notion of weak $\infty$ -groupoid or homotopy type is at any given time. Of course this is to a certain extent a matter of taste, but I feel that the difference between the two points of view is worth drawing attention to.

I guess what you mean is that there ought to be a completely new formal calculus (i.e. not MLTT) constructed with ∞-groupoids as its intended semantics?

Exactly, except that I see no reason that it could not be an extension of Martin-Löf type theory. I have been working on such a foundations (for ordinary categories) myself.

Finding philosophically perspicuous semantics (though nice if it can happen) is not, as I see it, an issue on which HoTT/UF stands or falls. This is because the driving force behind HoTT/UF as a foundation is not necessarily for it to become the “ultimate” foundation e.g. like ZFC.

I entirely agree. But if one adopts the point of view that HoTT/UT is just another kind of synthetic mathematics, like synthetic differential geometry, then one should I think be very clear about this. In particular, one should not attempt to claim that intensional Martin-Löf type theory is somehow impractical or deficient as a foundations for mathematics, and that HoTT/UF magically ‘fixes it’ or ‘improves it’. In addition, as above, one should be wary of asserting that one exactly captures homotopy types or weak $\infty$ -groupoids.

The driving force, rather, is to provide foundations formalizable in a proof assistant so that the use of proof-assistants can actually become a tool for working mathematicians. From this perspective it is clearly preferable to rely on a formal system that was tailor-made to be implemented in computers. And for exactly the same reasons the original intended semantics of this system become less of a constraint when putting this pre-existing formal system to new use.

I have no absolutely no problem with putting a pre-existing formal system to use, irrespective of the original semantics of that formal system. But one could try to find a way to build on the formal system in which we directly posit a type of (higher) categories/groupoids as a separate primitive notion (i.e. just posit Cat : Type as an axiom and posit rules which govern how we work with it), rather than taking one’s ‘type of homotopy types/weak $\infty$ -groupoids’ to be a pre-existing type, as in HoTT/UF.

the fact that identity types in intensional MLTT possesed this feature independently of its original intended semantics does not mean, in my opinion, that employing this feature constitutes a hack of MLTT.

I do not think that you have accurately represented what it is that I consider to be a hack. That identity types in Martin-Löf type theory can be viewed as weak $\infty$ -groupoids is beautiful. It is the a posteori attempt to turn this around and claim that, after univalence, Martin-Löf type theory magically becomes a synthetic theory of weak $\infty$ -groupoids that I am criticising.

Similarly, do you really want to say that ZFC is a hack of the predicate calculus of Frege?

Whilst I would happily claim that ZFC is a hack, I do not see any close analogy to the point I have been making!

Posted by: Richard Williamson on April 28, 2015 12:56 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

But one could try to find a way to build on the formal system in which we directly posit a type of (higher) categories/groupoids as a separate primitive notion (i.e. just posit Cat : Type as an axiom and posit rules which govern how we work with it), rather than taking one’s ‘type of homotopy types/weak ∞-groupoids’ to be a pre-existing type, as in HoTT/UF.

So if I understand correctly, you’re saying it would be acceptable to posit $\infty-Grpd : Type$ along with rules governing it, but you object to taking $\infty-Grpd \equiv Type: Type$ .

But I’m sure you’d agree that if we write down the rules governing $\infty-Grpd: Type$ , and realize that they’re the same rules as those governing $Type:Type$ , then it would be acceptable to take $\infty-Grpd \equiv Type$ .

So I’m curious: how should the rules governing $\infty-Grpd: Type$ differ from the rules governing $Type:Type$ ?

Posted by: Tim Campion on April 28, 2015 3:01 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

So if I understand correctly, you’re saying it would be acceptable to posit $\infty−\mathsf{Grpd}:\mathsf{Type}$ along with rules governing it, but you object to taking $\infty−\mathsf{Grpd}\equiv \mathsf{Type}:\mathsf{Type}$ .

Yes, that is correct.

But I’m sure you’d agree that if we write down the rules governing $\infty−\mathsf{Grpd}:\mathsf{Type}$ , and realize that they’re the same rules as those governing $\mathsf{Type}:\mathsf{Type}$ , then it would be acceptable to take $\infty−\mathsf{Grpd} \equiv \mathsf{Type}$ .

Yes, I would agree with that.

So I’m curious: how should the rules governing $\infty−\mathsf{Grpd}:\mathsf{Type}$ differ from the rules governing $\mathsf{Type}:\mathsf{Type}$ ?

There are several possibilities. One I’m particularly interested in (in the case of ordinary categories) is to encode in the syntactics various aspects of the 2-category of categories (or strict 2-categories, but I’ll stick to categories here for simplicity). We will certainly have $A : \mathsf{Cat}, B : \mathsf{Cat} \vdash \mathsf{Functor}(A,B):\mathsf{Type}$ as well, and probably a type of natural transformations too (one could define it, of course, as a special kind of functor type too, as long as we encode products).

I would like to speak of objects and arrows of a category. So I will posit a term $1_Cat : Cat$ , and think of an object of $A : \mathsf{Cat}$ as a term of type $\mathsf{Functor}(1_\mathsf{Cat},A)$ . Similarly for arrows.

One then posits by hand the existence of certain limits and colimits, and 2-limits and 2-colimits. One has certain rules which allow one to construct terms of identity types on ‘arrows’: this is how commutative diagrams are encoded. The main thrust of my work on this kind of foundations has been to capture various fundamental categorical constructions (free constructions: free categories, free strict monoidal categories, free co-completion, …) in such a foundations. One needs in fact remarkably little in one’s foundations, but I make a lot of use of simple 2-colimits and 2-limits.

To deal with different sizes of categories is no problem. One way I like to approach this is to have both a ‘sized’ notion of category’ (in Coq, it is convenient to define this via an inductive type: small categories, large categories, very large categories, etc), and an ‘unsized’ notion of category. In this way, one can encode ‘size polymorphism’ without any tedious repetition.

Hopefully this is already enough for you to see that the syntactics in this kind of approach are of a completely different nature to those of HoTT/UF.

Posted by: Richard Williamson on April 28, 2015 7:50 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

A modern, type theory - based, synthetic theory of categories sounds very interesting. But it doesn’t directly answer my question “What should a synthetic, type-theoretic theory of $\infty$ -groupoids look like if not like HoTT?”.

From what you’ve said, it sounds to me like you’d prefer a synthetic, type-theoretic theory of $\infty$ -categories, with which one could reason about $\infty$ -groupoids as a special case (Is that accurate?). And such a theory would look very different, no doubt.

But I think we established that you object to HoTT as a synthetic theory of $\infty$ -groupoids. So far I don’t understand what you think HoTT gets wrong about $\infty$ -groupoids. Is there a theorem of HoTT which is not true of $\infty$ -groupoids? Are there theorems about $\infty$ -groupoids that you should be able to prove but you can’t in HoTT? I think you agreed that if a theory like HoTT proves the right theorems, then it is a satisfactory synthetic theory of $\infty$ -groupoids.

Posted by: Tim Campion on April 28, 2015 9:13 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

it doesn’t directly answer my question “What should a synthetic, type-theoretic theory of ∞-groupoids look like if not like HoTT?”

What I intended was to give a flavour of the kind of approach that could be taken to such a theory. In principle, the approach that I outlined could be followed in the case of $\infty$ -groupoids too.

However, I’m not convinced that we are in any position as yet to try to find a synthetic theory of weak $\infty$ -groupoids akin the one I sketched for categories. I had refrained from mentioning this until now in order to try to keep the discussion focused. But I think that people are too blasé about the homotopy hypothesis. Once we have a good algebraic understanding of weak $\infty$ -groupoids, we may be able to begin to abstract from this to a synthetic theory of the kind I mentioned for categories.

Moreover, I have some ontological doubts about the notion of a weak $\infty$ -groupoid. By this, I mean that I am not yet convinced that weak $\infty$ -groupoids, as usually conceived, really exist in any substantial sense, and in particular whether this usual conception is appropriate to base a foundations upon. I certainly think that there is an algebraic notion of weak $\infty$ -groupoid which satisfies the homotopy hypothesis: in the nForum, I am working on demonstrating exactly this claim. But this notion will be understood, ontologically speaking, through category theory: there will be a 2-category of such gadgets, and category theory will be used to construct them. Eventually, we may be able to understand the ontology of $\infty$ -categories and groupoids. But this, in my opinion, is a long way off: I would say that we only really understand very well the ontology of categories; understand quite well the ontology of 2-categories; and understand slightly the ontology of 3-categories. Beyond this, nothing.

I appreciate that ‘ontology’ is an unusual word to use in this context, but it is the only word I can think of that approaches what I am getting at: we don’t really know what to do with 4-categories, we don’t have a ‘feeling’ for them, etc. This is, in my opinion, related to size issues! If we begin with small categories, everybody would agree that large categories are fundamental to category theory. But sometimes, especially in a 2-categorical setting, we wish to work with the category of large categories. So very large categories are useful. But I don’t know any work which makes use of very, very large categories in a significant way. I expect that if we had some good use to put the very large 2-category of large categories in a 3-categorical setting, then very, very large categories would become useful.

All of this is to explain why I restricted to ordinary categories: in principle a similar sort of thing could be done for $\infty$ -groupoids, but it seems to me that we are a very long way off understanding the latter deeply enough.

But, all that said, there are other possible approaches to a synthetic $\infty$ -groupoids than the one I described. One could try to syntactically capture one of the algebraic notions of $\infty$ -groupoid, rather than capture a category (or 2-category, etc) of such gadgets. For instance, the Ara-Grothendieck-Maltsiniotis notion. Whilst I haven’t worked on implementing this in type theory, it should seem to me plausible that one might be able to ‘remove’ the category theory which is used to define the notion of a coherator, etc, and implement the idea directly syntactically. But the rules would again look very different to those in HoTT.

I don’t think I would call such a theory a synthetic theory of weak $\infty$ -groupoids, though: it would just be a theory of weak $\infty$ -groupoids. This is the same distinction as, say, defining categories in Martin-Löf type theory versus defining a kind of ‘2-category of categories’ in Martin-Löf type theory.

From what you’ve said, it sounds to me like you’d prefer a synthetic, type-theoretic theory of ∞-categories, with which one could reason about ∞-groupoids as a special case (Is that accurate?).

Not quite. Such a synthetic theory of $\infty$ -categories would be great, but there is nothing wrong with a direct synthetic theory of $\infty$ -groupoids. What I do mean to emphasise, though, is that if we think of weak $\infty$ -groupoids algebraically, then I do not expect a synthetic theory of weak $\infty$ -groupoids to be any easier than a synthetic theory of weak $\infty$ -categories. Of course, if one is just using weak $\infty$ -groupoid as a synonym for homotopy type, then this point is not relevant, but I always think of a weak $\infty$ -groupoid as a structural (algebraic/categorical/…) notion.

I think you agreed that if a theory like HoTT proves the right theorems, then it is a satisfactory synthetic theory of ∞-groupoids.

No, I do not agree with this! My point is many ways the opposite. I am arguing:

1) that we do not understand weak $\infty$ -groupoids well enough yet for any claim that we have a synthetic theory of them to be much more than vacuous (true more or less by definition);

2) that the justification that you have written in this quote is not enough for a good synthetic theory, we should rather be able to understand the primitive gadgets in the synthetic theory in a good, direct, and natural way as weak $\infty$ -groupoids (or as homotopy types). This is the case, for instance, for synthetic differential geometry: the axiomatics correspond directly and naturally to the aspects of differential geometry that we wish to have a synthetic theory of.

If our only criterion is ‘proving the right theorems’, and we do not truly understand the primitive notions, our foundations will not, in my opinion, be very robust. There is always the possibility that some flaw, or some hole, will be revealed. If our primitive notions are built with the intended semantics in mind, this is not possible (of course, our semantical needs may change over time, but that is a different matter, and the case for any foundations).

But I think we established that you object to HoTT as a synthetic theory of ∞-groupoids.

Yes (and as a synthetic theory of homotopy types). Specifically, I object to the claim that the a posteriori ‘forcing’ of the univalence axiom (or related things) magically gives us such a synthetic theory.

Is there a theorem of HoTT which is not true of ∞-groupoids? Are there theorems about ∞-groupoids that you should be able to prove but you can’t in HoTT?

Hopefully what I have written above explains that I do not consider these questions to be the correct ones to ask to understand my point.

Whilst I do not work in HoTT for the reasons I have given, and do not have much acquaintance with exactly what has or has not been proven, beyond what I see/hear in passing, I would expect the answer to your second question to definitely be ‘yes’, eventually. I would also expect the answer to your first question to be ‘yes’, but not of course if we take $\infty$ -groupoid to mean a type in HoTT, because then the answer is certainly affirmative, so long as we have soundness.

So far I don’t understand what you think HoTT gets wrong about ∞-groupoids.

From what I’ve written above, hopefully it is now clearer that what I am arguing is that it is not at all clear that HoTT is a synthetic theory of $\infty$ -groupoids at all! It is a synthetic theory of something (we do not know what), which in one semantics matches up with some aspects of homotopy theory, and thus, if one assumes the homotopy hypothesis, etc, with some aspects of the theory of $\infty$ -groupoids.

Posted by: Richard Williamson on April 29, 2015 2:29 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

So we’re agreed that there are at least two possible approaches to a synthetic theory of $\infty$ -groupoids: a 2-categorical approach, or an approach based on an algebraic theory of $\infty$ -categories.

You claim that HoTT is very different from what you’d get following the second approach. Let’s unpack that. Unless I misunderstand, in the second approach, you would posit all the various n-cell types and n-cell compositions and coherences as individual constructors. You’d have two $\infty$ -groupoid structures on your type: the one you posited, and the one coming from the identity types. Presumably you’d say something about how these two interact. Isn’t it much simpler to simply use the $\infty$ -groupoid structure of the identity types as your object of interest? Are you worried that there might be $\infty$ -groupoids which can’t arise from identity types?
You said

that we do not understand weak ∞-groupoids well enough yet for any claim that we have a synthetic theory of them to be much more than vacuous (true more or less by definition)

I don’t understand this. It seems to me that we know the “intended model” of any theory of $\infty$ -grouoids; in fact there are many equivalent descriptions of it, e.g. Kan complexes. Since MLTT+univalence has the intended model as a model, it seems to me that MLTT+univalence is therefore a theory $\infty$ -groupoids. So you must be saying that, yes, it’s a theory of $\infty$ -groupoids, but it’s not synthetic. Presumably this is because it doesn’t have the right primitive notions? But this brings us back to the first point: we have a few very natural options for which primitive notions to use, HoTT picks one and builds a sound theory around it. What’s the problem?

Posted by: Tim Campion on April 29, 2015 4:36 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Richard, are you familiar with the “cubical type theory” that Coquand et. al. and Brunerie–Licata are developing? It seems like it might be more along the lines of what you’re looking for.

Posted by: Mike Shulman on April 29, 2015 6:19 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I am very interested in it. and there are some things around it that I would very much like to work on. Alas, I am less familiar with it than I would like at the moment, for lack of opportunity to look into it, and I’m not sure when the opportunity will arise!

I definitely agree that it seems much closer, from what I have seen of it, to fitting into the paradigm I am advocating.

Posted by: Richard Williamson on April 29, 2015 8:12 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I don’t really know anything about this approach. What are the relevant differences? Is this supposed to be an approach which captures algebraic $\infty$ -groupoids syntactically, or does it axiomatize the category of $\infty$ -groupoids?

HoTT is supposed to be a syntactic approach – we have 0-cells (terms), 1-cells (terms of identity types), and so forth. Is your objection that the various compositions and coherence cells are not posited as primitive notions, but rather derived in an opaque manner from path induction? Is the issue that the access we have to them is not sufficiently explicit and “combinatorial”?

Posted by: Tim Campion on April 29, 2015 10:47 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I am somewhat reluctant to comment because I have not looked into it in detail, so my impressions could be incorrect.

But my impression is that the syntax of cubical type theory expresses the notion of a cubical Kan complex (in the modified sense which is used in the model of Bezem, Coquand, and Huber), and related things, directly. So we are not modelling MLTT any more, we are directly capturing syntactically those aspects of the models of MLTT that are significant.

Is this supposed to be an approach which captures algebraic ∞-groupoids syntactically, or does it axiomatize the category of ∞-groupoids?

As can be concluded from what I’ve written above: neither, really. When I wrote that it fits into the paradigm that I am advocating, I was referring to the specifying the meaning of primitive notions directly, rather than applying an a posteriori ‘forcing’.

Is your objection that the various compositions and coherence cells are not posited as primitive notions, but rather derived in an opaque manner from path induction? Is the issue that the access we have to them is not sufficiently explicit and “combinatorial”?

This is definitely an important part of it. But it is specifically the way in which the univalence axiom is imposed that is most central to my objection: we are taking a primitive notion (identity types) which originally had a completely different meaning (equality, in a propositional sense), and changing that meaning without any understanding of the effect that this change of meaning has on the meaning of the theory as a whole. In particular, without any understanding of what the notion of weak $\infty$ -groupoid that we arrived at precisely is.

Posted by: Richard Williamson on April 30, 2015 10:59 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I guess I’m starting to understand some aspects of what you’re objecting to -

You object to the “overloading” of equality in HoTT. This amount to pointing out that in a theory of $\infty$ -groupoids, it might be desirable to reserve the right to characterize identity types differently than the way univalence does. For example, you might want equivalence of $\infty$ -groupids to correspond to equivalence in the usual sense (where we’re allowed to use the axiom of choice for sets, and other classical rules), while identity corresponds to some kind of “computable equivalence”.
You object to how the primitive notions of HoTT are formulated. This amounts to pointing out that in a theory of $\infty$ -groupoids, it might be desirable to postulate compositions and coherence cells more explicitly and combinatorially, rather than deriving them from the identity type constructor and path induction.
You object to a possible “hole” in the theory - a mismatch between syntax and semantics. This amounts to pointing out that it’s still not established that HoTT is sound in all the intended models. I’m not totally clear on the state of affairs here.

Is that a fair summary?

Posted by: Tim Campion on April 30, 2015 5:19 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Yes, it is a fair summary of these aspects!

I would quibble with a few things if I were to try to go from what you have written to a definitive statement on these points. Particularly the second, where I would say that my objection is not tied specifically to saying that compositions and coherences should be more explicitly part of the syntax, in the manner of one of the algebraic definitions of weak $\infty$ -groupoid, although this would certainly be one possibility to which my objection would not apply. And I would just mention regarding the first point, in case there is any confusion, that my own taste would not be towards classical sets (the axiom of choice, etc).

But overall, definitely a fair summary, thank you for taking the time to write it!

Posted by: Richard Williamson on April 30, 2015 7:15 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Thanks for raising these points. I’m pleasantly surprised not to have misunderstood too badly!

Posted by: Tim Campion on April 30, 2015 7:38 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Cubical type theory is syntactic just like the version of HoTT that’s built on top of MLTT. The difference is, roughly, that instead of identity types being defined as inductive families, they are taken as “basic” and we assert various operations on them satisfying certain judgmental rules. These operations are not those of a Batanin $\infty$ -groupoid or a simplicial Kan complex but rather those of an “algebraic uniform Kan cubical set”, but one hopes (as far as I know this is still unproven) that the latter are indeed a model for $\infty$ -groupoids.

Posted by: Mike Shulman on April 30, 2015 2:26 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Unless I misunderstand, in the second approach, you would posit all the various n-cell types and n-cell compositions and coherences as individual constructors

Well, that could be an approach in principle, but it is too na¯ve. In all algebraic approaches to higher groupoids/categories of the kind we are discussing here, the crucial point is to specify the coherences, etc, implicitly, in some nice way (and indeed most of the approaches in the literature do this in a very similar way). In the Ara-Grothendieck-Maltsiniotis approach, this is achieved by the notion of a coherator, and the heart of the matter with trying to find a syntactic formulation would be to express a coherator in MLTT, presumably without building in a syntactic formulation of category theory first.

You’d have two ∞-groupoid structures on your type: the one you posited, and the one coming from the identity types. Presumably you’d say something about how these two interact.

Not at all. I am viewing MLTT only as a foundations which allows us to express an algebraic notion of $\infty$ -groupoid by positing extra types and rules. Identity types are seen exactly as they are intended in the original semantics, namely as a propositional notion of equality. Identity types of terms of identity types (and so on) are likely to be irrelevant.

As a slight digression, I would also like to point out that there is no reason that because identity types correspond to ‘propositional equality’, then having a term of an identity type corresponds to a ‘strict equality’ as in set theory. It could correspond to isomorphism, equivalence, whatever, depending on how the rest of the rules of one’s theory make use of these identity types. This is a principal and undervalued virtue of propositional as opposed to definitional equality, in my view: we are free to say what consequences we wish to allow of having ‘sameness’ (a term of an identity type).

Isn’t it much simpler to simply use the ∞-groupoid structure of the identity types as your object of interest?

There is nothing necessarily wrong with this per se, but this idea alone does not make a syntactic theory of $\infty$ -groupoids. One issue which relates specifically to what you are getting at, if I understand you correctly, I will discuss below.

A more general issue, and the one that is at the heart of this discussion, is that one needs the correct notion of equivalence of $\infty$ -groupoids, and the reason that the univalence axiom is imposed is because ordinary Martin-Löf theory alone does not have this as part of its syntactics under the homotopical semantics. Thus the univalence axiom is fundamental, and it is exactly the univalence axiom that I regard as a hack. The other possible approaches that I am indicating are ones which I do not regard as ‘hacked’.

And in fact I do not find these possible approaches to be less simple, indeed, I would regard them as simpler: we are positing exactly what we need in a way which can be understood in and of itself, and this is cleanly separated from the ‘foundational’ part of MLTT.

Are you worried that there might be ∞-groupoids which can’t arise from identity types?

It is not really this kind of thing that is at the heart of my criticism, but, yes, one has to be careful about what one means. Certainly if one views a type as an $\infty$ -groupoid in the way I think you are getting at (as in the paper Types are weak $\omega$ -groupoids of van den Berg and Garner, for instance), then the expectation, as far as I know, is that one always has some kind of free $\infty$ -groupoid, not an arbitrary one.

It seems to me that we know the “intended model” of any theory of ∞-grouoids; in fact there are many equivalent descriptions of it, e.g. Kan complexes.

Not at all. Kan complexes (are conjectured to) model the homotopy type of a weak $\infty$ -groupoid, but this a completely different matter from having a theory of weak $\infty$ -groupoids itself.

So you must be saying that, yes, it’s a theory of ∞-groupoids, but it’s not synthetic.

I am arguing that it is not a theory of $\infty$ -groupoids at all, synthetic or otherwise, except in a more or less vacuous way (true by redefinition).

Presumably this is because it doesn’t have the right primitive notions?

Yes. Or, more precisely: the approach that is taken in HoTT is not one which I would regard as valid for specifying a theory of anything, because in such a theory we do not understand the primitive notions.

But this brings us back to the first point: we have a few very natural options for which primitive notions to use, HoTT picks one and builds a sound theory around it. What’s the problem?

I don’t know whether what I have written has made things clearer, but my very point is that HoTT does not pick any primitive notion to encode in its syntactics.

I do not mean to say, as I think I have made clear elsewhere in the discussion, that mathematics carried out in HoTT is not valid or interesting mathematics, or anything like that, so there is no ‘problem’ in that sense. I am just justifying why I myself regard the univalence axiom as a hack, and why I avoid it and do not consider HoTT to be a genuine synthetic theory of $\infty$ -groupoids; and the reason that I mentioned that I felt the univalence axiom to be a hack in the first place was because I am not aware of this argument having been made before, and felt that somebody might be interested to ponder it!

Posted by: Richard Williamson on April 29, 2015 9:39 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Hmm.

Maybe I am finally starting to figure out what we’re talking about. I may have contributed to the confusion by being sloppy or even wrong in my phrasing of things.

if one adopts the point of view that HoTT/UT is just another kind of synthetic mathematics, like synthetic differential geometry, then one should I think be very clear about this.

I do adopt that point of view. (With a caveat, see below.)

I didn’t mean to claim that MLTT is itself exactly a synthetic theory of $\infty$ -groupoids. I think MLTT is better viewed as a sort of “primordial” or “neutral” theory that can be interpreted in many different places, so that its types have all sorts of “latent structure”. Its types might be $\infty$ -groupoids, and so we can construct all the operations on higher identity types and we can’t prove UIP. But they might also be topological objects, and so we can define convergent sequences and we can’t prove LEM. Or they might be computable objects, or classical sets, etc. By adding axioms specific to $\infty$ -groupoids (such as univalence) or topological objects (such as a Brouwerian continuity principle) or computable objects (such as strong Church’s thesis) or classical sets (such as the axiom of choice), we make it into a synthetic theory of those things.

(I said as much in the paper, in paragraph 5 of section 5.)

If we want to view MLTT as a synthetic theory in its own right, the only thing I can think of to call it is something like a theory of “collections” — some word broad enough to encompass the possibility of being sets or $\infty$ -groupoids or topological spaces or whatever.

one should be wary of asserting that one exactly captures homotopy types or weak $\infty$ -groupoids

Here I think again the situation is no different than with other synthetic theories. We used to study $\infty$ -groupoids constructed out of sets; now we are interested in studying them based on rules and axioms governing their behavior. Of course the synthetic rules and axioms cannot be expected to capture exactly the analytic theory that we had before, any more than the axioms of SDG can capture exactly the behavior of familiar smooth manifolds. On the contrary, one of the whole points of a synthetic theory is that now it has more models than the analytic theory with which we began, so that our theorems are more general.

In the case of synthetic theories built on MLTT, we get something more general even after imposing new principles because the types retain many other kinds of latent structure as well. In particular, the types of HoTT/UF might have topological or computable structure in addition to their $\infty$ -groupoid structure. We can even combine multiple synthetic theories, e.g. we can have a theory of “topological $\infty$ -groupoids”: this is what cohesion is all about. But that doesn’t prevent HoTT/UF from being a synthetic theory of $\infty$ -groupoids. We don’t reject ZF as a synthetic theory of sets because it has forcing and permutation models.

one should not attempt to claim that intensional Martin-Löf type theory is somehow impractical or deficient as a foundations for mathematics, and that HoTT/UF magically ‘fixes it’ or ‘improves it’.

Here’s one thing that I think can definitely be justified. It’s great to do mathematics in MLTT when possible, without assuming any additional principles, because then the theorems you prove will be true in all derived synthetic theories. But knowing that certain kinds of models or synthetic extensions are possible can and should inform the doing of mathematics in MLTT. This is where HoTT has something to teach even people who would prefer not to assume univalence themselves.

By analogy, a classical mathematician will feel uncomfortable in MLTT because its constructivity makes familiar principles like LEM and AC fail. But once s/he recognizes that the types in MLTT have latent topological or computable structure, this behavior makes much more sense: LEM and AC don’t hold continuously or computably. So in order to do mathematics in MLTT, we need to keep in mind that everything we do has to be continuous or computable.

Similarly, there are some aspects of MLTT, like the failure of UIP, that “look weird” until we recognize that types have latent $\infty$ -groupoid structure. Once we recognize this, we can do mathematics in MLTT in a better way. E.g. we can keep track of which types in a given statement are required to be sets, or truth values, or more generally $n$ -types for other $n$ , those being notions “inspired by HoTT” but which can be defined in plain MLTT.

There is more to it than this, however; I personally do feel that here are deficiencies in MLTT and that HoTT/UF has specific advantages, even relative to other synthetic theories. For instance, MLTT lacks quotients and colimits; HITs provide those. (Actually, MLTT+HITs is still a sort of neutral “theory of collections” that can be interpreted as sets or $\infty$ -groupoids or spaces or whatever.)

MLTT also doesn’t determine what it means for two functions or two types to be equal; I think this is a very unsatisfying attribute for a purportedly foundational theory to be unable to say what it means for two of its basic objects to be equal. You may not like the answer that univalence gives to the question “when are two types equal?”, but I am not aware of any other consistent way to answer that question in a theory based on MLTT.

Finally, the class of models of HoTT/UF is (or at least includes) a very natural and well-behaved class of categories, namely $(\infty,1)$ -toposes. MLTT itself admits models in many more ill-behaved categories (cf. above lack of colimits). But more seriously, this is in contrast to other synthetic theories such as SDG, whose models are a much more restrictive class of categories. There is no general theory of “categories modeling SDG” in the same way there is a beautiful, general, and useful theory of $(\infty,1)$ -toposes.

Posted by: Mike Shulman on April 29, 2015 5:31 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I think MLTT is better viewed as a sort of “primordial” or “neutral” theory that can be interpreted in many different places, so that its types have all sorts of “latent structure”.

If we want to view MLTT as a synthetic theory in its own right, the only thing I can think of to call it is something like a theory of “collections” — some word broad enough to encompass the possibility of being sets or ∞-groupoids or topological spaces or whatever.

I agree with you that MLTT can be thought of in this way, but with the fundamental caveat that we should write: encompass the possibility of being thought of as.

Its types might be …

Again, I agree with you, but with the fundamental caveat that we should write: its types might be thought of as. In other words: yes, we could have all these possible semantics, but they are exactly that, namely semantics for the same original syntactics, or ‘synthetic theory of collections’, as you put it.

By adding axioms specific to ∞-groupoids (such as univalence) or topological objects (such as a Brouwerian continuity principle) or computable objects (such as strong Church’s thesis) or classical sets (such as the axiom of choice), we make it into a synthetic theory of those things.

Here is where we fundamentally disagree. To use the same phrase as I used at the end of my reply to Tim: by adding axioms in this way, we make MLTT into a synthetic theory of something (we do not know what) which in one semantics corresponds more closely to a theory of $\infty$ -groupoids/topological spaces/etc. This may seem like playing with words, but I am trying to express something which is not playing with words at all, but rather a view about the way in which syntactics and semantics relate: in particular, a view that a synthetic theory should be built from the ground up, so that we understand exactly what we are talking about. Hopefully what I wrote in the reply to Tim explains a little more why I feel this is important.

Of course, it might be perfectly possible to find a ‘bottom up’ semantics for one of the ‘modified Martin-Löf type theories’ that you mention, so that we do understand the primitive gadgets. But it is not the adding of axioms to MLTT motivated by a particular semantics that achieves this, and I do not regard this as being the case for HoTT.

Here I think again the situation is no different than with other synthetic theories…

Yes, I agree with what you write in this paragraph and the next. My disagreement is only with the claim that HoTT is a synthetic theory of $\infty$ -groupoids/homotopy types at all, for the fundamental reason above.

But knowing that certain kinds of models or synthetic extensions are possible can and should inform the doing of mathematics in MLTT. This is where HoTT has something to teach even people who would prefer not to assume univalence themselves.

Yes, I have no objection to this, just as mathematics in a non-constructive foundations can inform constructive mathematics.

I personally do feel that here are deficiencies in MLTT and that HoTT/UF has specific advantages, even relative to other synthetic theories. For instance, MLTT lacks quotients and colimits

This issue only arises if one wishes to view all types as sets/ $\infty$ -groupoids/etc. If one instead extends MLTT by positing separately the types and rules that one needs for one’s set theory/ $\infty$ -groupoid theory/etc, as I outlined above in the case of categories to Tim, then it is perfectly natural to build in whatever one needs (quotients, colimits, etc).

One can see this distinction already with natural numbers! Namely, one can view the natural numbers as all of Martin-Löf type theory (this is perhaps clearest with universes: we have the empty universe, then the universe of truth values, then the universe of natural numbers), but we instead typically ‘extend’ Martin-Löf type theory without universes by just positing a type of natural numbers and rules governing it.

Thus I feel that it can be argued that it is ‘overloading’ MLTT (without any extensions) to try to just take types themselves as sets/ $\infty$ -groupoids/etc, and that it is not surprising that quotients, colimits, etc, are lacking.

MLTT also doesn’t determine what it means for two functions or two types to be equal; I think this is a very unsatisfying attribute for a purportedly foundational theory to be unable to say what it means for two of its basic objects to be equal. You may not like the answer that univalence gives to the question “when are two types equal?”, but I am not aware of any other consistent way to answer that question in a theory based on MLTT.

I’m not completely sure what you mean here. Do you mean that there is essentially no way to construct non-trivial terms of type $\mathsf{Id}(A,B)$ where $A$ and $B$ are types (assuming that we have a universe), or of type $\mathsf{Id}(f,g)$ where $f$ and $g$ are terms of a function type? Because the way I view MLTT is precisely that one has the freedom to specify rules which, for instance, allow one to construct terms of identity types. And I certainly agree you that one will need such rules in practise. But there is no problem with this: in the sketch of a synthetic theory of categories that I wrote in reply to Tim, I mentioned for instance that will need to posit rules giving terms of identity types between arrows, to allow for commutative diagrams to be captured. The crucial point with regard to the discussion on the univalence axiom is that, in my view, these rules should be built into the setting up of the theory according to one’s intended semantics, not forced after the fact.

Finally, the class of models of HoTT/UF is (or at least includes) a very natural and well-behaved class of categories, namely (∞,1)-toposes. MLTT itself admits models in many more ill-behaved categories (cf. above lack of colimits).

My view on this is similar to the one I outlined above regarding ‘overloading MLTT’. I see MLTT as a foundations as able to stand on its own feet, without deriving its meaning from any more primitive foundations. This means that, whilst models are of course important and help us to improve our understanding of MLTT, these improvements of understanding do not actually affect the basic semantics of MLTT, and its ability to serve as a foundations. This is in the same way as which the work of set theorists is largely irrelevant to being able to take ZFC as a foundations, even though it improves our understanding of set theory.

For me, it is actually very natural that it is a rather thorny business to fully rigorously define models of Martin-Löf type theory, taking into account all the technical points, because Martin-Löf type theory is rather different as a foundational formalism from the classical ones based on first order logic/set theory, and one should probably not expect it to fit neatly into a different foundational setting.

Posted by: Richard Williamson on April 29, 2015 8:07 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

It just makes no sense to me to object to a theory X (or claim that it “isn’t a theory of blah”) just because, as an accident of history, it arose by adding stuff Y to theory Z, rather than being invented sui generis. You should evaluate the theory on its own as it stands, to decide whether it is good or whether it is a theory of blah. If someone had invented HoTT/UF by sitting in a closed room and thinking about what a synthetic theory of $\infty$ -groupoids should look like, and then when they came out of the room they discovered that their theory consisted of MLTT plus some stuff, would that make you happier? That makes no sense to me; it’s all, as you say, playing with words.

Posted by: Mike Shulman on April 29, 2015 9:12 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

It is not the ‘adding stuff’ that is the problem: as you can see from what I have written elsewhere in this discussion, I have indeed been advocating ‘adding stuff’. The problem is with ‘adding stuff’ which changes the meaning of things in unclear ways.

Maybe the following analogy will help. Constructive propositional logic has a model in the Heyting algebra of truth values. Suppose that we are rather fond of using excluded middle when working with truth values. We might then formulate excluded middle syntactically in constructive propositional logic, and, motivated by our truth value semantics which we are fond of, force it to hold. Now this, I would regard, just like the univalence axiom, as a hack. This is because we no longer (at least a priori) understand the meaning of our primitive notions (propositions). A strong constructivist (as with Bishop’s notorious ‘debasement of meaning’ assertion) would argue that there is no good meaning by means of which we can understand our new theory.

In the same way, I am arguing against the ‘changing of meaning’ caused by the univalence axiom. This is all the more the case because what is claimed is that we have given something meaning (the notion of weak $\infty$ -groupoid), which I would regard us as being very far from understanding the meaning of.

You should evaluate the theory on its own as it stands, to decide whether it is good or whether it is a theory of blah

Yes, as I have already written, one can of course redefine the concept of an weak $\infty$ -groupoid to be a type in one’s new theory, in which case it is vacuously a theory of weak $\infty$ -groupoids. And it indeed might be a perfectly good theory.

But, as I wrote to Tim earlier, I would argue that a theory created by ‘changing meaning’ is always vulnerable to finding a hole, to there being a mismatch between the syntactics and our intended semantics. Maybe such a hole will never turn up, but I am pointing out that the possibility is there, and is not there in a ‘bottom up’ approach.

And, in addition, we may lose something in our redefinition. I happen to think that the search to deeply understand the nature of weak $\infty$ -groupoids so that we could write down a syntactics/synthetic theory of the style I have suggested, will lead to very deep and rewarding mathematics. If it is asserted widely that we now magically have a synthetic theory of weak $\infty$ -groupoids, this could have a significant sociological impact that leads away from trying to understand the nature of weak $\infty$ -groupoids, and I think it is important to recognise that the magic does not give us an answer to this.

If someone had invented HoTT/UF by sitting in a closed room and thinking about what a synthetic theory of ∞-groupoids should look like, and then when they came out of the room they discovered that their theory consisted of MLTT plus some stuff, would that make you happier?

Yes, if the synthetic theory of weak $\infty$ -groupoids were meaningful, namely it explained in a meaningful (I used the words ‘direct and natural’ earlier in the discussion) way how exactly we are to think of a weak $\infty$ -groupoid or a category/2-category/whatever of weak $\infty$ -groupoids.

The point, which I have made all along, is simply that I do not see any way to do this which will give HoTT/UF.

Posted by: Richard Williamson on April 29, 2015 10:36 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

You seem to be using “change the meaning” in two different ways.

Your analogy to constructive logic suggests that you are saying that HoTT “changes the meaning” of things in MLTT. As I’ve said, I think that this is irrelevant, because HoTT should be evaluated as a theory in its own right, independently of the historical accident that it can be described by adding things to MLTT.

You also seem to be saying that HoTT changes the meaning of “ $\infty$ -groupoid” relative to an analytic definition in set theory of the latter. This is true, but it’s exactly the same thing that happens whenever we move from an analytic theory to a synthetic one. The word “line” in synthetic projective geometry is rather more general than its original meaning in real geometry, but we nevertheless use the word “line” for it. Context makes clear whether we are talking about analytic objects or synthetic ones.

I do not know what you mean by “hole” or “mismatch”. As long as we know that the analytic objects are a model of our synthetic theory, which can be true regardless of how our synthetic theory was arrived at, then every synthetic theorem will also be an analytic one. Of course, not every analytic theorem will be a synthetic one, but this is inherent in the fact that passing to a synthetic theory is a process of generalization.

As for your last point, I do find that HoTT gives a meaningful, direct, and natural way to think about weak $\infty$ -groupoids.

Posted by: Mike Shulman on April 30, 2015 12:27 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Your analogy to constructive logic suggests that you are saying that HoTT “changes the meaning” of things in MLTT.

Exactly, but also, crucially (after all, I would have thought the observation that we change the meaning to be evident): we do not know what we have changed the meaning to. To put it bluntly, I am arguing that the types in HoTT/UF are in themselves meaningless.

Now most mathematicians are not particularly interested in questions of meaning, and do not appreciate that such questions are significant. Therefore most mathematicians will be entirely happy with a meaningless theory (of course they would not put it that way themselves!). So long as it performs some purpose within mathematics, let us accept it. Maybe this is how you yourself view the matter.

But for me, meaning is important. And the concept of a weak $\infty$ -groupoid is one whose meaning I consider to be deep, and which I regard as far from understood. So for me, having a synthetic theory of weak $\infty$ -groupoids would say that we have such an understanding. But for me, it does nothing of the sort: HoTT/UF tells me next to nothing about what a weak $\infty$ -groupoid is.

HoTT should be evaluated as a theory in its own right, independently of the historical accident that it can be described by adding things to MLTT

I feel that I’ve responded to this several times now. The question of the historical evolution of the ideas is irrelevant to my point. If MLTT had never been thought of, and HoTT/UF was written down in one go, my criticism would be the same: what does it mean? You might respond: we think of types as ‘weak $\infty$ -groupoids’ or ‘homotopy types’ in such a way, we think of the rest of type theory in such a way, now look what we can do with our theory! But that does not truly give meaning, for me. I am arguing that we should know what we are talking about, whilst you are arguing that we do not need to know what we are talking about, it is enough to think we know what we are talking about, as long as we do not run into any problems in practise.

You also seem to be saying that HoTT changes the meaning of “∞-groupoid” relative to an analytic definition in set theory of the latter.

No: I do not regard us as understanding the meaning of ‘weak $\infty$ -groupoid’ at all, in either an analytic (in any foundations) or synthetic sense. We have some expectations as to what a weak $\infty$ -groupoid should be (the homotopy hypothesis, the intuition coming from strict $\infty$ -groupoids, the proposed algebraic definitions, etc), and part of the reaching an understanding of the meaning of the notion of weak $\infty$ -groupoid will be either to meet these expectations, or to explain why they cannot be fulfilled. HoTT/UF achieves none of this.

I do not know what you mean by “hole” or “mismatch”. As long as we know that the analytic objects are a model of our synthetic theory, which can be true regardless of how our synthetic theory was arrived at, then every synthetic theorem will also be an analytic one.

Yes, but not necessarily in a way which we like. To take the analogy with constructive propositional logic again: we might, somewhere again the line, discover a consequence of imposing excluded middle that we do not like, because we do not regard it as meaningful. In other words, we discover a ‘hole’ in our theory: we cannot justify/explain its meaning. If we have built a massive edifice upon our ‘meaningless’ theory with excluded middle, it will be a huge task to rebuild it, which we could have avoided if we had paid attention to meaning from the beginning.

In the case of HoTT/UF, we might find something somewhere along the line that we do not regard as meaningful from the point of view of thinking of types as weak $\infty$ -groupoids: again, we will have a ‘hole’ in our theory which we cannot give meaning to. Such a ‘hole’ might be serious, or it might not, but the point is: who knows?

I do find that HoTT gives a meaningful, direct, and natural way to think about weak ∞-groupoids.

Of course, there is no absolute sense in which anybody could persuade you otherwise! But maybe something of what I’ve written regarding why I do not find this will strike a chord with somebody!

Posted by: Richard Williamson on April 30, 2015 10:27 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I guess this discussion is going nowhere; I can’t think of anything more to say than “I’m sorry that you don’t think you understand what $\infty$ -groupoids are; the rest of us do.” (Of course “understanding” them doesn’t mean that every possible theorem about them has already been proven, otherwise we could never understand anything in mathematics.)

Posted by: Mike Shulman on April 30, 2015 2:29 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Yes, I feel that I have made my argument as best I can. In the last few comments, I have felt myself to be addressing misunderstandings of things I have written, rather than really saying anything new.

I don’t think there was any need for the following though, which seems to me rather condescending.

“I’m sorry that you don’t think you understand what ∞-groupoids are; the rest of us do”

I have thought deeply about weak $\infty$ -groupoids and higher categories in general for a number of years, and I have been trying to make what I feel is a serious point that is informed by that thinking. You may not appreciate it, understand it, or agree with it, but maybe there is somebody amongst ‘the rest of us’ who does think that there is something to it.

(Of course “understanding” them doesn’t mean that every possible theorem about them has already been proven, otherwise we could never understand anything in mathematics.)

I have suggested nothing of this sort. It, as I feel with some other comments, seems a little like an attempt to trivialise the point I have been making.

Posted by: Richard Williamson on April 30, 2015 4:35 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I’m sorry, I didn’t mean to sound condescending. I should have said instead “many of us do”. For what it’s worth, I found your

you are arguing that we do not need to know what we are talking about, it is enough to think we know what we are talking about

to also sound somewhat condescending (plus incorrect). It seems like we are both getting too frustrated to continue having a polite discussion, plus as you said we have made our points. I would like to thank you for the discussion, however; it has at least helped me to clarify my own opinions.

Posted by: Mike Shulman on April 30, 2015 6:12 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

No problem!

For what it’s worth, I found your

you are arguing that we do not need to know what we are talking about, it is enough to think we know what we are talking about

to also sound somewhat condescending (plus incorrect).

My apologies that it came across this way, this was very far from my intention. My sincere intention was to try to find a phrasing which would help to illustrate what I feel to be the difference between the two points of view: I had not succeeded in the phrasings I had chosen before, so I tried something that might be a little more ‘dramatic’/emphasise the difference a little more starkly.

With all due assurance that I mean no offence and that the personal tone was only for ‘dramatic effect’ and was not personal in the pejorative sense, I must say that I do stand by that sentence: it does express the way I see the difference in our points of view. If you or somebody else wishes, I can elaborate on/clarify that, but otherwise I am happy to leave it at that, as you suggest.

Thank you too for the discussion!

Posted by: Richard Williamson on April 30, 2015 7:28 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

No problem!

For what it’s worth, I found your

you are arguing that we do not need to know what we are talking about, it is enough to think we know what we are talking about

to also sound somewhat condescending (plus incorrect).

With all due assurance that I mean no offence and that the personal tone was only for ‘dramatic effect’ and was not personal in the pejorative sense, I must say that I do stand by what I wrote: it does express the way I see the difference in our points of view. If you or somebody else wishes, I can elaborate on/clarify that, but otherwise I am happy to leave it at that, as you suggest.

Thank you too for the discussion!

Posted by: Richard Williamson on April 30, 2015 7:29 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

You shouldn’t blame a theory of X for not “actually” being a theory of X because it is discovered to be essentially the same as an existing theory of Y. To the contrary, such discoveries are the deep and important insights that connect mathematics together! In particular, the fact that the basic structure of HoTT/UF is the same as that of MLTT doesn’t prevent us from claiming that the types “are really synthetic $\infty$ -groupoids” any more that it prevents us from claiming that they really are… um, whatever Martin-Lof said they were. Just because Martin-Lof discovered the theory first doesn’t mean that it is intrinsically about what he said it was about any more than it is intrinsically about anything else that we discover later that it might just as well be about.

(I suppose “the original semantical justification” refers to the much-vaunted “meaning explanation”? Despite several long conversations with type theorists about it, I still haven’t figured out in what sense the “meaning explanation” “explains” anything. It seems to be trying to explain type theory in terms of something untyped, which to me is utterly backwards from reality: types come first.)

It’s true that the current implementation of univalence as an axiom is unsatisfactory. But that’s not a reason to reject HoTT/UF, only a reason to seek to improve it.

Posted by: Mike Shulman on April 27, 2015 4:53 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

As is hopefully clearer from the reply I have just written to Dimitris, I am arguing that no such discovery has been made. A deep and important discovery has been made that there is a connection between intensional Martin-Löf type theory and homotopy theory/the theory of $\infty$ -groupoids. It is the claim that these two theories are the same that I disagree with, precisely because of the a posteori nature of HoTT/UF.

Of course, one can redefine homotopy theory or the theory of weak $\infty$ -groupoids to be that captured by HoTT/UF. But it should be made clear that this is what one is doing. And one is then free to observe, as I am doing, that this redefinition may not capture all aspects of what we may wish to think of as homotopy theory or a theory of weak $\infty$ -groupoids.

I suppose “the original semantical justification” refers to the much-vaunted “meaning explanation”?

I’m not sure exactly what you mean by the ‘meaning explanation’. I am myself just thinking of the basic semantics as explained, for instance, in the notes Intuitionistic type theory taken by Sambin. I am very fond also of On the meanings of the logical constants …. These notes were a revelation to me when I first read them a number of years ago, one of the works that most influenced the way I think about mathematics.

Just because Martin-Lof discovered the theory first doesn’t mean that it is intrinsically about what he said it was

Of course.

Posted by: Richard Williamson on April 28, 2015 1:28 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Meaning explanations. Can you give a link that describes the explanations you are thinking of?

Posted by: Mike Shulman on April 29, 2015 5:33 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Ah, what is written on nLab page is not what I would consider to be the basic semantics of Martin-Löf type theory, nor is it the explanation which I think Martin-Löf had in mind in the quote (which is taken from the notes of Sambin, and which I wholeheartedly agree with!) at the end of the introduction section.

These notes of Sambin that I was referring to can be found here.

On the meaning of the logical constants… can be found here.

But I would be surprised if you were not familiar with both of these already, and I’m sure you will be familiar with the semantical explanations given.

Posted by: Richard Williamson on April 29, 2015 8:35 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I’m not sure if this is implied by the article, but I certainly think that the philosophical justification of UF should not stop at declaring “You have your own intuitions, we have our own, and time will tell that ours are just as robust as yours.” There is more to be said about the intuitive meaning of homotopy types as abstract shapes.

That’s a good point; I should try to bring it out more. A related point, which perhaps I didn’t emphasize strongly enough, is that with HoTT/UF we no longer need to think of an $\infty$ -groupoid as a tower of infinitely many different kinds of equality/isomorphism; we can think of it as a single coherent thing. I mentioned this advantage of the synthetic viewpoint, but perhaps my wording sounds like it was mainly about technical mathematical convenience, when I think there is also a big psychological/intuitive/philosophical benefit.

Posted by: Mike Shulman on April 24, 2015 8:21 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Here’s a first try at a new concluding paragraph (probably now in a section by itself):

There is much more to HoTT/UF than I have been able to mention in this short chapter, but those aspects I have touched on revolve around a single idea, which generalizes Bishop’s set-definition principle: whenever we define a collection of objects, we must also pay attention to the identifications and higher identifications between them. Sometimes these identifications arise “automatically”, such as from the univalence axiom; other times we have to generate new ones, as with higher inductive types. But in no case must we (or even can we) separate those identifications from the objects themselves: with $\infty$ -groupoids as basic foundational objects, every collection carries along with itself the appropriate notion of identification between its objects. This can be regarded as the central innovation of HoTT/UF, both for mathematics and for philosophy.

Posted by: Mike Shulman on April 24, 2015 9:38 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

one ought to consider adding shape modalities as in cohesive HoTT in order to be able to strengthen the interaction between the synthetic and the “analytic” side

I agree entirely! I’ve been working on exactly this problem recently, and I have some partial results: in cohesive HoTT I can prove (and have formalized in Coq) that the shape of the topological circle is the homotopical circle. A very similar argument ought to show that the shape of the topological sphere is the homotopical sphere, so that from the inequivalence of the homotopical circle and sphere one could conclude the inequivalence of the topological ones.

However, I unfortunately don’t really have space to discuss cohesion in this chapter; I’m already pushing up against the word limit. But perhaps I should add a footnote or something in the paragraph where $S^1$ and $S^2$ are introduced, warning that these are purely homotopical spheres and that to relate them to the topological ones requires something more.

Posted by: Mike Shulman on April 24, 2015 7:51 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Cohesion turns up in my chapter. I’m sure there could be some useful cross-referencing, if people get to see each other’s work.

Posted by: David Corfield on April 24, 2015 8:11 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Here’s a first try at such a footnote:

This is a “homotopical” circle, not a “topological” circle such as $\{(x,y)\in \mathbb{R}\times \mathbb{R} \mid x^2+y^2=1\}$ . The latter can also be defined in HoTT/UF, of course, but it will be a {set}, whereas the HIT $S^1$ is not. The HIT circle is so-called because the corresponding classical $\infty$ -groupoid is “homotopically presented” by the topological circle, with identifications in the former arising from continuous paths in the latter, and historically $\infty$ -groupoids were studied mainly by using topological presentations. This relationship between the two circles ought also to be true in HoTT/UF, but it becomes much easier if we add “cohesion” (regarding which, see Corfield’s chapter).

Posted by: Mike Shulman on April 24, 2015 9:37 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I of course completely agree with the content of the footnote. The following is no longer relevant to the content of the article as such, just a general question.

This relationship between the two circles ought also to be true in HoTT/UF

I’m quite surprised by this. My intuition is that there shouldn’t be enough in the mere syntax of identity types in a univalent universe (without cohesion) to always give us a geometric realization “functor” that behaves as it does in the usual cases. Not sure exactly how to make this precise - perhaps by saying that there will always be some kind of geometric realization but it won’t always have all the properties of the usual geometric realization e.g. left exact, has a right adjoint etc. Is there a good reason to believe that in UF (without cohesion) we will always have a good geometric realization from synthetically defined homotopy types to topological spaces defined as h-sets? Or am I misunderstanding your quote?

Posted by: Dimitris on April 25, 2015 12:29 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Even classically, there is definitely no faithful functor from homotopy types to ${Top}$ , so I don’t think that’s what Mike has in mind. Geometric realization is a functor from simplicial sets to ${Top}$ , but homotopy types are a localization of simplical sets and the functor does not extend along this localization (although perhaps it extends up to a 2-cell?). The goal would have to be to construct an arrow $Top \to Type$ (that’s the 1-type of topological spaces and homeomorphisms on the left and the universe on the right) which, after 1-truncation of $Type$ , satisfies the universal property of localization of weak equivalences (there are probably better ways to state that universal property).

Actually, this description of the arrow:

The HIT circle is so-called because the corresponding classical ∞-groupoid is “homotopically presented” by the topological circle, with identifications in the former arising from continuous paths in the latter, and historically ∞-groupoids were studied mainly by using topological presentations.

sounds really exciting (or maybe I’m just behind the times!). Unless I’m misinterpreting, the approach is to present the homotopy type of the circle as a higher inductive type with one point constructor for each point of the topological circle, one path constructor for each continuous map from the topological interval to the topological circle, and so forth (all the way up – although perhaps this is hard to formalize?). In the classical setting, one has to go through various contortions to construct the homotopy category, but here it sounds like it just arises naturally from the most naive notion of what the homotopy type of a space should be!

Will this construction work for arbitrary topological spaces, or just for CW complexes or something?

Posted by: Tim Campion on April 25, 2015 5:18 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Right, I didn’t say anything about geometric realization. As Tim says, even classically there is no geometric realization from $\infty$ -groupoids to topological spaces, only the “shape” (“fundamental $\infty$ -groupoid”) functor ʃ from spaces to $\infty$ -groupoids. Saying that the homotopical circle is presented by the topological circle means that the shape of the latter is the former; it says nothing about any functor in the other direction.

The goal would have to be to construct an arrow $Top \to Type$ … which, after 1-truncation of $Type$ , satisfies the universal property of localization of weak equivalences

No, I don’t think that can be expected either. Such a universal property would imply that every type can be presented by a topological space, which is true classically but can’t be expected to be true in HoTT/UF (unless we add it as an extra classicality axiom). In particular, that would imply that every type admits a surjection from a set (the set of points of a presenting space), which is false in some models.

I think the most we can expect in pure HoTT/UF is that there is that arrow $ʃ:Top\to Type$ , not that it has any universal property.

the approach is to present the homotopy type of the circle as a higher inductive type with one point constructor for each point of the topological circle, one path constructor for each continuous map from the topological interval to the topological circle, and so forth (all the way up – although perhaps this is hard to formalize?).

Yes, that’s what I’m suggesting ought to be true, and it is indeed quite hard to actually do (hence why no one has done it yet); it seems to depend on solving the “problem of infinite objects”. It might be doable in HTS. If it were doable, then it ought to work for any topological space.

In cohesive HoTT, however, the situation is different: we do have the arrow ʃ (as opposed to merely hoping/expecting to have it), and it does have a universal property: it’s a reflector into the subcategory of “topologically-discrete types”. Moreover, in “real-cohesive HoTT”, we actually have a construction of ʃ: it is the nullification at the type of Dedekind reals. That is, $ʃ X$ is obtained from $X$ by universally forcing every map $\mathbb{R} \to X$ to be constant. In particular, any two points connected by a (topological!) path are forced to become equal (i.e. connected by a “homotopical path”). This nullification, like any localization, can be presented as a single recursive HIT which (somewhat magically) turns out to do this coherently in all dimensions.

Posted by: Mike Shulman on April 25, 2015 7:24 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

It’s interesting to hear that “topological” homotopy types might not include all types.

Now, the “topological homotopy types” should be the same as homotopy types of CW complexes. But there’s already another class of types that (I think?) I should think of as being like CW complexes – namely the class of higher inductive types which can be defined “without parameters”, i.e. the arities of the constructors must be sets (e.g. $S^2$ has a point constructor and a 2-loop constructor, but both constructors have a contractible domain). Does that seem roughly correct, and if so, should these two classes of “homotopy types of CW complexes” coincide?

In a sheaf model, (I think?) the homotopy types constructible from topological spaces should be the locally constant sheaves. So an analogous question is: in a sheaf model, do the simplest higher inductive types, like $S^2$ , end up being (locally) constant sheaves?

Also, in the discussion of the cohesive approach, I’m a little confused about how the “magic” works. Is it the case that a natural cohesive structure exists on natural models of HoTT, but that it’s difficult (or impossible) to construct a cohesive structure internally to HoTT?

Posted by: Tim Campion on April 26, 2015 4:59 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Does that seem roughly correct, and if so, should these two classes of “homotopy types of CW complexes” coincide?

I expect so… perhaps modulo some issues involving infinity. Certainly for finite CW complexes it should be true. Maybe also for infinite ones, but you’d have to be a little careful with whether the infinity is internal (parametrized by nat) or external (E.g. a “HIT” with infinitely many constructors).

in a sheaf model, do the simplest higher inductive types, like $S^2$ , end up being (locally) constant sheaves?

Yes, because they are “just colimits”, and the “constant sheaf” functor preserves colimits. So I think you really only get constant sheaves this way, not locally constant ones.

Is it the case that a natural cohesive structure exists on natural models of HoTT, but that it’s difficult (or impossible) to construct a cohesive structure internally to HoTT?

You have to specifically construct a cohesive model. I’m not sure what you mean by a “natural” model of HoTT. I would say that one natural class of models for HoTT is $\infty$ -toposes. The “canonical” $\infty$ -topos $\infty Gpd$ does not support any nontrivial cohesive structure, but other models (such as this one) do.

Since not all models have a nontrivial cohesive structure, one can’t be constructed internally, but one can get surprisingly close — one example of this is what I call “real-cohesion”. A cohesive structure consists of a triple of modalities $ʃ \dashv \flat \dashv \sharp$ , and you can construct good candidates for ʃ and $\sharp$ internally, by nullifying at $\mathbb{R}_D$ and localizing at $\mathbb{R}_C\to\mathbb{R}_D$ respectively. But the existence of a corresponding $\flat$ linking the two then has to be postulated.

Posted by: Mike Shulman on April 26, 2015 6:06 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Right, OK - that makes sense. For some reason I had read the footnote as saying the inverse which is why I spoke of realization, though when I said realization I meant it loosely, i.e. not as an actual functor $\mathcal{U} \rightarrow$ Top but of some sort of process of turning a type defined as a HIT into a topological space. The footnote is perfectly clear and the new version even more so. Also, thanks for all the clarifications Tim and Mike.

This is moving too far from your post, but with respect to this

[I]t seems to depend on solving the “problem of infinite objects”. It might be doable in HTS.

Right - I mean essentially this is a special instance of a more general problem, which is how to make HoTT/UF talk about HITs internally. If one were able to do this then one could use the relevant topological information (e.g. points and paths) and send it to the HIT generated by that information, but of course there is no way to “send it to the HIT” internally which is why $\int$ hasn’t been defined yet. Right? I cannot see any way in which $\int$ could be defined without, as you essentially suggest, making HoTT/UF eat itself.

It’s really nice how cohesive HoTT seems to circumvent this difficulty with some very natural looking axioms - though the details are not fully clear to me. Looking forward to reading your work on $\int$ in cohesive HoTT. Is it available anywhere by the way, or not yet?

Posted by: Dimitris on April 26, 2015 5:23 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

essentially this is a special instance of a more general problem, which is how to make HoTT/UF talk about HITs internally

I wouldn’t quite say that. I would say that we don’t yet even know how to define the realization as a HIT, because of the problem of infinite objects; it’s not a question of internalizing HITs. It’s true that we do sort of have realization as a “HIT with infinitely many constructors”, but I wouldn’t consider the problem of reducing that to finitely many to be the same as the problem of internalizing HITs. By “internalizing HITs” I would think of finding a “generic” HIT that can represent all of them, analogous to W-types for ordinary inductive types, and that’s not necessary or sufficient for having realization as a single (finite) HIT.

No, I haven’t posted that work anywhere yet. Kind of swamped recently with this philosophy stuff, not to mention other personal and professional committments….

Posted by: Mike Shulman on April 26, 2015 6:05 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Here’s an attempt to further clarify the footnote:

This is a “homotopical” circle, not a “topological” circle such as $\{(x,y)\in \mathbb{R}\times \mathbb{R} \mid x^2+y^2=1\}$ . The latter can also be defined in HoTT/UF, of course, but it will be a set, whereas the HIT $\mathbb{S}^1$ is not. The homotopical circle is so-called because it is the shape (a.k.a. “fundamental $\infty$ -groupoid”) of the topological circle, in which continuous paths are made into identifications; and historically $\infty$ -groupoids were originally studied as shapes of topological spaces. In HoTT/UF the shape ought to be constructible as a HIT, but no one has yet managed to do it coherently at all levels. Unlike classically, not every type in HoTT/UF can be the shape of some space, but we can hope that the HIT $\mathbb{S}^1$ will still be the shape of the topological circle. (There is also a different approach to such questions called “axiomatic cohesion”; see Corfield’s chapter.)

Posted by: Mike Shulman on April 25, 2015 7:50 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Some minor comments:

(1) Although it doesn’t affect any of the points you are trying to make and is indeed a purely terminological point, I am of the opinion that it is not right to think of general covariance as an instance of gauge invariance. In particular general relativity should not be thought of as a gauge theory with the Einstein group as the gauge group. But this does not take away from any of your points.

(2) In footnote 3 on p. 5 you write

A model of ZFC (or similar) can then be constructed in the usual way, or directly as in [26, §10.5].

By the “usual way” I’m guessing you mean by adding e.g. the categorical replacement axiom, i.e. taking ETCS+R, right? Is it known whether there is a model of UF+LEM in which $Set_U$ does satisfy categorical replacement? Is it perhaps immediate that in the simplicial model $Set_U$ is a model of ZFC? (I’m sorry if this is trivial).

(3) I think there is a typo on the third paragraph of p. 9: “some of constructors of”

(4) Is it fair to say that your conclusion is: The central message from UF/HoTT is that a Bishop-style $\infty$ -groupoid theory can fruitfully be regarded as a foundation for mathematics? (I got a bit lost in the phrasing of the last paragraph.)

Posted by: Dimitris on April 24, 2015 5:07 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

(Just to clarify, when I said in (1) “it’s a purely terminological point” I meant it is so for the purposes of your article. I don’t think it’s a purely terminological point in general. I think in general general covariance and gauge invariance should certainly be thought of as different concepts.)

Posted by: Dimitris on April 24, 2015 5:10 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Actually, by “in the usual way” I meant to refer to the Cole-Mitchell-Osius construction by which one obtains a material set theory like ZFC from a structural set theory like ETCS. That’s the main point here, not anything about the replacement axiom; maybe I should clarify that. (In HoTT/UF the replacement axiom is basically automatic because we have universes.)

Posted by: Mike Shulman on April 24, 2015 7:58 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Ah, OK – then I would say that the way that the footnote is phrased sounds like you automatically get a set theory equiconsistent to ZFC in UF+LEM via the model $Set_U$ but $Set_U$ models ETCS which is weaker than ZFC.

You do of course get ZFC as a HIT but adding the ZFC HIT should correspond to a stronger system than “merely” UF+LEM right?

Posted by: Dimitris on April 24, 2015 8:22 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Unlike ZFC, “HoTT/UF” does not (yet) refer to a unique specific well-defined system of rules/axioms. Personally, when I say “HoTT/UF”, I always include HITs as one of the rules. It’s true that if you leave out HITs, then you can prove strictly less; but I’m not sure whether it changes the consistency strength or not.

Here’s a suggested replacement:

More precisely, there is a subclass of the $\infty$ -groupoids of HoTT/UF which together satisfy the axioms of ETCS. (If we exclude the Axiom of Choice and Law of Excluded Middle from HoTT/UF, which is common, then we get instead an “intuitionistic” version of ETCS.) A model of ZFC can then be constructed using trees as described in McLarty’s chapter, or directly as in [26, §10.5].

Posted by: Mike Shulman on April 24, 2015 10:08 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

It’s true that if you leave out HITs, then you can prove strictly less; but I’m not sure whether it changes the consistency strength or not.

The picture ought to be that that univalence doesn’t add consistency strength and HITs don’t add consistency strength compared with an equal number of iterated (0-)inductive types. (And propositional resizing adds much more strength, in any case.)

Posted by: Ulrik Buchholtz on April 25, 2015 3:43 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Why ought that to be the picture?

Posted by: Mike Shulman on April 25, 2015 7:09 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

The first part would follow from an internal model construction, e.g., the cubical modal. For the part about HITs, we would need to build them in the model using 0-inductive types, which I’m less sure about but seems plausible. (On the other hand, it clear that propositional resizing gives power types and a fortiori all 0-inductive types, but I don’t see how to build HITs using propositional resizing; of course one could still build an internal model in which to interpret them, again like the cubical model, or even, I suppose the simplicial model, if we’re just concerned with consistency strength.)

Posted by: Ulrik Buchholtz on April 25, 2015 1:20 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I’m sorry if I’m being slow here, but I’m having quite a hard time understanding this. Perhaps I’m misunderstanding the set-up. Let’s call MLTT+U the system of intensional MLTT with all usual type constructors including W-types and a universe U closed under these type constructors. Are you saying that MLTT+U+Univalence for U should be of the same consistency strength as MLTT+U+HITs? Or am I completely misunderstanding you?

Posted by: Dimitris on April 26, 2015 5:31 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Yes, that’s one thing I’m saying. More precisely, I conjecture that in each of the following lines, the items have the same consistency strength, where now, MLTT is Martin-Löf type theory with N, +, Σ, Π, Id-types, and U a universe closed under these. When we add (higher) inductive types, these are added to U, and UA is the univalence axiom:

MLTT, MLTT + UA for U
MLTT with n universes, MLTT with n univalent universes
MLTT + n iterated inductive types in U, MLTT + UA + n iterated HITs in U
MLTT + W types in U, MLTT + UA + unlimited iterated HITs in U
MLTT + Prop type in U, MLTT + W + Prop in U, MLTT + UA + Prop. resizing, MLTT + UA + Prop. resizing + unlimited iterated HITs

The first item in the last line includes the impredicative Prop universe from the calculus of constructions. (There are of course variations for a hierarchy with multiple or an unlimited number of universes.)

Is that clearer?

Posted by: Ulrik Buchholtz on April 26, 2015 10:29 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Yes, thanks, this is much clearer. I thought initially you were saying that MLTT+UA for U would have the same strength as MLTT + UA + HITs in U, which seems to me harder to believe.

Posted by: Dimitris on April 27, 2015 1:48 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Just a small nit-pick

If we exclude the Axiom of Choice and Law of Excluded Middle from HoTT/UF, which is common, then we get instead an “intuitionistic” version of ETCS.

Without either LEM or AC we only get a $\Pi W$ -pretopos right? Is that what you mean by an “intuitionistic version of ETCS”? Because I think strictly speaking intuitionistic ETCS would be stronger that a $\Pi W$ -pretopos.

Posted by: Dimitris on April 26, 2015 5:36 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Without LEM and without propositional resizing, yes we get only a $\Pi W$ -pretopos. As I said elsewhere, I’m not using “HoTT/UF” to refer to a single unique formal system, and I haven’t specified whether resizing is included. I also put “intuitionistic” in quotes to try to avoid this kind of question; you seem to be following the material-set-theory convention whereby “intuitionistic” implies impredicativity? Maybe I should say “constructive/intuitionistic” to be extra clear.

Posted by: Mike Shulman on April 26, 2015 6:05 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I think it’s perfectly clear, especially given the fact that you are using HoTT/UF as a generic term for a cluster of formal systems, as you just reminded me.

Posted by: Dimitris on April 26, 2015 6:12 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Regarding whether GR is a gauge theory, there seems to be some dispute within the physics community: a quick google turns up this and this and this. Since I’m not writing about physics, I feel justified in saying that gauge invariance is used broadly to refer to the phenomenon in question. But maybe I’ll reword it a bit so as not to seem to be taking a side here.

Posted by: Mike Shulman on April 24, 2015 9:44 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Mike,

Regarding whether GR is a gauge theory, there seems to be some dispute within the physics community: a quick google turns up this and this and this. Since I’m not writing about physics, I feel justified in saying that gauge invariance is used broadly to refer to the phenomenon in question.

Here is a quote from R.M. Wald’s General Relativity (1984):

… if $\phi : M \to N$ is a diffeomorphism, then $M$ and $N$ have identical manifold structure. If a theory describes nature in terms of a spacetime manifold $M$ and tensor fields $T^{(i)}$ defined on the manifold, then if $\phi : M \rightarrow N$ is a diffeomorphism, the solutions $(M, T^{(i)})$ and $(N, \phi^{\ast}T^{(i)})$ have physically identical properties. Any physically meaningful statement about $(M, T^{(i)})$ will hold with equal validity for $(N, \phi^{\ast}T^{(i)})$ . On the other hand, if $(N, T^{\prime}^{(i)})$ is not related to $(M, T^{(i)})$ by a diffeomorphism and if the tensor fields $T^{(i)}$ represent measurable quantities, then $(N, T^{\prime}^{(i)})$ will be physically distinguishable from $(M, T^{(i)})$ . Thus, the diffeomorphisms comprise the gauge freedom of any theory formulated in terms of tensor fields on a spacetime manifold. (Wald 1984: 438, emphasis added)

Posted by: Jeffrey Ketland on April 25, 2015 3:01 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Typo: “by analogy with Turing-complete programming languanges”

Posted by: Blake Stacey on April 24, 2015 7:48 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Mike, here are some quick comments, some on Frege directly related to (i) the history of type theory, (ii) lambda abstraction and (iii) what identity means.

So far as I’m aware, the first person to discuss the intensionality of identity statements is Frege, 1892, “On Sense and Reference”. This article introduces and anticipates everything that came later. We have distinct terms $t$ , $u$ and a truth “ $t = u$ ”, and Frege asks how this can be informative, given that they denote the same object. His answer is to distinguish the sense (intension, Der Sinn) of the terms from their reference (Der Bedeutung). He goes on to develop things further. Frege calls the sense “the mode of presentation”, although it’s a matter of huge debate what senses are. Some people have argued that they are akin to proofs.
I think the point about “0.5” versus “0.5000…” amounts to the same point. We have distinct syntactical entities (linguistic expressions) denoting the same real.
Frege’s definition of “ $n$ is a number” in Frege 1884, The Foundations of Arithmetic (and 1893) isn’t quite “the set of all sets equinumerous to a given one”. In particular, Frege has a type (or order/level) distinction. But his own definition is mixed up with the problems that Russell discovered around 1901. Roughly, Frege tries to map second-level concepts down to first-level objects, and this causes the paradox.
A good argument can be made that Frege invented the type distinction between objects and concepts, and worried a lot about it. See, e.g., “Function and Concept” (1891).
Frege’s official formal theory is second-order logic, a kind of type theory or 2-sorted logic. Frege didn’t use anything like set theory as now understood. He used second-order comprehension $\exists X \forall y(X(y) \leftrightarrow \phi(y))$ . The problem arise here because of the abstraction principle he introduced, $ext(X) = ext(Y) \leftrightarrow \forall z(X(z) \leftrightarrow Y(z))$ . This, with comprehension, leads to contradiction.
Frege introduced $\lambda$ -abstraction in his “Function and Concept” (1891). This was later adapted by Church (1940). Look at page 136: this is $\lambda$ -abstraction. I quote from the SEP article on $\lambda$ -calculus: “ $\lambda$ -calculus arose from the study of functions as rules. Already the essential ingredients of the subject can be found in Frege’s pioneering work (Frege, 1893). Frege observed, as we did above, that in the study of functions it is sufficient to focus on unary functions (i.e., functions that take exactly one argument). (The procedure of viewing a multiple-arity operation as a sequence of abstractions that yield an equivalent unary operation is called currying the operation. Perhaps it would be more historically accurate to call the operation fregeing, but there are often miscarriages of justice in the appellation of mathematical ideas.)”
By and large, I think that what you write as “ $x$ is equal to $y$ ” ought better to be considered to mean “ $x$ and $y$ are indiscernible”, rather than $x = y$ . There are many ways that $x$ and $y$ might be indiscernible; mappings are one example. But “indiscernible” doesn’t mean “identical”.
It’s true there is a considerable debate about the sense in which GR is a “gauge theory”. But Wald’s account of equivalent spacetime models (Wald 1984, General Relativity, p 438) is described as “gauge equivalence”. If $\phi: M \to N$ is a diffeomorphism, then spacetime models $(M,T^{(i)})$ and $(N,\phi_{\ast}T^{(i)})$ represent the same physical situation, and are gauge equivalent in that sense.

Posted by: Jeffrey Ketland on April 25, 2015 11:59 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Thanks. Most of that doesn’t really seem relevant to the paper I’m writing, except (7) which I disagree with, and (3) which means that perhaps I should waffle a little bit more about Frege’s definition of cardinality. SEP says “Frege defined ‘the number of the concept F’ … to be the extension or set of all concepts that are equinumerous with F”, so I think I’m on reasonably solid ground.

Posted by: Mike Shulman on April 25, 2015 9:36 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Mike, I kind of agree. By the way, I should say - nice paper. I enjoyed reading it, and, as always, really clear. The Frege stuff is sitting in the background and is a bit hard to summarize (Frege uses “concept” to mean a second-order/level entity, not an object, as opposed to first-order set theory, where everything is an object). But while it’s not so closely related as such, I think it does relate more directly to the broader underlying philosophical debate here, which involves questions about how identity ought to be understood. (Maybe we come back to this another time, with David, Dimitris, too…) Still, the Wald quote might be useful though – even if it’s just to confirm that your brief analysis of the hole argument being expressed in terms of gauge equivalence is fine from the perspective of a standard monograph on the subject. Yeah, I know you disagree with (7) - I just had to register a lonely voice of protest!

Posted by: Jeffrey Ketland on April 25, 2015 11:11 PM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

Thanks!

Posted by: Mike Shulman on April 27, 2015 6:15 AM | Permalink | Reply to this

Re: A synthetic approach to higher equalities

$MathML-enabled post (click for more details).$

I have updated the posted version to the one that I just sent to Elaine, which incorporates the very helpful suggestions from everyone here, as well as others who sent feedback privately. I am very, very grateful to everyone who helped; I think the chapter is exceedingly better for your feedback.

Posted by: Mike Shulman on April 27, 2015 6:26 AM | Permalink | Reply to this

Re: A Synthetic Approach to Higher Equalities

$MathML-enabled post (click for more details).$

The book is now available for pre-order at OUP and Amazon. The OUP link includes a special discount code; but for those of us in the US, Amazon may still be cheaper when you factor in shipping and exchange rates.

Posted by: Mike Shulman on October 11, 2017 11:35 PM | Permalink | Reply to this

Re: A Synthetic Approach to Higher Equalities

$MathML-enabled post (click for more details).$

David Roberts compiled a list of chapters available online as preprints and arrived at

Awodey, Cockett-Seely, Coecke-Kissinger, Corfield, Halvorson-Tsementzis, Lambek, Shulman, Spivak, Weatherall

Posted by: David Corfield on October 13, 2017 8:21 AM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

April 24, 2015