computational disclaimers in Chapter 2

[awodey]

I don't like the reservations about the system expressed at several points in Chapter 2:

the penultimate par. of 2.5, and the remarks immediately following axiom 2.9.3 (FunExt) and 2.10.3 (UA) about how these "could eventually be built into a more computational version of homotopy type theory". This is research ideas bleeding to the statement of the current theory, and it belongs in the notes, or at least moved away from the main development and qualified. We have to simply assert the Univalence Axiom, etc., in the main text, without immediately calling it into question.

[mikeshulman]

I think it's really important not to give the reader the impression that there is a "current theory" in any sense other than "the theory we've chosen to use in writing this book". We've chosen to write the book in more or less the style of an introductory textbook on set theory, but like it or not, we are currently doing research on the foundations, and I think pretending otherwise would do the reader a disservice. For one thing, we don't want them to get confused when the Second Edition changes the underlying type theory!

[awodey]

yes, but the official statement of the Univalence Axiom should not be immediately followed by a disclaimer like "the univalence axiom could eventually be built into a more computational version of homotopy type theory".
That's just one person's research project. I might think that UA is fully in order as it is, or that it should follow from a quotients axiom, or from parametricity, or from some other changes. Such remarks belong in the notes.

On Apr 15, 2013, at 2:30 PM, Mike Shulman notifications@github.com wrote:

I think it's really important not to give the reader the impression that there is a "current theory" in any sense other than "the theory we've chosen to use in writing this book". We've chosen to write the book in more or less the style of an introductory textbook on set theory, but like it or not, we _are_currently doing research on the foundations, and I think pretending otherwise would do the reader a disservice. For one thing, we don't want them to get confused when the Second Edition changes the underlying type theory!

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

[mikeshulman]

On Mon, Apr 15, 2013 at 2:45 PM, Steve Awodey notifications@github.comwrote:

I might think that UA is fully in order as it is, or that it should follow from a quotients axiom, or from parametricity, or from some other changes.

Now I'm curious: do you?

[awodey]

I think that the special role given to "axioms" is overrated -- things can be set up as "axioms" and other things then follow as "theorems" in different ways, depending on the purpose. I think it's very likely that we'll find other principles that imply univalence -- for example, if we had a good notion of oo-groupoid and could make quotients, we could quotient a universe by equivalence to get a univalent one. That would be just as interesting as a "more computational version of type theory", in my opinion. Or how about a general notion of "cocompleteness" which implies oo-groupoid quotients -- that would be another interesting "axiom".

On Apr 15, 2013, at 2:50 PM, Mike Shulman notifications@github.com wrote:

On Mon, Apr 15, 2013 at 2:45 PM, Steve Awodey notifications@github.comwrote:

I might think that UA is fully in order as it is, or that it should follow from a quotients axiom, or from parametricity, or from some other changes.

Now I'm curious: do you? — Reply to this email directly or view it on GitHub.

[mikeshulman]

How about this: 43485f2 ?

[txa]

I don't mind to put this discussion in the notes and I agree that it shouldn't be were it is.

However, there is a fundamental difference to type-theoretic principles which can be justified by some normalisation argument and "axioms" which don't really belong into type theory. I can accept as a stop-gap measure to do this (and have been doing this for a while), but saying it doesn't matter or one is as good as another does not reflect the idea behind type theory.

Thorsten

[RobertHarper]

i held my tongue, but now that thorsten mentions it, i will simply say that i agree with this point. type theory is not an axiomatic theory in the way that first- or higher-order logic is, precisely because the computational interpretation is the prime characteristic of intuitionistic type theory. it's not just "one person's" favorite problem, in my opinion.

bob

On Apr 15, 2013, at 4:35 PM, Thorsten Altenkirch wrote:

I don't mind to put this discussion in the notes and I agree that it shouldn't be were it is.

However, there is a fundamental difference to type-theoretic principles which can be justified by some normalisation argument and "axioms" which don't really belong into type theory. I can accept as a stop-gap measure to do this (and have been doing this for a while), but saying it doesn't matter or one is as good as another does not reflect the idea behind type theory.

Thorsten

