Universal Properties Section 2.6 about book HOT 13 CLOSED

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?

from book.

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
#3 (comment).

from book.

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 <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Wednesday, 6 March 2013 22:49
To: HoTT/book <[email protected]mailto:[email protected]>
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//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.

from book.

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 [email protected] 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 <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Wednesday, 6 March 2013 22:49
To: HoTT/book <[email protected]mailto:[email protected]>
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//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.

from book.

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 <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Wednesday, 6 March 2013 23:06
To: HoTT/book <[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]>
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 <[email protected]mailto:[email protected]> 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 <[email protected]mailto:[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]mailto:[email protected]>
Date: Wednesday, 6 March 2013 22:49
To: HoTT/book <[email protected]mailto:[email protected]mailto:[email protected]>
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//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//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.

from book.

On Mar 6, 2013, at 11:24 PM, Thorsten Altenkirch [email protected] 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 <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Wednesday, 6 March 2013 23:06
To: HoTT/book <[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]>
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 <[email protected]mailto:[email protected]> 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 <[email protected]mailto:[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]mailto:[email protected]>
Date: Wednesday, 6 March 2013 22:49
To: HoTT/book <[email protected]mailto:[email protected]mailto:[email protected]>
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//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//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.

from book.

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

from book.

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?

from book.

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" [email protected] 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//issues/3#issuecomment-14556883
.

from book.

From: Steve Awodey <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Wednesday, 6 March 2013 23:34
To: HoTT/book <[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]>
Subject: Re: [book] Universal Properties Section 2.6 (#3)

On Mar 6, 2013, at 11:24 PM, Thorsten Altenkirch <[email protected]mailto:[email protected]> 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 <[email protected]mailto:[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]mailto:[email protected]>
Date: Wednesday, 6 March 2013 23:06
To: HoTT/book <[email protected]mailto:[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]mailto:[email protected]>
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 <[email protected]mailto:[email protected]mailto:[email protected]> 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 <[email protected]mailto:[email protected]mailto:[email protected]:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]mailto:[email protected]:[email protected]>
Date: Wednesday, 6 March 2013 22:49
To: HoTT/book <[email protected]mailto:[email protected]mailto:[email protected]:[email protected]>
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//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//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//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.

from book.

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 <[email protected]mailto:[email protected]>
Reply-To: HoTT/book <[email protected]mailto:[email protected]>
Date: Thursday, 7 March 2013 00:38
To: HoTT/book <[email protected]mailto:[email protected]>
Cc: Thorsten Altenkirch <[email protected]mailto:[email protected]>
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//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.

from book.

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

from book.

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

from book.