Universal Properties Section 2.6 #3
Comments
|
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? |
|
Yes, I have encountered the phenomenon when types with trivial induction On 3/6/2013 10:49 PM, Mike Shulman 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.commailto:notifications@github.com> 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? — 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. |
|
what does it mean to "assume relational parametricity"? Steve On Mar 6, 2013, at 11:00 PM, Thorsten Altenkirch notifications@github.com wrote:
|
|
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 We can define \int X. F(X,X) as Cheers, From: Steve Awodey <notifications@github.commailto:notifications@github.com> what does it mean to "assume relational parametricity"? Steve On Mar 6, 2013, at 11:00 PM, Thorsten Altenkirch <notifications@github.commailto:notifications@github.com> wrote:
— 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. |
|
On Mar 6, 2013, at 11:24 PM, Thorsten Altenkirch notifications@github.com wrote:
you mean we should add all instances of this scheme to type theory?
yes, this is the naturality condition that I mentioned. Steve
|
|
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... |
|
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? |
|
I think your sentence 'it is too naive...' is precisely the point, since
|
|
From: Steve Awodey <notifications@github.commailto:notifications@github.com> On Mar 6, 2013, at 11:24 PM, Thorsten Altenkirch <notifications@github.commailto:notifications@github.com> wrote:
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.
yes, this is the naturality condition that I mentioned. 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
— 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. |
|
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.commailto:notifications@github.com> 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... — 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. |
|
Well, I didn't say it was unrelated. But it's a different statement. |
|
I've fixed the original comment with a forward reference to chapter 4. |
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
The text was updated successfully, but these errors were encountered: