Make products and sums cumulative.

[dgb37]

Based on some discussion on the zulip and my own need, sums and products have been made cumulative, with the associated necessary changes.

[jdchristensen]

See #1657 for another PR that adds cumulativity. Does it work to use Local Set Polymorphic Inductive Cumulativity near the top of Datatypes.v?

[jdchristensen]

I verified that it works to put Local Set Polymorphic Inductive Cumulativity. near the top of the Datatypes.v file, and to remove the Cumulative keyword on sum and prod, without any additional changes. So I recommend making this change.

[dgb37]

If we add the Local Set &c., do we still want explicit universe annotations akin to what @Alizter requested on all the types defined?

[jdchristensen]

If we add the Local Set &c., do we still want explicit universe annotations akin to what @Alizter requested on all the types defined?

To me that sounds orthogonal to whether the definitions are cumulative, so I see no need for such changes to be part of this PR. But maybe @Alizter has good reasons to ask for this?

[Alizter]

If it works without the annotations then it is fine. My suggestion was in case the number of variables needed reducing.

[jdchristensen]

If it works without the annotations then it is fine. My suggestion was in case the number of variables needed reducing.

I checked, and the annotations to sum don't change the universe variables. The only slight difference is that without annotations, the output universe is max(Set,u,u0), but that's equivalent. So maybe it's better to remove the annotations?

(BTW, I didn't realize that it was even allowed to use max. It is not allowed for the output type of a regular Definition, where it would often be useful, but now I see that it is sometimes allowed for an input type. Interesting.)

[jdchristensen]

@dgb37 Would you like me to push the last couple of changes needed so we can merge this?

[Alizter]

@jdchristensen I think you should just go ahead so we can merge.

[jdchristensen]

I will do it in a day or two.

[jdchristensen]

Ok, I think this is ready to merge. In the end, only three lines are changed by this PR.

[jdchristensen]

Is the doc-proviola CI failure anything to do with this PR, or is it unrelated?

[jdchristensen]

@Alizter @JasonGross Do you know whether the doc-proviola errors are related to this PR? It seems like almost every file is giving a python error 'NoneType' object is not callable. E.g.:

CAMERA html/HoTT.Homotopy.CayleyDickson.html
DEBUG:root:Processing: html/HoTT.Homotopy.CayleyDickson.html
Exception in thread Thread-2 (most likely raised during interpreter shutdown):
Traceback (most recent call last):
  File "/usr/lib/python2.7/threading.py", line 801, in __bootstrap_inner
  File "/usr/lib/python2.7/threading.py", line 754, in run
  File "/github/workspace/proviola/camera/Popen_noblock.py", line 20, in enqueue_output
  File "/usr/lib/python2.7/Queue.py", line 138, in put
  File "/usr/lib/python2.7/threading.py", line 384, in notify
<type 'exceptions.TypeError'>: 'NoneType' object is not callable
proviola-xml/HoTT.Homotopy.BlakersMassey.xml (real: 28.77, user: 3.35, sys: 0.81, mem: 36968 ko)
CAMERA html/HoTT.Homotopy.ClassifyingSpace.html
DEBUG:root:Processing: html/HoTT.Homotopy.ClassifyingSpace.html
proviola-xml/HoTT.Homotopy.CayleyDickson.xml (real: 25.08, user: 0.79, sys: 0.12, mem: 23200 ko)

[Alizter]

@jdchristensen they seem to be related due to the frequency. My guess is that there is a bit of syntax (probably new) that causes proviola to fail. Its definitely in the new arithmetic file, but will require some work to find. I can take a look later.

[jdchristensen]

Weird---despite all of the python errors, the doc-proviola run is now marked as being successful. This PR only changes 3 lines and doesn't have the new arithmetic file, so I think it should be merged now. If I don't hear any disagreement, I'll do so.

(Maybe the doc-proviola runs have been generating errors for a while, but somehow suppress the error codes?)

[Alizter]

@jdchristensen In that case, it is probably due to the Github runner running out of memory and killing a process. If it is green now then I think it is good to merge.