Ex 4.4

[txa]

What is the corresponding statement for natural numbers?

[mikeshulman]

I think the obvious one would be that the space of sections \prd{n:nat}E(n) is equivalent to the space of recurrence data E(0) * \prd{n:nat} E(n) -> E(n+1).

[kristinas]

Right, which it is not.

On Thu, Apr 4, 2013 at 8:43 PM, Mike Shulman notifications@github.comwrote:

I think the obvious one would be that the space of sections \prd{n:nat}E(n) is equivalent to the space of recurrence data E(0) * \prd{n:nat} E(n) -> E(n+1).

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

[txa]

Since we know that

Nat -> X ~ Stream X

I thought

\prd{n:nat}E(n)

is isomorphic to A 0 where A : Nat -> U is the terminal coalgebra generated by the constructor

cons : \prd{n:\nat}E(n) -> A(n) -> A(suc n)

that is E(0)xE(1)xE(2),…

which ought to work.

Thorsten

From: Kristina Sojakova notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Thursday, 4 April 2013 19:47 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] Ex 4.4 (#66)

Right, which it is not.

On Thu, Apr 4, 2013 at 8:43 PM, Mike Shulman notifications@github.com<mailto:notifications@github.com>wrote:

I think the obvious one would be that the space of sections \prd{n:nat}E(n) is equivalent to the space of recurrence data E(0) * \prd{n:nat} E(n) -> E(n+1).

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

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

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]

Maybe we should clarify by saying the "obvious" corresponding statement?

On Thu, Apr 4, 2013 at 11:50 PM, Thorsten Altenkirch < notifications@github.com> wrote:

Since we know that

Nat -> X ~ Stream X

I thought

\prd{n:nat}E(n)

is isomorphic to A 0 where A : Nat -> U is the terminal coalgebra generated by the constructor

cons : \prd{n:\nat}E(n) -> A(n) -> A(suc n)

that is E(0)xE(1)xE(2),…

which ought to work.

Thorsten

From: Kristina Sojakova <notifications@github.com<mailto: notifications@github.com>> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com>

