Added definition for cyclic' to AbGroups/Cyclic.v

[ndcroos]

See #2022

[Alizter]

Also I would add a comment dividing this definition from the top half of the file:

(** ** Alternative definition of cyclic group *)

(** The [n]-th cyclic ....

The format for comments is:

(* Comment that doesn't appear in documentation *)
(** Comment that appears in documentation *)
(** * Title *)
(** ** Header 1 *)
(** *** Header 2 *)

[Alizter]

Thanks, this looks good to me. I'll create an issue so that we remember to replace the old definition of cyclic at some point.

[Alizter]

Actually, upon further thinking, this shouldn't take any universe variables. If you remove all references of u and the universe annotation on AbGroup and ab_cokernel you will see Coq complain about an unbound universe.

To fix this, at the top of the file before the (** * Cyclic groups *) title put

Local Set Universe Minimization ToSet.

This will tell Coq to try to minimize unbound universe variables to Set the lowest universe. Afterwards, the definition of cyclic'@{} should be accepted and you will see it lands in AbGroup@{Set} if you inspect it with About and Set Printing Universes.

[ndcroos]

I have an issue with equiv_Z1_home that I can't resolve by removing universe variables

Coq-HoTT/theories/Algebra/AbGroups/Cyclic.v

Line 32 in a6c4ec7

(** The universal property of [ab_Z1]. *)

I get the error: Universe instance length is 2 but should be 1. If I change the annotation to ab_Z1@{u}, I get another error.

[Alizter]

OK it looks like Local Set Universe Minimization ToSet messed some things up earlier up in the file. In that case, let's move it to after the "alternative def" title.

[jdchristensen]

Other parts of the file don't work with minimization to set. I'm sure they aren't hard to fix, but to keep this PR focused, @ndcroos could just use:

Definition cyclic'@{} (n : nat) : AbGroup@{Set}
  := ab_cokernel (ab_mul@{Set} (A:=abgroup_Z) n).

[ndcroos]

Using this definition, Coq complains here about an unbound universe.

[jdchristensen]

Other parts of the file don't work with minimization to set. I'm sure they aren't hard to fix, but to keep this PR focused, @ndcroos could just use:

Definition cyclic'@{} (n : nat) : AbGroup@{Set}
  := ab_cokernel (ab_mul@{Set} (A:=abgroup_Z) n).

[jdchristensen]

Why was this changed? It gets rid of one universe variable, but we don't generally try to avoid wild category notation just for that. (Moreover, I think with the next release of Coq those stray universe variables might go away.)

[Alizter]

This was my suggestion from earlier, and yes, this will go away when Coq gets algebraic universes. I don't know if it will be the next release of Coq however. It still seems unfinished.

FTR @ndcroos the issue here is that the wildcat of groups should land in the unvierse Set+1 however Coq doesn't let you write that for the moment, meaning we have to introduce a new universe variable strictly larger.

[jdchristensen]

Ok, I missed that comment. But it seems weird to optimize that one result in Image.v to save a universe variable, but not the other results. And it's really orthogonal to this PR.

[Alizter]

One difference here is that we are expecting no universe variables, whereas in other places it is one extra. Anyway, we can cleanup other universe issues some other time.

[jdchristensen]

I'll create an issue so that we remember to replace the old definition of cyclic at some point.

I've wondered whether defining the integers as the free group on one generator might be the best basic definition. You get a lot of properties for free... But now that Int is developed so thoroughly, it does make sense to focus on that definition.

[ndcroos]

I reverted the changes in grp_image in Image.v, and SixTerm.v.
The universe annotations are now removed for both the old and new versions of cyclic.

[ndcroos]

Thanks @Alizter and @jdchristensen for your helpful feedback.

[Alizter]

@ndcroos Thank you for the contribution. For #2022, I believe the next step (new PR) would be to define

Definition cyclic'_in {n} : abgroup_Z $-> cyclic' n := grp_quotient_map _. 

and then show

Definition ab_mul_cyclic'_in (n : nat) (x y : abgroup_Z)
  : ab_mul (@cyclic'_in n x) y = cyclic'_in (x * y).

(The @foo notation makes all implicit arguments of foo explicit.)

[jdchristensen]

Thanks for this!