some remaining exercises in Chapter 2

[Theongck]

No description provided.

[jdchristensen]

Thanks for this! Just a couple of comments.

[jdchristensen]

Suggested change

	(** This exercise is solved in the library as HoTT.Basics.PathGroupoids.apD_homotopic *)
	(** This exercise is solved in the library as HoTT.Basics.PathGroupoids.apD_homotopic, except that the equation is rearranged slightly. *)

Or maybe this version should be added to the library, to be analogous to concat_Ap? And then apD_homotopic could be proved using this new result? @Alizter , what do you think?

[Alizter]

This sounds sensible.

[Alizter]

Thanks, this is great! I'm happy with this once you've addressed Dan's suggestion of adding a variant of apD_homotopic. Not sure what to name that though. It ought to be something like concat_Ap but that doesn't quite work since we are doing some sort of dependent concatenation.

[Alizter]

Thanks, this is great! I'm happy with this once you've addressed Dan's suggestion of adding a variant of apD_homotopic. Not sure what to name that though. It ought to be something like concat_Ap but that doesn't quite work since we are doing some sort of dependent concatenation.

[jdchristensen]

Thanks, this is great! I'm happy with this once you've addressed Dan's suggestion of adding a variant of apD_homotopic. Not sure what to name that though. It ought to be something like concat_Ap but that doesn't quite work since we are doing some sort of dependent concatenation.

What if we just call it apD_natural and put it right before apD_homotopic? (I'm also tempted to rename concat_Ap to ap_natural, but then there would be many other similar results of the form "concat_...A..." that would not fit into the pattern.)

[Alizter]

Looks great, thanks! @jdchristensen feel free to merge when you've taken a look.

[jdchristensen]

Thanks, @Theongck! If you'd like to contribute more to the library, that would be great!

I'll merge once most of the CI passes.