Chapter 1: "recursor" or "eliminator"?

[awodey]

both terms occur often -- the former more often. shall we even try to be consistent?

[awodey]

but then we also need to say that we're using both terms interchangeably, because as it is now, the reader learns the term "recursor" where the type is introduced, and is then later confronted with the undefined term "eliminator" and is expected to know it's the same thing.

[mikeshulman]

In the version I'm looking at, the first occurence of the word "eliminator" is in the sentence "The term ``eliminator" is often used as well" immediately after introduction of the recursor.

On Fri, Apr 26, 2013 at 4:27 PM, Steve Awodey notifications@github.comwrote:

but then we also need to say that we're using both terms interchangeably, because as it is now, the reader learns the term "recursor" where the type is introduced, and is then later confronted with the undefined term "eliminator" and is expected to know it's the same thing.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/145#issuecomment-17100895 .

[RobertHarper]

a recursor for an inductive type is an eliminator, but the terms are not synonymous.

bob

On Apr 26, 2013, at 5:29 PM, Mike Shulman wrote:

In the version I'm looking at, the first occurence of the word "eliminator" is in the sentence "The term ``eliminator" is often used as well" immediately after introduction of the recursor.

On Fri, Apr 26, 2013 at 4:27 PM, Steve Awodey notifications@github.comwrote:

but then we also need to say that we're using both terms interchangeably, because as it is now, the reader learns the term "recursor" where the type is introduced, and is then later confronted with the undefined term "eliminator" and is expected to know it's the same thing.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/145#issuecomment-17100895 .

— Reply to this email directly or view it on GitHub.

[mikeshulman]

Application of a function is an elimination rule, but is it also called an eliminatOR?

On Fri, Apr 26, 2013 at 4:30 PM, Robert Harper notifications@github.comwrote:

a recursor for an inductive type is an eliminator, but the terms are not synonymous.

bob

On Apr 26, 2013, at 5:29 PM, Mike Shulman wrote:

In the version I'm looking at, the first occurence of the word "eliminator" is in the sentence "The term ``eliminator" is often used as well" immediately after introduction of the recursor.

On Fri, Apr 26, 2013 at 4:27 PM, Steve Awodey notifications@github.comwrote:

but then we also need to say that we're using both terms interchangeably, because as it is now, the reader learns the term "recursor" where the type is introduced, and is then later confronted with the undefined term "eliminator" and is expected to know it's the same thing.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/145#issuecomment-17100895> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/145#issuecomment-17100995 .

[RobertHarper]

yes, it's a function eliminator.

bob

On Apr 26, 2013, at 5:31 PM, Mike Shulman wrote:

Application of a function is an elimination rule, but is it also called an eliminatOR?

On Fri, Apr 26, 2013 at 4:30 PM, Robert Harper notifications@github.comwrote:

a recursor for an inductive type is an eliminator, but the terms are not synonymous.

bob

On Apr 26, 2013, at 5:29 PM, Mike Shulman wrote:

In the version I'm looking at, the first occurence of the word "eliminator" is in the sentence "The term ``eliminator" is often used as well" immediately after introduction of the recursor.

On Fri, Apr 26, 2013 at 4:27 PM, Steve Awodey notifications@github.comwrote:

but then we also need to say that we're using both terms interchangeably, because as it is now, the reader learns the term "recursor" where the type is introduced, and is then later confronted with the undefined term "eliminator" and is expected to know it's the same thing.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/145#issuecomment-17100895> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/145#issuecomment-17100995 .

— Reply to this email directly or view it on GitHub.

[mikeshulman]

Okay, interesting. Would it be enough to mention that in the Notes?

On Fri, Apr 26, 2013 at 4:34 PM, Robert Harper notifications@github.comwrote:

yes, it's a function eliminator.

bob

On Apr 26, 2013, at 5:31 PM, Mike Shulman wrote:

Application of a function is an elimination rule, but is it also called an eliminatOR?

On Fri, Apr 26, 2013 at 4:30 PM, Robert Harper notifications@github.comwrote:

a recursor for an inductive type is an eliminator, but the terms are not synonymous.

bob

On Apr 26, 2013, at 5:29 PM, Mike Shulman wrote:

In the version I'm looking at, the first occurence of the word "eliminator" is in the sentence "The term ``eliminator" is often used as well" immediately after introduction of the recursor.

On Fri, Apr 26, 2013 at 4:27 PM, Steve Awodey < notifications@github.com>wrote:

but then we also need to say that we're using both terms interchangeably, because as it is now, the reader learns the term "recursor" where the type is introduced, and is then later confronted with the undefined term "eliminator" and is expected to know it's the same thing.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/145#issuecomment-17100895> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/145#issuecomment-17100995> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/145#issuecomment-17101371 .

[RobertHarper]

sure

On Apr 26, 2013, at 5:36 PM, Mike Shulman wrote:

Okay, interesting. Would it be enough to mention that in the Notes?

On Fri, Apr 26, 2013 at 4:34 PM, Robert Harper notifications@github.comwrote:

yes, it's a function eliminator.

bob

On Apr 26, 2013, at 5:31 PM, Mike Shulman wrote:

Application of a function is an elimination rule, but is it also called an eliminatOR?

On Fri, Apr 26, 2013 at 4:30 PM, Robert Harper notifications@github.comwrote:

a recursor for an inductive type is an eliminator, but the terms are not synonymous.

bob

On Apr 26, 2013, at 5:29 PM, Mike Shulman wrote:

In the version I'm looking at, the first occurence of the word "eliminator" is in the sentence "The term ``eliminator" is often used as well" immediately after introduction of the recursor.

On Fri, Apr 26, 2013 at 4:27 PM, Steve Awodey < notifications@github.com>wrote:

but then we also need to say that we're using both terms interchangeably, because as it is now, the reader learns the term "recursor" where the type is introduced, and is then later confronted with the undefined term "eliminator" and is expected to know it's the same thing.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/145#issuecomment-17100895> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/145#issuecomment-17100995> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/145#issuecomment-17101371 .

— Reply to this email directly or view it on GitHub.

[awodey]

I don't think this level of terminological detail is important enough to discuss (in the book, that is). this is supposed to be informal type theory. Let's just find some terminology that's not too technical and stick with it.

we could just call all these things different "canonical functions" -- the difference between eliminators, recursors, inductors, is not important here. what is important is that we don't throw around a buch of undefined jargon.

On Apr 26, 2013, at 11:36 PM, Mike Shulman notifications@github.com wrote:

Okay, interesting. Would it be enough to mention that in the Notes?

On Fri, Apr 26, 2013 at 4:34 PM, Robert Harper notifications@github.comwrote:

yes, it's a function eliminator.

bob

On Apr 26, 2013, at 5:31 PM, Mike Shulman wrote:

Application of a function is an elimination rule, but is it also called an eliminatOR?

On Fri, Apr 26, 2013 at 4:30 PM, Robert Harper notifications@github.comwrote:

a recursor for an inductive type is an eliminator, but the terms are not synonymous.

bob

On Apr 26, 2013, at 5:29 PM, Mike Shulman wrote:

In the version I'm looking at, the first occurence of the word "eliminator" is in the sentence "The term ``eliminator" is often used as well" immediately after introduction of the recursor.

On Fri, Apr 26, 2013 at 4:27 PM, Steve Awodey < notifications@github.com>wrote:

but then we also need to say that we're using both terms interchangeably, because as it is now, the reader learns the term "recursor" where the type is introduced, and is then later confronted with the undefined term "eliminator" and is expected to know it's the same thing.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/145#issuecomment-17100895> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/145#issuecomment-17100995> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/145#issuecomment-17101371 .

— Reply to this email directly or view it on GitHub.

[andrejbauer]

Any issue that has this much discussion obviously needs to be talked about some more.

[RobertHarper]

informal or formal, there is no reason to alter the standard type-theoretic terminology for a type-theoretic concept. eliminators are eliminators, they are not canonical functions, nor are they always recursors.

thorsten's earlier remark applies here in spades. honestly, it is quite annoying that all things from math are just dandy, but anything from cs must be ruled out of court and renamed.

bob

On Apr 26, 2013, at 5:42 PM, Steve Awodey wrote:

I don't think this level of terminological detail is important enough to discuss (in the book, that is). this is supposed to be informal type theory. Let's just find some terminology that's not too technical and stick with it.

