Comments (13)
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,
ThorstenFrom: 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 equivalencePi (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,
ThorstenFrom: 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.
Related Issues (20)
- Rules for universes in Appendix A.2 are incomplete HOT 3
- identity type usage HOT 19
- Augment assumptions for Thm 5.4.4, 5.4.5, and 5.4.7 HOT 19
- Typos in proof of Lemma 10.3.12 HOT 5
- Use parentheses in the proof of Lemma 2.1.4(iii) HOT 3
- Cumulativity of the universe hierarchy HOT 4
- CI problem: "dubious ownership" HOT 1
- Provided Hashes in errata.pdf Not Found HOT 2
- Errata PDF unreadable
- Corollary 8.8.5 HOT 4
- Lemma 8.5.9 is missing a label
- Nightly builds pdfs are dead links HOT 8
- Exercise 7.3 could be made stronger
- Indexing of maps in fiber and exact sequences HOT 3
- proof-theoretic consistency in the introduction HOT 6
- cardinal numbers in the introduction HOT 5
- real numbers in the introduction HOT 7
- Switch to using truncated logic as default in the book HOT 2
- max and sup HOT 9
- Exercise 11.6 seems to need WLPO not LPO HOT 3
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from book.