Universal Properties Section 2.6

[kristinas]

The following statement in section 2.6 confuses me: "In fact, basically every induction principle in type theory is part of a universal property of this sort", where an example of the said universal property is \Pi (w : A x B), C(w) is equivalent to \Pi (a : A) \Pi (b : B), C(a,b) for products, where the function from right to left (typo in the book says left-to-right) is the dependent eliminator.

The statement seems to suggest a direct generalization to natural numbers: \Pi (n : Nat), C(w) is equivalent to C(0) x (\Pi (n : Nat), C(n) -> C(s(n))) where the function from right to left is the dependent elimination principle.

However, dependent elimination on natural numbers is not an equivalence: there can be multiple distinct recurrences generating the same function, e.g., the recurrences (0, \lambda n,y, s(n)) and (0, lambda n,y, s(y)) both generate the identity function but they can be easily shown not to be equal. So I am not sure what the statement about universal properties is intended to mean ..?

Thanks,

Kristina

[mikeshulman]

Hmm, I guess you're right: that statement is wrong! I was misled by the fact that the non-dependent eliminator is always an equivalence and the fact that the dependent one is also an equivalence in some cases. What is it about products, \Sigma-types, and coproducts that makes the dependent eliminator also be an equivalence? Is it just non-recursiveness?

[kristinas]

Yes, I have encountered the phenomenon when types with trivial induction behave very differently also in some other cases (for example, they can be characterized as the special homotopy-initial algebras whose computation laws are strict).

On 3/6/2013 10:49 PM, Mike Shulman wrote:

Hmm, I guess you're right: that statement is wrong! I was misled by the fact that the non-dependent eliminator is always an equivalence and the fact that the dependent one is also an equivalence in some cases. What is it about products, \Sigma-types, and coproducts that makes the dependent eliminator also be an equivalence? Is it just non-recursiveness?

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

[txa]

At least in the non-dependent case it is true that the type of the eliminator:

Nat -> Pi X.X -> (X -> X) -> X

is an equivalence, if one assumes relational parametricity or interprets Pi as an end.

Thorsten

From: Mike Shulman notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Wednesday, 6 March 2013 22:49 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Subject: Re: [book] Universal Properties Section 2.6 (#3)

Hmm, I guess you're right: that statement is wrong! I was misled by the fact that the non-dependent eliminator is always an equivalence and the fact that the dependent one is also an equivalence in some cases. What is it about products, \Sigma-types, and coproducts that makes the dependent eliminator also be an equivalence? Is it just non-recursiveness?

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

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]

what does it mean to "assume relational parametricity"? or to "interpret Pi as an end"? these are not things that make any sense in the theory -- they are about certain kinds of models. on the other hand, there is a statement in type theory that does make sense -- it involves replacing the Pi with a naturality condition, constructed using identity types. but then the analogy to the other cases is broken.

Steve

On Mar 6, 2013, at 11:00 PM, Thorsten Altenkirch notifications@github.com wrote:

At least in the non-dependent case it is true that the type of the eliminator:

Nat -> Pi X.X -> (X -> X) -> X

is an equivalence, if one assumes relational parametricity or interprets Pi as an end.

Thorsten

