Universes about book

[txa]

I see. Yes, we could introduce the symbol U for a universe of types after function types and before Pi-types when we need to talk about families and move the predicative hierarchy and the discussion to the end of the chapter.

In the section for equality proofs I am now using the "impredicative" but concise construction suggested by Mike. At this point it would be good if one would have introduced the hierarchy, but on the other hand one could postpone the discussion until one introduces the hierarchy.

I have done lots of rejugging of this chapter which has slowed down the progress. I have more ideas how to improve it but in the moment I want to get t the end before changing everything again.

Thorsten

From: Steve Awodey <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Monday, 25 March 2013 23:18
To: HoTT/book <[email protected]mailto:[email protected]>
Subject: [book] Universes (#32)

the section 1.2 on Universes gets things off to a rather technical and arcane start -- sets as trees, paradoxes, impredicativity, typical ambiguity, it's all rather much for the mathematical reader encountering type theory for the first time.

How about moving this technical discussion to the end of the chapter (and saying that it is optional), and starting with function types instead? We just need to introduce the symbol UU as a way of talking about dependent types. That can be deferred to section 1.4 on dependent types.

UU shouldn't occur in 1.3 anyway.

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

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]

that sounds very good.

Steve

On Mar 26, 2013, at 9:42 AM, Thorsten Altenkirch [email protected] wrote:

I see. Yes, we could introduce the symbol U for a universe of types after function types and before Pi-types when we need to talk about families and move the predicative hierarchy and the discussion to the end of the chapter.

In the section for equality proofs I am now using the "impredicative" but concise construction suggested by Mike. At this point it would be good if one would have introduced the hierarchy, but on the other hand one could postpone the discussion until one introduces the hierarchy.

I have done lots of rejugging of this chapter which has slowed down the progress. I have more ideas how to improve it but in the moment I want to get t the end before changing everything again.

Thorsten

From: Steve Awodey <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Monday, 25 March 2013 23:18
To: HoTT/book <[email protected]mailto:[email protected]>
Subject: [book] Universes (#32)

the section 1.2 on Universes gets things off to a rather technical and arcane start -- sets as trees, paradoxes, impredicativity, typical ambiguity, it's all rather much for the mathematical reader encountering type theory for the first time.

How about moving this technical discussion to the end of the chapter (and saying that it is optional), and starting with function types instead? We just need to introduce the symbol UU as a way of talking about dependent types. That can be deferred to section 1.4 on dependent types.

UU shouldn't occur in 1.3 anyway.

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

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]

this is still ToDo

[txa]

That's done. I close it.

[awodey]

I see now -- thanks!

On Apr 4, 2013, at 6:09 PM, Thorsten Altenkirch [email protected] wrote:

That's done. I close it.

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