ndcroos
ndcroos
This is what I have at the moment for item 1. However, it doesn't use `grp_quotient_map`. (I also needed to add ``{Funext}`). ```coq (** Recursion principle for `cyclic`. *) Definition...
For (1), I have now: ```coq (** Recursion principle for `cyclic`. *) Definition cyclic_rec (n : nat) {G : Group} (g : G) (p : grp_pow g n = mon_unit)...
@Alizter and @jdchristensen, thanks both for your feedback. I am going to try to address also https://github.com/HoTT/Coq-HoTT/issues/2015.
@Alizter For (1) I get the follow error: ``` In environment n : nat G : Group g : G p : grp_pow g n = mon_unit x, a :...
What is the correct way to do such a type conversion in this case? I tried to do something like this: ```coq Definition int_to_abgroup_Z (a : Int) : abgroup_Z :=...