Whitehead's principle

[DanGrayson]

"From a foundational point of view, therefore, we may speak of Whitehead’s principle as a “classicality axiom”, akin to LEM and AC....Thus, by showing us a world of mathematics where ∞-groupoids are basic objects, univalent foundations reveals new axioms that have heretofore been implicitly assumed without realizing it, solely due to the nature of our chosen foundational system."

I like the ideas in the paragraph containing the sentences above, and have two remarks:

(1) Is there anything more "fundamental" that would serve as an axiom implying Whitehead's principle?

(2) The phrase "axioms that have heretofore been implicitly assumed without realizing it" will sound a bit fishy to mathematicians who think of Whitehead's Principle as a theorem of classical mathematics, with its own complete proof, not implicitly "assuming" anything. It will also sound a bit fishy to mathematicians who dread the prospect of adding a new axiom to the system in every chapter to cover yet another classical theorem whose proof doesn't quite fit into the new framework. A slight shift of emphasis in the phrasing would perhaps go over better.

[mikeshulman]

If you have any suggestions, I'd love to hear them.

[DanGrayson]

Perhaps something like:

Thus, as we work to formalize classical mathematics based on univalent foundations in a world of mathematics where $\infty$-groupoids are basic objects, important classical results are revealed as prominent new axioms.

[EgbertRijke]

Shouldn't we approach whiteheads theorem as a feature rather than as an axiom? Just like when we work with sets we don't assume that UIP holds for all types (being a set is a feature), when we want to consider consequences of Whiteheads theorem we can just consider those types which are the limit of their own truncations (this describes a modality).

[DanGrayson]

That would be true if you wanted to study types where Whitehead's Principle fails, and had some alternative useful axiom that would produce such types. I doubt we're in that situation.

On Mon, Mar 25, 2013 at 6:29 PM, EgbertRijke notifications@github.comwrote:

Shouldn't we approach whiteheads theorem as a feature rather than as an axiom? Just like when we work with sets we don't assume that UIP holds for all types (being a set is a feature), when we want to consider consequences of Whiteheads theorem we can just consider those types which are the limit of their own truncations (this describes a modality).

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

[spitters]

I don't think we want to explicitly restrict ourselves to hypercomplete toposes.

On Mon, Mar 25, 2013 at 6:31 PM, Daniel R. Grayson <notifications@github.com

wrote:

That would be true if you wanted to study types where Whitehead's Principle fails, and had some alternative useful axiom that would produce such types. I doubt we're in that situation.

On Mon, Mar 25, 2013 at 6:29 PM, EgbertRijke notifications@github.comwrote:

Shouldn't we approach whiteheads theorem as a feature rather than as an axiom? Just like when we work with sets we don't assume that UIP holds for all types (being a set is a feature), when we want to consider consequences of Whiteheads theorem we can just consider those types which are the limit of their own truncations (this describes a modality).

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

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

[EgbertRijke]

I'm not sure if I agree with Dan. I was trying to suggest that can study Whitehead's principle without assuming that it holds for all types in the same way as we study sets without assuming UIP for all types.

[awodey]

I would say "condition" rather than axiom. some types have the "Whitehead property" of being fully determined by their pi_n's, others not.

steve

Perhaps something like:

Thus, as we work to formalize classical mathematics based on univalent foundations in a world of mathematics where $\infty$-groupoids are basic objects, important classical results are revealed as prominent new axioms.

---

Reply to this email directly or view it on GitHub: https://github.com/HoTT/book/issues/28#issuecomment-15429477

[awodey]

I don't think we want to explicitly restrict ourselves to hypercomplete toposes.

definition please.

On Mon, Mar 25, 2013 at 6:31 PM, Daniel R. Grayson <notifications@github.com

wrote:

That would be true if you wanted to study types where Whitehead's Principle fails, and had some alternative useful axiom that would produce such types. I doubt we're in that situation.

On Mon, Mar 25, 2013 at 6:29 PM, EgbertRijke notifications@github.comwrote:

Shouldn't we approach whiteheads theorem as a feature rather than as an axiom? Just like when we work with sets we don't assume that UIP holds for all types (being a set is a feature), when we want to consider consequences of Whiteheads theorem we can just consider those types which are the limit of their own truncations (this describes a modality).

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

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

---

Reply to this email directly or view it on GitHub: https://github.com/HoTT/book/issues/28#issuecomment-15430310

[spitters]

http://ncatlab.org/nlab/show/hypercomplete+%28infinity,1%29-topos An (∞,1)-topos is hypercomplete if the Whitehead theorem is valid in it.