From: Steve Awodey notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Subject: Re: [book] computational disclaimers in Chapter 2 (#126)

I think that the special role given to "axioms" is overrated -- things can be set up as "axioms" and other things then follow as "theorems" in different ways, depending on the purpose. I think it's very likely that we'll find other principles that imply univalence -- for example, if we had a good notion of oo-groupoid and could make quotients, we could quotient a universe by equivalence to get a univalent one. That would be just as interesting as a "more computational version of type theory", in my opinion. Or how about a general notion of "cocompleteness" which implies oo-groupoid quotients -- that would be another interesting "axiom".

On Apr 15, 2013, at 2:50 PM, Mike Shulman notifications@github.com<mailto:notifications@github.com> wrote:

On Mon, Apr 15, 2013 at 2:45 PM, Steve Awodey notifications@github.com<mailto:notifications@github.com>wrote:

I might think that UA is fully in order as it is, or that it should follow from a quotients axiom, or from parametricity, or from some other changes.

Now I'm curious: do you? — 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/126#issuecomment-16404584.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation. — Reply to this email directly or view it on GitHub.

[awodey]

Sent from my iPhone

On Apr 15, 2013, at 4:39 PM, Robert Harper notifications@github.com wrote:

i held my tongue, but now that thorsten mentions it, i will simply say that i agree with this point. type theory is not an axiomatic theory in the way that first- or higher-order logic is, precisely because the computational interpretation is the prime characteristic of intuitionistic type theory. it's not just "one person's" favorite problem, in my opinion.

The categorical description is another point of view. But I'm not claiming that its the main one or something.

bob

On Apr 15, 2013, at 4:35 PM, Thorsten Altenkirch wrote:

I don't mind to put this discussion in the notes and I agree that it shouldn't be were it is.

However, there is a fundamental difference to type-theoretic principles which can be justified by some normalisation argument and "axioms" which don't really belong into type theory. I can accept as a stop-gap measure to do this (and have been doing this for a while), but saying it doesn't matter or one is as good as another does not reflect the idea behind type theory.

Thorsten

From: Steve Awodey notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Subject: Re: [book] computational disclaimers in Chapter 2 (#126)

I think that the special role given to "axioms" is overrated -- things can be set up as "axioms" and other things then follow as "theorems" in different ways, depending on the purpose. I think it's very likely that we'll find other principles that imply univalence -- for example, if we had a good notion of oo-groupoid and could make quotients, we could quotient a universe by equivalence to get a univalent one. That would be just as interesting as a "more computational version of type theory", in my opinion. Or how about a general notion of "cocompleteness" which implies oo-groupoid quotients -- that would be another interesting "axiom".

On Apr 15, 2013, at 2:50 PM, Mike Shulman notifications@github.com<mailto:notifications@github.com> wrote:

On Mon, Apr 15, 2013 at 2:45 PM, Steve Awodey notifications@github.com<mailto:notifications@github.com>wrote:

I might think that UA is fully in order as it is, or that it should follow from a quotients axiom, or from parametricity, or from some other changes.

Now I'm curious: do you? — 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/126#issuecomment-16404584.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation. — Reply to this email directly or view it on GitHub.

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

[mikeshulman]

While I see these points, I also think type theorists may want to entertain the possibility that type theory can have grown beyond its beginnings, or that there is more than one valid viewpoint on it. Personally, I hope we do find a computational interpretation of univalence and HITs, because I want the multiple viewpoints on type theory to remain harmonious as much as possible, and also because it would just be more convenient. But I also think there are lots of other potentially useful principles that we could import into type theory from categorical semantics, e.g. for doing synthetic differential geometry, synthetic quantum field theory, synthetic stable homotopy theory, etc., and it's not reasonable to expect that all of them will have a good computational interpretation. We should be aware of and value the computational perspective, but we shouldn't be bound by it as a straitjacket to say that nothing we add to type theory can be valid unless we eventually find a computational interpretation for it.

[andrejbauer]

Bob and Thorsten, I am a bit confused as to what it is that you are saying. Which of the following comes closest (maybe a convex combination)?

1. You are defending terminology. People are welcome to do whatever they like, and you acknowledge that their way of doing type theory makes sense and is valuable, but if they do not follow the prescribed methodology, then they should not call it "type theory".
2. You are offering advice on how we should do type theory, i.e., you are telling us that it is best, for mathematical reasons, to stick to the methodology you are advocating. So, should someone find a better methodology for doing type theory, you would gladly adopt it, even if that meant leaving behind some of your philosopical convictions.
3. You are establishing a dogma, namely that there is a Correct Way to do type theory, and that we should do it that way, or else we are sinners.

[RobertHarper]

Personally, I'm reacting to the remark that the computational interpretation is just one person's interest. One may say the same about other interpretations as well.

But it is nevertheless true that Int Type Theory has always been a theory of computation within which one may do (constructive) mathematics.

Bob

(sent from handheld)

On Apr 15, 2013, at 18:36, Andrej Bauer notifications@github.com wrote:

Bob and Thorsten, I am a bit confused as to what it is that you are saying. Which of the following comes closest (maye a convex combination)?

You are defending terminology. People are welcome to do whatever they like, and you acknowledge that their way of doing type theory makes sense and is valuable, but if they do not follow the prescribed methodology, then they should not call it "type theory".

You are offering advice on how we should do type theory, i.e., you are telling us that it is best, for mathematical reasons, to stick to the methodology you are advocating. So, should someone find a better methodology for doing type theory, you would gladly adopt it, even if that meant leaving behind some of your philosopical convictions.

You are establishing a dogma, namely that there is a Correct Way to do type theory, and that we should do it that way, or else we are sinners.

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

[awodey]

On Apr 15, 2013, at 7:03 PM, Robert Harper notifications@github.com wrote:

Personally, I'm reacting to the remark that the computational interpretation is just one person's interest. One may say the same about other interpretations as well.

precisely

But it is nevertheless true that Int Type Theory has always been a theory of computation within which one may do (constructive) mathematics.

among other things. the origins of type theory are murky, at best.

the context of the remark is important:

currently, the univalence axiom is officially presented, and in the very same breath it is said that it is defective because of computational issues, etc. I'm just saying that the computational aspect is just one among many, and so that remark doesn't belong there. Of course the issue needs to be discussed somewhere -- I proposed in the notes -- but the current exposition is an awkward 2 steps forward, 1 step back.

Bob

(sent from handheld)

On Apr 15, 2013, at 18:36, Andrej Bauer notifications@github.com wrote:

Bob and Thorsten, I am a bit confused as to what it is that you are saying. Which of the following comes closest (maye a convex combination)?

You are defending terminology. People are welcome to do whatever they like, and you acknowledge that their way of doing type theory makes sense and is valuable, but if they do not follow the prescribed methodology, then they should not call it "type theory".

You are offering advice on how we should do type theory, i.e., you are telling us that it is best, for mathematical reasons, to stick to the methodology you are advocating. So, should someone find a better methodology for doing type theory, you would gladly adopt it, even if that meant leaving behind some of your philosopical convictions.

You are establishing a dogma, namely that there is a Correct Way to do type theory, and that we should do it that way, or else we are sinners.

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

[awodey]

I think it's much better now. thanks,

Steve

On Apr 15, 2013, at 3:42 PM, Mike Shulman notifications@github.com wrote:

How about this: 43485f2 ?

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

[RobertHarper]

(sent from handheld)

On Apr 15, 2013, at 19:19, Steve Awodey notifications@github.com wrote:

On Apr 15, 2013, at 7:03 PM, Robert Harper notifications@github.com wrote:

Personally, I'm reacting to the remark that the computational interpretation is just one person's interest. One may say the same about other interpretations as well.

precisely

I'm merely responding to the dismissal.

But it is nevertheless true that Int Type Theory has always been a theory of computation within which one may do (constructive) mathematics.

among other things. the origins of type theory are murky, at best.

the context of the remark is important:

currently, the univalence axiom is officially presented, and in the very same breath it is said that it is defective because of computational issues, etc. I'm just saying that the computational aspect is just one among many, and so that remark doesn't belong there. Of course the issue needs to be discussed somewhere -- I proposed in the notes -- but the current exposition is an awkward 2 steps forward, 1 step back.

I'm out on my bike, will have a look later.

Bob

(sent from handheld)

On Apr 15, 2013, at 18:36, Andrej Bauer notifications@github.com wrote:

Bob and Thorsten, I am a bit confused as to what it is that you are saying. Which of the following comes closest (maye a convex combination)?

You are defending terminology. People are welcome to do whatever they like, and you acknowledge that their way of doing type theory makes sense and is valuable, but if they do not follow the prescribed methodology, then they should not call it "type theory".

You are offering advice on how we should do type theory, i.e., you are telling us that it is best, for mathematical reasons, to stick to the methodology you are advocating. So, should someone find a better methodology for doing type theory, you would gladly adopt it, even if that meant leaving behind some of your philosopical convictions.

You are establishing a dogma, namely that there is a Correct Way to do type theory, and that we should do it that way, or else we are sinners.

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

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

[awodey]

Mike's revision solves the problem I think.

Sent from my iPhone

On Apr 15, 2013, at 7:29 PM, Robert Harper notifications@github.com wrote:

(sent from handheld)

On Apr 15, 2013, at 19:19, Steve Awodey notifications@github.com wrote:

On Apr 15, 2013, at 7:03 PM, Robert Harper notifications@github.com wrote:

Personally, I'm reacting to the remark that the computational interpretation is just one person's interest. One may say the same about other interpretations as well.

precisely

I'm merely responding to the dismissal.

But it is nevertheless true that Int Type Theory has always been a theory of computation within which one may do (constructive) mathematics.

among other things. the origins of type theory are murky, at best.

the context of the remark is important:

currently, the univalence axiom is officially presented, and in the very same breath it is said that it is defective because of computational issues, etc. I'm just saying that the computational aspect is just one among many, and so that remark doesn't belong there. Of course the issue needs to be discussed somewhere -- I proposed in the notes -- but the current exposition is an awkward 2 steps forward, 1 step back.

I'm out on my bike, will have a look later.

Bob

(sent from handheld)

On Apr 15, 2013, at 18:36, Andrej Bauer notifications@github.com wrote:

Bob and Thorsten, I am a bit confused as to what it is that you are saying. Which of the following comes closest (maye a convex combination)?

You are defending terminology. People are welcome to do whatever they like, and you acknowledge that their way of doing type theory makes sense and is valuable, but if they do not follow the prescribed methodology, then they should not call it "type theory".

You are offering advice on how we should do type theory, i.e., you are telling us that it is best, for mathematical reasons, to stick to the methodology you are advocating. So, should someone find a better methodology for doing type theory, you would gladly adopt it, even if that meant leaving behind some of your philosopical convictions.

You are establishing a dogma, namely that there is a Correct Way to do type theory, and that we should do it that way, or else we are sinners.

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

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

[RobertHarper]

Ok, good, I'll have a look later.

(sent from handheld)

On Apr 15, 2013, at 19:38, Steve Awodey notifications@github.com wrote:

Mike's revision solves the problem I think.

Sent from my iPhone

On Apr 15, 2013, at 7:29 PM, Robert Harper notifications@github.com wrote:

(sent from handheld)

On Apr 15, 2013, at 19:19, Steve Awodey notifications@github.com wrote:

On Apr 15, 2013, at 7:03 PM, Robert Harper notifications@github.com wrote:

Personally, I'm reacting to the remark that the computational interpretation is just one person's interest. One may say the same about other interpretations as well.

precisely

I'm merely responding to the dismissal.

But it is nevertheless true that Int Type Theory has always been a theory of computation within which one may do (constructive) mathematics.

among other things. the origins of type theory are murky, at best.

the context of the remark is important:

currently, the univalence axiom is officially presented, and in the very same breath it is said that it is defective because of computational issues, etc. I'm just saying that the computational aspect is just one among many, and so that remark doesn't belong there. Of course the issue needs to be discussed somewhere -- I proposed in the notes -- but the current exposition is an awkward 2 steps forward, 1 step back.

I'm out on my bike, will have a look later.

Bob

(sent from handheld)

On Apr 15, 2013, at 18:36, Andrej Bauer notifications@github.com wrote:

Bob and Thorsten, I am a bit confused as to what it is that you are saying. Which of the following comes closest (maye a convex combination)?

You are defending terminology. People are welcome to do whatever they like, and you acknowledge that their way of doing type theory makes sense and is valuable, but if they do not follow the prescribed methodology, then they should not call it "type theory".

You are offering advice on how we should do type theory, i.e., you are telling us that it is best, for mathematical reasons, to stick to the methodology you are advocating. So, should someone find a better methodology for doing type theory, you would gladly adopt it, even if that meant leaving behind some of your philosopical convictions.

You are establishing a dogma, namely that there is a Correct Way to do type theory, and that we should do it that way, or else we are sinners.

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

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

[txa]

I think it is to some degree a case of having different backgrounds.

For Mathematicians HoTT is just another, maybe better, way to do Mathematics and the question of computational interpretation is interesting but not essential.

For a computer scientist HoTT is a programming language and having axioms means that you cannot run your code. Hence it is useless but we are prepared to wait for the delivery of that compiler and program in the hope that it will arrive some day (soon).

I think what we were asking for that both of these views are approrpiately represented in the inroduction.

Thorsten

From: Andrej Bauer notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Mon, 15 Apr 2013 23:36:02 +0100 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Cc: Thorsten Altenkirch txa@Cs.Nott.AC.UK<mailto:txa@Cs.Nott.AC.UK> Subject: Re: [book] computational disclaimers in Chapter 2 (#126)

Bob and Thorsten, I am a bit confused as to what it is that you are saying. Which of the following comes closest (maye a convex combination)?

1. You are defending terminology. People are welcome to do whatever they like, and you acknowledge that their way of doing type theory makes sense and is valuable, but if they do not follow the prescribed methodology, then they should not call it "type theory".
2. You are offering advice on how we should do type theory, i.e., you are telling us that it is best, for mathematical reasons, to stick to the methodology you are advocating. So, should someone find a better methodology for doing type theory, you would gladly adopt it, even if that meant leaving behind some of your philosopical convictions.
3. You are establishing a dogma, namely that there is a Correct Way to do type theory, and that we should do it that way, or else we are sinners.

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

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

[andrejbauer]

Right, I think this is a typical case when someone is surprised by an unintended interpretation of his favorite theory.

[mikeshulman]

Can this be closed?

[awodey]

Yes.

Sent from my iPhone

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

Can this be closed?

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