Date: Thursday, 4 April 2013 19:47 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] Ex 4.4 (#66)

Right, which it is not.

On Thu, Apr 4, 2013 at 8:43 PM, Mike Shulman <notifications@github.com mailto:notifications@github.com>wrote:

I think the obvious one would be that the space of sections \prd{n:nat}E(n) is equivalent to the space of recurrence data E(0) * \prd{n:nat} E(n) -> E(n+1).

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

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

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/HoTT/book/issues/66#issuecomment-15937779 .

[kristinas]

Yea, that makes it clearer indeed.

On 4/4/2013 11:57 PM, Mike Shulman wrote:

Maybe we should clarify by saying the "obvious" corresponding statement?

On Thu, Apr 4, 2013 at 11:50 PM, Thorsten Altenkirch < notifications@github.com> wrote:

Since we know that

Nat -> X ~ Stream X

I thought

\prd{n:nat}E(n)

is isomorphic to A 0 where A : Nat -> U is the terminal coalgebra generated by the constructor

cons : \prd{n:\nat}E(n) -> A(n) -> A(suc n)

that is E(0)xE(1)xE(2),…

which ought to work.

Thorsten

From: Kristina Sojakova <notifications@github.com<mailto: notifications@github.com>> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com>

Date: Thursday, 4 April 2013 19:47 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] Ex 4.4 (#66)

Right, which it is not.

On Thu, Apr 4, 2013 at 8:43 PM, Mike Shulman <notifications@github.com mailto:notifications@github.com>wrote:

I think the obvious one would be that the space of sections \prd{n:nat}E(n) is equivalent to the space of recurrence data E(0) * \prd{n:nat} E(n) -> E(n+1).

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

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

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/HoTT/book/issues/66#issuecomment-15937779 .

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

[mikeshulman]

Done.

[txa]

Hang on. Isn't the correct generalisation \prd{n:\nat} X(n) = X(0) x \prd{n:\nat} X(\suc(n)) ? which can be obtained from \nat = 1 + \nat and \prod{x:A+B}f(x) = \prod{a:A}f(\inl(a)) \times \prod{b:B}X(\inr(b)).

[peterlefanulumsdaine]

This is certainly more correct than the false statement under consideration — but I think the false one is indeed the more obvious generalisation, as “the type of premises of the eliminator”, or more precisely, “the type of (fun X => 1 + X)-algebra structures on A.

[peterlefanulumsdaine]

(For anyone reading this thread out of context, by the way: the exercise in question is “Formulate a corresponding statement for natural numbers and show that it fails to hold.”, so the point at issue is not finding a true statement to put here, but about finding the right wording to nudge a reader towards this specific incorrect statement.)

[mikeshulman]

Maybe we should just make it more open-ended. "Formulate a corresponding statement for natural numbers. Does it hold? (There is more than one possibility, and some of the most obvious ones fail.)"

On Fri, Apr 5, 2013 at 9:53 AM, Peter LeFanu Lumsdaine < notifications@github.com> wrote:

(For anyone reading this thread out of context, by the way: the exercise in question is “Formulate a corresponding statement for natural numbers and show that it fails to hold.”, so the point at issue is not finding a true statement to put here, but about finding the right wording to nudge a reader towards this specific incorrect statement.)

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

[txa]

I don't think it is a good idea to nudge the reader in finding a wrong statement.

Why don't we just ask to generalize the statement to Nat and maybe warn the reader that there is a garden path.

T.

From: Peter LeFanu Lumsdaine notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Friday, 5 April 2013 08:53 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] Ex 4.4 (#66)

(For anyone reading this thread out of context, by the way: the exercise in question is “Formulate a corresponding statement for natural numbers and show that it fails to hold.”, so the point at issue is not finding a true statement to put here, but about finding the right wording to nudge a reader towards this specific incorrect statement.)

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

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 think that would be misleading. The point is that in general, the statement doesn't generalize. The fact that you can tweak the obvious false version for nat to obtain modified versions that are true seems like a red herring to me.

On Fri, Apr 5, 2013 at 10:04 AM, Thorsten Altenkirch < notifications@github.com> wrote:

I don't think it is a good idea to nudge the reader in finding a wrong statement.

Why don't we just ask to generalize the statement to Nat and maybe warn the reader that there is a garden path.

T.

From: Peter LeFanu Lumsdaine <notifications@github.com<mailto: notifications@github.com>> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com>

Date: Friday, 5 April 2013 08:53 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] Ex 4.4 (#66)

(For anyone reading this thread out of context, by the way: the exercise in question is “Formulate a corresponding statement for natural numbers and show that it fails to hold.”, so the point at issue is not finding a true statement to put here, but about finding the right wording to nudge a reader towards this specific incorrect statement.)

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

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/HoTT/book/issues/66#issuecomment-15957342 .

[peterlefanulumsdaine]

Agreed with Mike: the big-picture point is exactly that the statement generalizes very naturally to all inductive types, but in properly recursive cases, it typically fails.

Perhaps the wording could be improved (maybe the wording of the preceding exercise is where we should be looking); but I think the main idea of the exercise is a good one as it stands.

[txa]

The red herring is the "obvious false version".

We have that

\prd{x:bool}E(x) = E(0) x E(1)

and

\prd{x:nat}E(x) = E(0)x\prd{x:nat}E(\suc(x)))

and both are consequences of

