Exercises on univalence#636

Open
opened this Issue Feb 22, 2014 · 18 comments

5 participants

Chapter 2 has no exercises that make use of univalence. Can we come up with any good ones?

That's example 3.1.9...

Ok, well, that's one. Any more?

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?

@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?

Homotopy Type Theory member

@awodey's second suggestion is Corollary 5.8.5, and @EgbertRijke's is almost the same as exercise 4.2.

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.

Exercises 3.9 and 3.10 also use univalence.

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.

Homotopy Type Theory member