Whitehead's principle about book HOT 15 CLOSED

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

from book.

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.

from book.

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).

from book.

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 [email protected]:

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//issues/28#issuecomment-15429845
.

from book.

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 <[email protected]

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 [email protected]:

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//issues/28#issuecomment-15429957
.

from book.

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.

from book.

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:
#28 (comment)

from book.

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
<[email protected]

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
[email protected]:

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//issues/28#issuecomment-15429957
.

---

Reply to this email directly or view it on GitHub:
#28 (comment)

from book.

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 [email protected] 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
<[email protected]

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
[email protected]:

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//issues/28#issuecomment-15429957

.

---

Reply to this email directly or view it on GitHub:
#28 (comment)

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

from book.

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" [email protected]
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 [email protected]:

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//issues/28#issuecomment-15429957
.

from book.

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 <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Monday, 25 March 2013 18:50
To: HoTT/book <[email protected]mailto:[email protected]>
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" <[email protected]mailto:[email protected]>
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 <[email protected]mailto:[email protected]>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//issues/28#issuecomment-15429957
.

—
Reply to this email directly or view it on GitHubhttps://github.com//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.

from book.

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 <
[email protected]> wrote:

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

from book.

Thank you.

From: "Daniel R. Grayson" <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Tuesday, 26 March 2013 09:57
To: HoTT/book <[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]>
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 <
[email protected]:[email protected]> 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//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.

from book.

I reworked the wording a bit, see 8fae4dc

from book.

Looks good to me! Closing...

from book.