\prd{x:A+B}E(x) = (\prd{x:A}E(\inl(x))) x (\prd{x:B}E(\inr(b)).

So it does generalize and I don't really understand the reasoning behind the "obvious false version".

T.

From: Mike Shulman notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Friday, 5 April 2013 09:08 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] Ex 4.4 (#66)

I think that would be misleading. The point is that in general, the statement doesn't generalize. The fact that you can tweak the obvious false version for nat to obtain modified versions that are true seems like a red herring to me.

On Fri, Apr 5, 2013 at 10:04 AM, Thorsten Altenkirch < notifications@github.commailto:notifications@github.com> wrote:

I don't think it is a good idea to nudge the reader in finding a wrong statement.

Why don't we just ask to generalize the statement to Nat and maybe warn the reader that there is a garden path.

T.

From: Peter LeFanu Lumsdaine notifications@github.com<mailto:notifications@github.com<mailto: notifications@github.commailto:notifications@github.com>> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.commailto:reply@reply.github.com>

Date: Friday, 5 April 2013 08:53 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.commailto:book@noreply.github.com> Cc: Thorsten Altenkirch txa@Cs.Nott.AC.UK<mailto:txa@Cs.Nott.AC.UKmailto:txa@Cs.Nott.AC.UK> Subject: Re: [book] Ex 4.4 (#66)

(For anyone reading this thread out of context, by the way: the exercise in question is “Formulate a corresponding statement for natural numbers and show that it fails to hold.”, so the point at issue is not finding a true statement to put here, but about finding the right wording to nudge a reader towards this specific incorrect statement.)

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

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/HoTT/book/issues/66#issuecomment-15957342 .

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

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]

The statement of the previous exercise is that the space of dependent functions out of the inductive type bool is equivalent to the space of recurrences, not the "space of dependent functions over each constructor". In other words, the induction constant ind(C,-), regarded as a function, is an equivalence.

On Fri, Apr 5, 2013 at 10:32 AM, Thorsten Altenkirch < notifications@github.com> wrote:

The red herring is the "obvious false version".

We have that

\prd{x:bool}E(x) = E(0) x E(1)

and

\prd{x:nat}E(x) = E(0)x\prd{x:nat}E(\suc(x)))

and both are consequences of

\prd{x:A+B}E(x) = (\prd{x:A}E(\inl(x))) x (\prd{x:B}E(\inr(b)).

So it does generalize and I don't really understand the reasoning behind the "obvious false version".

T.

From: Mike Shulman <notifications@github.com<mailto: notifications@github.com>> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com>

Date: Friday, 5 April 2013 09:08 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] Ex 4.4 (#66)

I think that would be misleading. The point is that in general, the statement doesn't generalize. The fact that you can tweak the obvious false version for nat to obtain modified versions that are true seems like a red herring to me.

On Fri, Apr 5, 2013 at 10:04 AM, Thorsten Altenkirch < notifications@github.commailto:notifications@github.com> wrote:

I don't think it is a good idea to nudge the reader in finding a wrong statement.

Why don't we just ask to generalize the statement to Nat and maybe warn the reader that there is a garden path.

T.

From: Peter LeFanu Lumsdaine <notifications@github.com<mailto: notifications@github.com><mailto: notifications@github.commailto:notifications@github.com>> Reply-To: HoTT/book <reply@reply.github.com<mailto: reply@reply.github.com>mailto:reply@reply.github.com>

Date: Friday, 5 April 2013 08:53 To: HoTT/book <book@noreply.github.com<mailto:book@noreply.github.com mailto:book@noreply.github.com> Cc: Thorsten Altenkirch <txa@Cs.Nott.AC.UK<mailto:txa@Cs.Nott.AC.UK mailto:txa@Cs.Nott.AC.UK> Subject: Re: [book] Ex 4.4 (#66)

(For anyone reading this thread out of context, by the way: the exercise in question is “Formulate a corresponding statement for natural numbers and show that it fails to hold.”, so the point at issue is not finding a true statement to put here, but about finding the right wording to nudge a reader towards this specific incorrect statement.)

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

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< https://github.com/HoTT/book/issues/66#issuecomment-15957342> .

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

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/HoTT/book/issues/66#issuecomment-15958924 .

[peterlefanulumsdaine]

Maybe it’s clearer if we say in Ex 4.3 something like “…the space of recurrences (i.e. the space of choices of the recurrence data required by the eliminator)…”; and then change Ex 4.4 to be a little less open-ended, eg “Show that the analogous statement for \N fails.”

(I would edit this myself but I’m rushing out the door…)

p.s. Mike — I put the Ch.5 comments in your mailbox.

[kristinas]

Maybe we can just say in Ex. 4.3, show that the eliminator is an equivalence.

[txa]

Yes, this is much better!

T.

From: Kristina Sojakova 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> Cc: Thorsten Altenkirch txa@Cs.Nott.AC.UK<mailto:txa@Cs.Nott.AC.UK> Subject: Re: [book] Ex 4.4 (#66)

Maybe we can just say in Ex. 4.3, show that the eliminator is an equivalence.

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

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]

ad22499