book
book copied to clipboard
HoTT
Exercises on univalence
Chapter 2 has no exercises that make use of univalence. Can we come up with any good ones?
Show that the universe is not a "0-type” (in the terms to be introduced in Chapter 3): it is not the case that parallel paths are always equal. (Hint: use the “negation" isomorphism 2 —> 2.)
On Feb 21, 2014, at 7:43 PM, Mike Shulman [email protected] wrote:
Chapter 2 has no exercises that make use of univalence. Can we come up with any good ones?
— Reply to this email directly or view it on GitHub.
that’s OK — the reader is still in chapter 2! we can even add a reference from there back to the exercise.
On Feb 21, 2014, at 7:58 PM, Mike Shulman [email protected] wrote:
That's example 3.1.9...
— Reply to this email directly or view it on GitHub.
I've found it interesting that you can prove (without univalence), e.g., ((p^)^ = p) = (p = p) (and similarly for the other coherence laws). I've wondered if having these type-level equalities for coherence laws at this level is sufficient to generate all the higher coherences with something weaker than path induction. I'm also curious if having univalence lets you extend these down a level (so you prove things about path spaces of points rather than path spaces of paths). Perhaps an exercise could be created from this idea?
How about something like this:
Show that the univalence axiom (for a universe U) is equivalent to the following principle of “equivalence induction" for U: given any family of types A(X, Y, Z) for X, Y : U and Z : Eq(X, Y), if for all X : U we have A(X, X, 1_X), then we also have A(X, Y, Z). Observe that, informally, this says that everything that can be said about types X : U necessarily respects the relation of equivalence of types.
On Feb 21, 2014, at 8:06 PM, Mike Shulman [email protected] wrote:
Ok, well, that's one. Any more?
— Reply to this email directly or view it on GitHub.
@awodey, is univalence actually equivalent to that, or do you need another computation rule (about what happens when you pass in Z := 1_X)? Said another way, is J sufficient to prove it's own computation rule?
How about:
The type of binary relations from X to Y with the property that for every x:X the type of y which are related to x is contractible is equivalent to the type of functions from X to Y.
You can interchange x and y to get funtions from Y to X. Taking both the first and the reversed conditions gives equivalences from X to Y.
One concern with this proposal is that it uses contractibility, but maybe we can reformulate it so that it nicely fits in chapter 2 without needing forward references?
Egbert
@awodey https://github.com/awodey, is univalence actually equivalent to that, or do you need another computation rule (about what happens when you pass in Z := 1_X)? Said another way, is J sufficient to prove it's own computation rule?
Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/636#issuecomment-35790340 .
That's a nice exercise, for it gives a "direct" definition for the term "one-to-one correspondence", which school children learn, without using functions at all.
On Sun, Feb 23, 2014 at 1:03 PM, EgbertRijke [email protected]:
How about:
The type of binary relations from X to Y with the property that for every x:X the type of y which are related to x is contractible is equivalent to the type of functions from X to Y.
You can interchange x and y to get funtions from Y to X. Taking both the first and the reversed conditions gives equivalences from X to Y.
One concern with this proposal is that it uses contractibility, but maybe we can reformulate it so that it nicely fits in chapter 2 without needing forward references?
Egbert
@awodey https://github.com/awodey, is univalence actually equivalent to
that, or do you need another computation rule (about what happens when you pass in Z := 1_X)? Said another way, is J sufficient to prove it's own computation rule?
Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/636#issuecomment-35790340
.
— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/636#issuecomment-35838069 .
@awodey's second suggestion is Corollary 5.8.5, and @EgbertRijke's is almost the same as exercise 4.2.
Yes, that's right... I'm sorry that I didn't look ahead carefully enough. Op 23 feb. 2014 20:01 schreef "Mike Shulman" [email protected]:
@awodey https://github.com/awodey's second suggestion is Corollary 5.8.5, and @EgbertRijke https://github.com/EgbertRijke's is almost the same as exercise 4.2.
Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/636#issuecomment-35839544 .
No need to apologize. As Steve said, we could consider moving some of these exercises forwards for the purpose of having some exercises on univalence in chapter 2, despite the fact that as currently written they fit better where they are. But it would also be nice to have some others.
One possibility, though perhaps not very interesting, would be to work through the facts about transport and equality of structures from section 2.14 using a particular structure other than semigroups. Monoids or graphs maybe.
Here's another idea: give a different proof of theorem 2.11.1 using univalence.
good thing somebody knows what’s where!
On Feb 23, 2014, at 2:01 PM, Mike Shulman [email protected] wrote:
@awodey's second suggestion is Corollary 5.8.5, and @EgbertRijke's is almost the same as exercise 4.2.
— Reply to this email directly or view it on GitHub.
We could also give some forward references at the end of the exercises section of chapter 2 to easy exercises which use univalence and only require the reader looking up a definition (such as contractibility) so that readers know with which exercises to start when they want to practice with univalence. It seems quite hard to come up with an exercise that doesn't use anything that only appears later on in the book.
2014-02-24 6:17 GMT+01:00 Steve Awodey [email protected]:
good thing somebody knows what's where!
On Feb 23, 2014, at 2:01 PM, Mike Shulman [email protected] wrote:
@awodey's second suggestion is Corollary 5.8.5, and @EgbertRijke's is almost the same as exercise 4.2.
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/636#issuecomment-35858418 .
Here's another exercise using univalence (and stuff from chapter 3). Let G be a (set) group and define a G-set to be a set with a G-action. Let B = Sigma(X:G-Set) || X =_{G-Set} G ||. Show that G =_B G is equivalent to G. We could also refer back to this exercise from chapter 8 when we define Eilenberg-Mac Lane spaces, and maybe include a (fairly easy) exercise in ch 8: Show that if G=Z, then the type B from exercise \ref{...} is equivalent to S^1.
Yes - very nice! I think Dan G has recently formalized this.
Sent from my iPhone
On Apr 11, 2014, at 7:24 PM, Mike Shulman [email protected] wrote:
Here's another exercise using univalence (and stuff from chapter 3). Let G be a (set) group and define a G-set to be a set with a G-action. Let B = Sigma(X:G-Set) || X =_{G-Set} G ||. Show that G =_B G is equivalent to G. We could also refer back to this exercise from chapter 8 when we define Eilenberg-Mac Lane spaces, and maybe include a (fairly easy) exercise in ch 8: Show that if G=Z, then the type B from exercise \ref{...} is equivalent to S^1.
— Reply to this email directly or view it on GitHub.
Yes, the first one is here: https://github.com/UniMath/UniMath/blob/d472fdc4ceda8bef85c720e257e425f96bb4ee00/UniMath/Ktheory/GroupAction.v#L418 and the second one is being approached here https://github.com/UniMath/UniMath/blob/d472fdc4ceda8bef85c720e257e425f96bb4ee00/UniMath/Ktheory/Circle.v#L223 and in following items, but without HITs, making it harder.
On Fri, Apr 11, 2014 at 7:47 PM, Steve Awodey [email protected]:
Yes - very nice! I think Dan G has recently formalized this.
Sent from my iPhone
On Apr 11, 2014, at 7:24 PM, Mike Shulman [email protected] wrote:
Here's another exercise using univalence (and stuff from chapter 3). Let G be a (set) group and define a G-set to be a set with a G-action. Let B = Sigma(X:G-Set) || X =_{G-Set} G ||. Show that G =_B G is equivalent to G. We could also refer back to this exercise from chapter 8 when we define Eilenberg-Mac Lane spaces, and maybe include a (fairly easy) exercise in ch 8: Show that if G=Z, then the type B from exercise \ref{...} is equivalent to S^1.
— 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/636#issuecomment-40264600 .