we could just call all these things different "canonical functions" -- the difference between eliminators, recursors, inductors, is not important here. what is important is that we don't throw around a buch of undefined jargon.

On Apr 26, 2013, at 11:36 PM, Mike Shulman notifications@github.com wrote:

Okay, interesting. Would it be enough to mention that in the Notes?

On Fri, Apr 26, 2013 at 4:34 PM, Robert Harper notifications@github.comwrote:

yes, it's a function eliminator.

bob

On Apr 26, 2013, at 5:31 PM, Mike Shulman wrote:

Application of a function is an elimination rule, but is it also called an eliminatOR?

On Fri, Apr 26, 2013 at 4:30 PM, Robert Harper notifications@github.comwrote:

a recursor for an inductive type is an eliminator, but the terms are not synonymous.

bob

On Apr 26, 2013, at 5:29 PM, Mike Shulman wrote:

In the version I'm looking at, the first occurence of the word "eliminator" is in the sentence "The term ``eliminator" is often used as well" immediately after introduction of the recursor.

On Fri, Apr 26, 2013 at 4:27 PM, Steve Awodey < notifications@github.com>wrote:

but then we also need to say that we're using both terms interchangeably, because as it is now, the reader learns the term "recursor" where the type is introduced, and is then later confronted with the undefined term "eliminator" and is expected to know it's the same thing.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/145#issuecomment-17100895> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/145#issuecomment-17100995> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/145#issuecomment-17101371 .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub.

[awodey]

On Apr 27, 2013, at 12:05 AM, Robert Harper notifications@github.com wrote:

informal or formal, there is no reason to alter the standard type-theoretic terminology for a type-theoretic concept. eliminators are eliminators, they are not canonical functions, nor are they always recursors.

I think there are very good reasons to alter some standard type theoretic terminology that was introduced for specific, formal purposes, but is out of place in a book that specifically sets out to do things more informally. With all due respect, Bob, many of your comments, and in particular your growing irritation, suggest to me that you may have missed the point of this book, which is not to be a presentation of standard type theory, but an attempt to develop a new kind of informal type theory that can be read and understood by ordinary mathematicians. Ordinary mathematicians do not care about the difference between recursors and eliminators -- it's just confusing jargon to them. You may think they should care, but that's not the purpose of this book.

[RobertHarper]

It may be your opinion that the audience is for mathematicians, but it is not my opinion. The vastly larger, and for me more important, audience is for computer scientists.

In any case the entire project is about the interactions between CS and HT, from which some interesting things have clearly emerged. It is exceedingly unfair, to the point of insult, to attempt to erase the CS connections by renaming every single CS concept to something bizarre, solely because it's a CS concept. It's just too damned bad if some mathematicians are going to have to get used to a different terminology. A helluva lot more computer scientists are going to have to get used to a helluva lot more terminology and concepts from HT in order to appreciate any of this.

The fact is that the CS perspective, in particular the emphasis on computation, is what made the difference here. It's the CS perspective that emphasizes inductive definitions and the use of abstract types --- to define paths, for example, inductively, rather than by some encoding as sets of points. And so forth. It is completely unfair to attempt to obscure this fact, or even to go so far as to deny the central importance of computation in the entire endeavor (the constructive perspective is one of computation, starting with Brouwer.)

Repeatedly, every single CS concept is contested as something that has to be stamped out. We can't use a turnstile, for example, where that is the standard notation in CS. Nor can we, heaven forbid, call a singleton type a singleton type. Instead we have to call an eliminator (aka elimination form) a "canonical function", a totally non-descrptive term which is, of course, not "jargon", because only CS terms are "jargon". Phrases like "canonical function" or "based path space" aren't jargon of course, they are plain English that any moron at the bus stop knows.

On Apr 26, 2013, at 6:23 PM, Steve Awodey wrote:

On Apr 27, 2013, at 12:05 AM, Robert Harper notifications@github.com wrote:

informal or formal, there is no reason to alter the standard type-theoretic terminology for a type-theoretic concept. eliminators are eliminators, they are not canonical functions, nor are they always recursors.

I think there are very good reasons to alter some standard type theoretic terminology that was introduced for specific, formal purposes, but is out of place in a book that specifically sets out to do things more informally. With all due respect, Bob, many of your comments, and in particular your growing irritation, suggest to me that you may have missed the point of this book, which is not to be a presentation of standard type theory, but an attempt to develop a new kind of informal type theory that can be read and understood by ordinary mathematicians. Ordinary mathematicians do not care about the difference between recursors and eliminators -- it's just confusing jargon to them. You may think they should care, but that's not the purpose of this book. — Reply to this email directly or view it on GitHub.

[mikeshulman]

Let's calm down a bit here. I guess it may seem like the mathematicians are maliciously trying to excise the CS perspective, but please remember that that isn't our goal. We really do appreciate and value the essential contributions coming from the CS side. What we're coming from is real experience trying to teach mathematicians about type theory (and learn about it ourselves) which foundered on notation and jargon that feels overwhelming and impenetrable.

I think the cause of this is not just the fact that everyone has to learn new language when they learn a new subject. In addition, it's that mathematics and computer science have different overall cultural expectations about what kind of notation and jargon is acceptable. A mathematician learning a new kind of mathematics has certain expectations about the way things will be explained and the sort of notation that will be used, which are violated when he/she comes to read about type theory. Cf. earlier discussion about parentheses; turnstyles and horizontal bars are even worse. Certainly, a mathematician who wants to seriously do type theory will eventually have to learn the notation and jargon used by type theorists, but that shouldn't be necessary for a mathematician who only wants to understand type theory informally and perhaps use it as a foundation for mathematics.

Of course, type theorists certainly have the opposite problem when coming to the mathematics; that's why we're including things like the introduction to homotopy theory that Dan L wrote. The whole thing is a balancing act, trying to make the book accessible to some readers without turning off others. Maybe we're right or wrong here or there about what's acceptable, but let's try to maintain the spirit of collaboration and work towards a common goal.

[mikeshulman]

(To clarify: by "even worse" I didn't mean "bad" in any objective sense -- just harder for a mathematician to accept and get used to.)

[mikeshulman]

To return to concrete things, I added a paragraph to the notes to Chapter 1 which mentions that all type formers come with introduction rules and elimination rules, and that the latter include both induction (for inductive types) and application (for function types). Whoever is not happy with the current state of the chapter as regards this terminology, could you please say specifically what you would like to add or remove?

[awodey]

there is still an important open point of misunderstanding here, which seems to be the root of a lot of tension, and that is the intent and purpose of this book. It's not just my opinion that the project here is to develop an informal style of doing type theory that breaks with tradition, and so is not bound by standard notation and conventions: that is what this whole thing is about. It's not a question of how big the math or cs readership will be that determines who we are writing for -- it's what we all agreed that we were doing here. As Andrej already said, that is the answer to your question "why does math terminology always get preferred over cs terminology". It's because we're essentially writing a math book, in the sense that we do things informally. Choices were made in the beginning, and that was the choice that was made.

[awodey]

there seems to be a real misunderstanding here: I / we are not by any means trying to belittle the cs perspective or contribution to the overall project -- we're just discussing how things should be done in the book here. The book is a limited project with specific goals and style that were agreed on way back, in the very beginning, which can be summarized as "no turnstyles", but which was discussed at length and laid down. I suspect that you missed this decision at some point, and have been misinterpreting the application of these guidelines as hostility toward your point of view. If you don't like the idea of this book, you should write a survey just from the CS perspective -- that would be very useful. But it would be more helpful to this book project if you would recognize the ground rules rather than constantly taking offense and questioning the validity of the project.

On Apr 27, 2013, at 12:49 AM, Robert Harper notifications@github.com wrote:

It may be your opinion that the audience is for mathematicians, but it is not my opinion. The vastly larger, and for me more important, audience is for computer scientists.

In any case the entire project is about the interactions between CS and HT, from which some interesting things have clearly emerged. It is exceedingly unfair, to the point of insult, to attempt to erase the CS connections by renaming every single CS concept to something bizarre, solely because it's a CS concept. It's just too damned bad if some mathematicians are going to have to get used to a different terminology. A helluva lot more computer scientists are going to have to get used to a helluva lot more terminology and concepts from HT in order to appreciate any of this.

The fact is that the CS perspective, in particular the emphasis on computation, is what made the difference here. It's the CS perspective that emphasizes inductive definitions and the use of abstract types --- to define paths, for example, inductively, rather than by some encoding as sets of points. And so forth. It is completely unfair to attempt to obscure this fact, or even to go so far as to deny the central importance of computation in the entire endeavor (the constructive perspective is one of computation, starting with Brouwer.)

Repeatedly, every single CS concept is contested as something that has to be stamped out. We can't use a turnstile, for example, where that is the standard notation in CS. Nor can we, heaven forbid, call a singleton type a singleton type. Instead we have to call an eliminator (aka elimination form) a "canonical function", a totally non-descrptive term which is, of course, not "jargon", because only CS terms are "jargon". Phrases like "canonical function" or "based path space" aren't jargon of course, they are plain English that any moron at the bus stop knows.

On Apr 26, 2013, at 6:23 PM, Steve Awodey wrote:

On Apr 27, 2013, at 12:05 AM, Robert Harper notifications@github.com wrote:

informal or formal, there is no reason to alter the standard type-theoretic terminology for a type-theoretic concept. eliminators are eliminators, they are not canonical functions, nor are they always recursors.

I think there are very good reasons to alter some standard type theoretic terminology that was introduced for specific, formal purposes, but is out of place in a book that specifically sets out to do things more informally. With all due respect, Bob, many of your comments, and in particular your growing irritation, suggest to me that you may have missed the point of this book, which is not to be a presentation of standard type theory, but an attempt to develop a new kind of informal type theory that can be read and understood by ordinary mathematicians. Ordinary mathematicians do not care about the difference between recursors and eliminators -- it's just confusing jargon to them. You may think they should care, but that's not the purpose of this book. — Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub.

[dlicata335]

To me, this book is mostly an act of pedagogy, and so the questions I would ask are "who are we teaching?" and "what do we want them to learn?". I think that people who don't know type theory, but do know some math, can learn about the use of type theory as a foundation of math from this book. Hopefully our examples in part II are compelling enough that they become convinced that it is a better foundation than what they are used to. I think that people who do know type theory, but don't know the math we do in part II, can learn how some rather high-powered math can be carried out in type theory from this book. Everyone can learn the basic definitions of HoTT from the first 200 pages. There are lots of other interesting aspects of homotopy type theory that we're not teaching in this book (e.g. how the math impacts programming), but that's okay with me: we can write other books on that, and I think that teaching these things to these audiences is important.

Both the math and the type theory are big rich deep subjects with long histories. To use the iceberg metaphor, almost all of both of them are going to be underwater here. In terms of the above pedagogical goals, it makes sense to me to do this, and to streamline, streamline, streamline until we get them down to the essential bits necessary in order to teach what we want to teach. The people coming from one background or the other will be able to read in the part that's below water. And the people who don't have one background or the other will have an easier path through the material, and get hooked on it, and then we draw back the curtain. I feel like we're doing a pretty good job at finding a smooth path through the material. There's a lot we're not saying, from both the math and the type theory perspective, but I think that's okay to teach what I, at least, want the book to teach.

[cangiuli]

Steve, you're absolutely right that the book is an attempt to develop an informal style of doing mathematics inside type theory, and as such, it makes sense to break from type-theoretic tradition. But in these arguments it often ends up being repeated that the book's readership is "ordinary mathematicians", which doesn't follow. For example, there are 41 people besides us starring this repository on Github; from a cursory glance, essentially all of them are computer scientists and/or functional programmers, who apparently care enough about the book to put up with a deluge of notifications.

This is a math book, so tangents about how to program better with HoTT, for example, are out of bounds. But often it seems like we adopt the position that we ought not mention something in passing which would help computer scientists (but not mathematicians), on the basis that it would confuse our True Readership of mathematicians. We can't be everything to everyone, but it's worth remembering that large portions of our readership are already familiar with things like "the Paulin-Mohring identity type" (as an example; I am not trying to reopen this specific argument) and would be helped by the presence of these familiar names, alongside standard mathematical ones.

I do appreciate the fact that reducing new terminology will make HoTT more palatable to mathematicians, but we're bringing genuinely new ideas and methodologies to the table---as we saw when trying to translate encode-decode proofs into categorical language---so it would be weird for a reader to be put off by the fact that type theorists have parallel terminology which they are free to completely ignore.

[awodey]

very well-put, dan. I agree with everything you say.

On Apr 27, 2013, at 7:20 AM, Dan Licata notifications@github.com wrote:

To me, this book is mostly an act of pedagogy, and so the questions I would ask are "who are we teaching?" and "what do we want them to learn?". I think that people who don't know type theory, but do know some math, can learn about the use of type theory as a foundation of math from this book. Hopefully our examples in part II are compelling enough that they become convinced that it is a better foundation than what they are used to. I think that people who do know type theory, but don't know the math we do in part II, can learn how some rather high-powered math can be carried out in type theory from this book. There are lots of other interesting aspects of homotopy type theory that we're not teaching in this book (e.g. how the math impacts programming), but that's okay with me: we can write other books on that, and I think that teaching these things to these audiences is important.

Both the math and the type theory are big rich deep subjects with long histories. To use the iceberg metaphor, almost all of both of them are going to be underwater here. In terms of the above pedagogical goals, it makes sense to me to do this, and to streamline, streamline, streamline until we get them down to the essential bits necessary in order to teach what we want to teach. The people coming from one background or the other will be able to read in the part that's below water. And the people who don't have one background or the other will have an easier path through the material, and get hooked on it, and then we draw back the curtain. I feel like we're doing a pretty good job at finding a smooth path through the material. There's a lot we're not saying, from both the math and the type theory perspective, but I think that's okay to teach what we want to teach.

— Reply to this email directly or view it on GitHub.

[awodey]

I'm not so sure that I agree with the point about it being useful to always mention the type-theoretic terminology in addition to the mathematical (or even to prefer the former over the latter, where it's very entrenched), so that the type theory reader will feel more comfortable. the problem is that it loads down the exposition to double up all the terminology (or more, since the type theory world is also not monolithic: see Paulin-Mohring vs. singleton type). The mathematical reader may be free to ignore the proliferation of terminology, but still will not be able to see the forest through all the trees.

I think a good compromise is to pick one (mathematical) terminology and use that for the main exposition, and then mention the various relevant type-theoretic alternatives along with relevant, related literature in the notes. That gives the type-theorist a point of reference and comparison, without cluttering up the main text with constant asides like "or, as it's also called ..." and "also referred to as …".

But my main point is still that the book is simply not intended as a compromise between math and CS points of view -- and the math people are being mean by not giving CS its due -- but rather an explicit exercise in Foundations of MATH from a mathematical perspective, where the formal type theory has been consciously relegated to the notes and appendices -- not because we don't think it's of value (it clearly is of great value!) but because one can't do everything in one place, and that's what we've decided to do in this particular book project.

Maybe next we'll write a book on Univalent Foundations of Computation -- that would be awesome!

On Apr 27, 2013, at 8:30 AM, Carlo Angiuli notifications@github.com wrote:

Steve, you're absolutely right that the book is an attempt to develop an informal style of doing mathematics inside type theory, and as such, it makes sense to break from type-theoretic tradition. But in these arguments it often ends up being repeated that the book's readership is "ordinary mathematicians", which doesn't follow. For example, there are 41 people besides us starring this repository on Github; from a cursory glance, essentially all of them are computer scientists and/or functional programmers, who apparently care enough about the book to put up with a deluge of notifications.

This is a math book, so tangents about how to program better with HoTT, for example, are out of bounds. But often it seems like we adopt the position that we ought not mention something in passing which would help computer scientists (but not mathematicians), on the basis that it would confuse our True Readership of mathematicians. We can't be everything to everyone, but it's worth remembering that large portions of our readership are already familiar with things like "the Paulin-Mohring identity type" (as an example; I am not trying to reopen this specific argument) and would be helped by the presence of these familiar names, alongside standard mathematical ones.

I do appreciate the fact that reducing new terminology will make HoTT more palatable to mathematicians, but we're bringing genuinely new ideas and methodologies to the table---as we saw when trying to translate encode-decode proofs into categorical language---so it would be weird for a reader to be put off by the fact that type theorists have parallel terminology which they are free to completely ignore.

— Reply to this email directly or view it on GitHub.