From: Mike Shulman notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Wednesday, 6 March 2013 22:49 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Subject: Re: [book] Universal Properties Section 2.6 (#3)

Hmm, I guess you're right: that statement is wrong! I was misled by the fact that the non-dependent eliminator is always an equivalence and the fact that the dependent one is also an equivalence in some cases. What is it about products, \Sigma-types, and coproducts that makes the dependent eliminator also be an equivalence? Is it just non-recursiveness?

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

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.

[txa]

Relational Parametricty can be viewed as an axiom scheme, internalizing System R by Plotkin and Abadi.

Interpreting Pi as an end makes sense inside type theory, the type

Pi X. X -> (X -> X) -> X

can be replaced by

\int_X X -> (X -> X) -> X

noting that the type X -> (X -> X) -> X is the diagonal of the bifunctor

F : Set^op x Set -> Set F(X-,X+) = X- -> (X+ -> X-) -> X+

We can define \int X. F(X,X) as {f : Pi X. F(X,X) | Pi A,B, g : A -> B, F(A,g) f(A) = F(g,B) f(B) }

Cheers, Thorsten

From: Steve Awodey notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Wednesday, 6 March 2013 23:06 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] Universal Properties Section 2.6 (#3)

what does it mean to "assume relational parametricity"? or to "interpret Pi as an end"? these are not things that make any sense in the theory -- they are about certain kinds of models. on the other hand, there is a statement in type theory that does make sense -- it involves replacing the Pi with a naturality condition, constructed using identity types. but then the analogy to the other cases is broken.

Steve

On Mar 6, 2013, at 11:00 PM, Thorsten Altenkirch notifications@github.com<mailto:notifications@github.com> wrote:

At least in the non-dependent case it is true that the type of the eliminator:

Nat -> Pi X.X -> (X -> X) -> X

is an equivalence, if one assumes relational parametricity or interprets Pi as an end.

Thorsten

From: Mike Shulman 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: Wednesday, 6 March 2013 22:49 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.commailto:book@noreply.github.com> Subject: Re: [book] Universal Properties Section 2.6 (#3)

Hmm, I guess you're right: that statement is wrong! I was misled by the fact that the non-dependent eliminator is always an equivalence and the fact that the dependent one is also an equivalence in some cases. What is it about products, \Sigma-types, and coproducts that makes the dependent eliminator also be an equivalence? Is it just non-recursiveness?

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

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.

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

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]

On Mar 6, 2013, at 11:24 PM, Thorsten Altenkirch notifications@github.com wrote:

Relational Parametricty can be viewed as an axiom scheme, internalizing System R by Plotkin and Abadi.

you mean we should add all instances of this scheme to type theory?

Interpreting Pi as an end makes sense inside type theory, the type

Pi X. X -> (X -> X) -> X

can be replaced by

\int_X X -> (X -> X) -> X

noting that the type X -> (X -> X) -> X is the diagonal of the bifunctor

F : Set^op x Set -> Set F(X-,X+) = X- -> (X+ -> X-) -> X+

We can define \int X. F(X,X) as {f : Pi X. F(X,X) | Pi A,B, g : A -> B, F(A,g) f(A) = F(g,B) f(B) }

yes, this is the naturality condition that I mentioned. the Pi's are over all hsets X, A, B, though, not all types.

Steve

Cheers, Thorsten

From: Steve Awodey notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Wednesday, 6 March 2013 23:06 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] Universal Properties Section 2.6 (#3)

what does it mean to "assume relational parametricity"? or to "interpret Pi as an end"? these are not things that make any sense in the theory -- they are about certain kinds of models. on the other hand, there is a statement in type theory that does make sense -- it involves replacing the Pi with a naturality condition, constructed using identity types. but then the analogy to the other cases is broken.

Steve

On Mar 6, 2013, at 11:00 PM, Thorsten Altenkirch notifications@github.com<mailto:notifications@github.com> wrote:

At least in the non-dependent case it is true that the type of the eliminator:

Nat -> Pi X.X -> (X -> X) -> X

is an equivalence, if one assumes relational parametricity or interprets Pi as an end.

Thorsten

From: Mike Shulman 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: Wednesday, 6 March 2013 22:49 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.commailto:book@noreply.github.com> Subject: Re: [book] Universal Properties Section 2.6 (#3)

Hmm, I guess you're right: that statement is wrong! I was misled by the fact that the non-dependent eliminator is always an equivalence and the fact that the dependent one is also an equivalence in some cases. What is it about products, \Sigma-types, and coproducts that makes the dependent eliminator also be an equivalence? Is it just non-recursiveness?

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

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.

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

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]

Steve and Thorsten, I think you guys are talking about something entirely different. The question here is about universal properties, where there is a fixed output type X and an induced equivalence on spaces of maps, e.g. (A + B -> X) is equivalent to (A -> X) * (B -> X). The point is that this is only the case for certain inductive types (the non-recursive ones?), not all of them -- not even in the non-dependent case, I guess, although there is still some universal property of N...

[andrejbauer]

I do not undertand how Kristina's non-example is "a direct generalization to natural numbers". The equivalence

Pi (w : A * B) C w <~> Pi (a : A) P (b : B) C (a, b)

is a dependent exponential law, i.e, some sort of an adjunction (can someone make this precise)? It is too naive to simply plug in the type constructors on one side and think it will "just work". Not all type constructors are born equal.

We can get an exponential law for natural numbers from the fact that Nat = 1 + Nat and an exponential law for sums:

Pi (n : Nat) C n <~> C 0 * Pi (n : Nat) C(n).

This is what I expected Kristina would write. But to get a "genuine" exponential law for natural numbers, we would need an exponential law about inductive types (here T : Type -> Type):

(fix X : Type . T(X)) -> A <~> ?

or even dependently:

Pi (w : (fix T)) C w <~> ?

I am not aware of such exponential laws. Of course, if T is constant the fixpoint is a mirage and the usual exponential laws for * and + kick in. Or we can unfold T a bit to see that it is defined as a sum, like I did above for Nat, and get something. But for a genuinely recursive type not much can be said, can it?

So, aren't we just talking about exponential laws (which tell us how to decompose complicated exponents) and noticing that inductive types do not have a good one?

[mikeshulman]

I think your sentence 'it is too naive...' is precisely the point, since this idea is what was suggested by the original sentence. On Mar 7, 2013 7:24 AM, "Andrej Bauer" notifications@github.com wrote:

I do not undertand how Kristina's non-example is "a direct generalization to natural numbers". The equivalence

Pi (w : A * B) C w <~> Pi (a : A) P (b : B) C (a, b)

is a dependent exponential law, i.e, some sort of an adjunction (can someone make this precise)? It is too naive to simply plug in the type constructors on one side and think it will "just work". Not all type constructors are born equal.

We can get an exponential law for natural numbers from the fact that Nat = 1 + Nat and an exponential law for sums:

Pi (n : Nat) C n <~> C 0 * Pi (n : Nat) C(n).

This is what I expected Kristina would write. But to get a "genuine" exponential law for natural numbers, we would need an exponential law about inductive types (here T : Type -> Type):

(fix X : Type . T(X)) -> A <~> ?

or even dependently:

Pi (w : (fix T)) C w <~> ?

I am not aware of such exponential laws. Of course, if T is constant the fixpoint is a mirage and the usual exponential laws for * and + kick in. Or we can unfold T a bit to see that it is defined as a sum, like I did above for Nat, and get something. But for a genuinely recursive type not much can be said, can it?

So, aren't we just talking about exponential laws (which tell us how to decompose complicated exponents) and noticing that inductive types do not have a good one?

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

[txa]

From: Steve Awodey notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Wednesday, 6 March 2013 23:34 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] Universal Properties Section 2.6 (#3)

On Mar 6, 2013, at 11:24 PM, Thorsten Altenkirch notifications@github.com<mailto:notifications@github.com> wrote:

Relational Parametricty can be viewed as an axiom scheme, internalizing System R by Plotkin and Abadi.

you mean we should add all instances of this scheme to type theory?

We could exploiting the recent work by Bernardy et al. However, I don't think there is a computational explanation for free theorems.

Anyway the instances we need to prove the particular equvalence are well known.

Interpreting Pi as an end makes sense inside type theory, the type

Pi X. X -> (X -> X) -> X

can be replaced by

\int_X X -> (X -> X) -> X

noting that the type X -> (X -> X) -> X is the diagonal of the bifunctor

F : Set^op x Set -> Set F(X-,X+) = X- -> (X+ -> X-) -> X+

We can define \int X. F(X,X) as {f : Pi X. F(X,X) | Pi A,B, g : A -> B, F(A,g) f(A) = F(g,B) f(B) }

yes, this is the naturality condition that I mentioned. the Pi's are over all hsets X, A, B, though, not all types.

Btw it is known (I think) that parametricity implies dinaturality (all big Pis over a bifunctorial type are ends) but I don't think the inverse is true.

Steve

Cheers, Thorsten

From: Steve Awodey 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: Wednesday, 6 March 2013 23:06 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] Universal Properties Section 2.6 (#3)

what does it mean to "assume relational parametricity"? or to "interpret Pi as an end"? these are not things that make any sense in the theory -- they are about certain kinds of models. on the other hand, there is a statement in type theory that does make sense -- it involves replacing the Pi with a naturality condition, constructed using identity types. but then the analogy to the other cases is broken.

Steve

On Mar 6, 2013, at 11:00 PM, Thorsten Altenkirch notifications@github.com<mailto:notifications@github.commailto:notifications@github.com> wrote:

At least in the non-dependent case it is true that the type of the eliminator:

Nat -> Pi X.X -> (X -> X) -> X

is an equivalence, if one assumes relational parametricity or interprets Pi as an end.

Thorsten

From: Mike Shulman notifications@github.com<mailto:notifications@github.commailto:notifications@github.commailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.commailto:reply@reply.github.commailto:reply@reply.github.com> Date: Wednesday, 6 March 2013 22:49 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.commailto:book@noreply.github.commailto:book@noreply.github.com> Subject: Re: [book] Universal Properties Section 2.6 (#3)

Hmm, I guess you're right: that statement is wrong! I was misled by the fact that the non-dependent eliminator is always an equivalence and the fact that the dependent one is also an equivalence in some cases. What is it about products, \Sigma-types, and coproducts that makes the dependent eliminator also be an equivalence? Is it just non-recursiveness?

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

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.

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

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.

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

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.

[txa]

I don't think it is something completely different.

The fact that the eliminator for + is an equivalence (reading Pi as end)

+-elim : A + B -> Pi X:Set. (A -> X) * (B -> X) -> X

is a consequence of the equivalence you mention. I was just saying that this extends to the eliminator for Nat, namely that

nat-elim : Nat -> Pi X:Set . X -> (X -> X) -> X

is an equivalence is a consequence of the universal property of Nat. Actually in this case I know it follows from parametricity but I am not sure it follows from dinaturality (replacing Pi by \int).

Thorsten

From: Mike Shulman notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Thursday, 7 March 2013 00:38 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] Universal Properties Section 2.6 (#3)

Steve and Thorsten, I think you guys are talking about something entirely different. The question here is about universal properties, where there is a fixed output type X and an induced equivalence on spaces of maps, e.g. (A + B -> X) is equivalent to (A -> X) * (B -> X). The point is that this is only the case for certain inductive types (the non-recursive ones?), not all of them -- not even in the non-dependent case, I guess, although there is still some universal property of N...

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

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]

Well, I didn't say it was unrelated. But it's a different statement.

[mikeshulman]

I've fixed the original comment with a forward reference to chapter 4.