and/or vs smash/wedge about book

[txa]

I have just written the section on propositions as types where I avoided using the logical symbols. Mainly because I didn't want to introduce another layer between the informal presentation and formal proof objects in type theory. But the fact that \wedge and \vee are used in homotopy theory adds another reason.

From: Mike Shulman <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Thursday, 28 March 2013 16:35
To: HoTT/book <[email protected]mailto:[email protected]>
Subject: [book] and/or vs smash/wedge (#48)

The traditional logical notation \land and \lor clashes with the traditional homotopy-theoretic notation for smash products and wedges. Is this irredeemable? What if we just wrote out the words "and" and "or"?

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/48.

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.

[awodey]

your section on PAT is very nice!

Steve

On Mar 28, 2013, at 7:27 PM, Thorsten Altenkirch [email protected] wrote:

I have just written the section on propositions as types where I avoided using the logical symbols. Mainly because I didn't want to introduce another layer between the informal presentation and formal proof objects in type theory. But the fact that \wedge and \vee are used in homotopy theory adds another reason.

From: Mike Shulman <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Thursday, 28 March 2013 16:35
To: HoTT/book <[email protected]mailto:[email protected]>
Subject: [book] and/or vs smash/wedge (#48)

The traditional logical notation \land and \lor clashes with the traditional homotopy-theoretic notation for smash products and wedges. Is this irredeemable? What if we just wrote out the words "and" and "or"?

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/48.

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.

[mikeshulman]

I realized that technically, there is no conflict, if we apply the logical
symbols only to hprops, since the smash and wedge apply only to pointed
types. The only pointed hprop is 1, and we have 1 /\ 1 =1 and 1 / 1 = 1
for both meanings of /\ and /. So the notation is never ambiguous. (-:
On Mar 28, 2013 7:27 PM, "Thorsten Altenkirch" [email protected]
wrote:

I have just written the section on propositions as types where I avoided
using the logical symbols. Mainly because I didn't want to introduce
another layer between the informal presentation and formal proof objects in
type theory. But the fact that \wedge and \vee are used in homotopy theory
adds another reason.

From: Mike Shulman <[email protected]<mailto:
[email protected]>>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>

Date: Thursday, 28 March 2013 16:35
To: HoTT/book <[email protected]mailto:[email protected]>
Subject: [book] and/or vs smash/wedge (#48)

The traditional logical notation \land and \lor clashes with the
traditional homotopy-theoretic notation for smash products and wedges. Is
this irredeemable? What if we just wrote out the words "and" and "or"?

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/48>.

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 GitHubhttps://github.com//issues/48#issuecomment-15621474
.

[andrejbauer]

When we introduce the logical notation, we can make a remark that it possibly clashes with the homotopy-theoretic ones, but we're never going to use both of them at the same time. The logical notation is useful for chapters 9 and 10.