On Mon, Mar 25, 2013 at 7:15 PM, Steve Awodey notifications@github.com wrote:

I don't think we want to explicitly restrict ourselves to hypercomplete toposes.

definition please.

On Mon, Mar 25, 2013 at 6:31 PM, Daniel R. Grayson <notifications@github.com

wrote:

That would be true if you wanted to study types where Whitehead's Principle fails, and had some alternative useful axiom that would produce such types. I doubt we're in that situation.

On Mon, Mar 25, 2013 at 6:29 PM, EgbertRijke notifications@github.comwrote:

Shouldn't we approach whiteheads theorem as a feature rather than as an axiom? Just like when we work with sets we don't assume that UIP holds for all types (being a set is a feature), when we want to consider consequences of Whiteheads theorem we can just consider those types which are the limit of their own truncations (this describes a modality).

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

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

.

---

Reply to this email directly or view it on GitHub: https://github.com/HoTT/book/issues/28#issuecomment-15430310

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

[mikeshulman]

It's not at all clear to me that S^2, for instance, satisfies Whitehead's principle. I rather suspect that it doesn't (at least, not without assuming it as an axiom). Types that provably satisfy Whitehead's theorem might be rather thin on the ground (except for those of finite h-level).

(By the way, being the limit of its truncations is actually a different property than satisfying Whitehead's principle.) On Mar 25, 2013 6:31 PM, "Daniel R. Grayson" notifications@github.com wrote:

That would be true if you wanted to study types where Whitehead's Principle fails, and had some alternative useful axiom that would produce such types. I doubt we're in that situation.

On Mon, Mar 25, 2013 at 6:29 PM, EgbertRijke notifications@github.comwrote:

Shouldn't we approach whiteheads theorem as a feature rather than as an axiom? Just like when we work with sets we don't assume that UIP holds for all types (being a set is a feature), when we want to consider consequences of Whiteheads theorem we can just consider those types which are the limit of their own truncations (this describes a modality).

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

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

[txa]

WHat exactly is Whitehead's principle? Didn't Dan prove this in Agda (I guess he was using the limit of truncation view) ?

From: Mike Shulman notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Monday, 25 March 2013 18:50 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Subject: Re: [book] Whitehead's principle (#28)

It's not at all clear to me that S^2, for instance, satisfies Whitehead's principle. I rather suspect that it doesn't (at least, not without assuming it as an axiom). Types that provably satisfy Whitehead's theorem might be rather thin on the ground (except for those of finite h-level).

(By the way, being the limit of its truncations is actually a different property than satisfying Whitehead's principle.) On Mar 25, 2013 6:31 PM, "Daniel R. Grayson" notifications@github.com<mailto:notifications@github.com> wrote:

That would be true if you wanted to study types where Whitehead's Principle fails, and had some alternative useful axiom that would produce such types. I doubt we're in that situation.

On Mon, Mar 25, 2013 at 6:29 PM, EgbertRijke notifications@github.com<mailto:notifications@github.com>wrote:

Shouldn't we approach whiteheads theorem as a feature rather than as an axiom? Just like when we work with sets we don't assume that UIP holds for all types (being a set is a feature), when we want to consider consequences of Whiteheads theorem we can just consider those types which are the limit of their own truncations (this describes a modality).

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

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

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

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.

[DanGrayson]

Section 7.6 of the book is about Whitehead's Principle. In Agda, Dan L proved it only under the additional assumption that the type is n-truncated for some n, see https://github.com/dlicata335/hott-agda/blob/master/homotopy/Whitehead.agda.

On Tue, Mar 26, 2013 at 10:48 AM, Thorsten Altenkirch < notifications@github.com> wrote:

WHat exactly is Whitehead's principle? Didn't Dan prove this in Agda (I guess he was using the limit of truncation view) ?

[txa]

Thank you.

From: "Daniel R. Grayson" notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Tuesday, 26 March 2013 09:57 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] Whitehead's principle (#28)

Section 7.6 of the book is about Whitehead's Principle. In Agda, Dan L proved it only under the additional assumption that the type is n-truncated for some n, see https://github.com/dlicata335/hott-agda/blob/master/homotopy/Whitehead.agda.

On Tue, Mar 26, 2013 at 10:48 AM, Thorsten Altenkirch < notifications@github.commailto:notifications@github.com> wrote:

WHat exactly is Whitehead's principle? Didn't Dan prove this in Agda (I guess he was using the limit of truncation view) ?

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

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.

[mikeshulman]

I reworked the wording a bit, see 8fae4dc63b4eb5e

[DanGrayson]

Looks good to me! Closing...