Add total/cototal category properties

[dschepler]

Unknown categories decided for "total" property:
category of Z-functors

Unknown categories for "cototal" property:
category of commutative monoids
category of locally ringed spaces
category of Z-functors

[dschepler]

I have some rough ideas on some of the others: on Hausdorff spaces and semigroups, I think I should be able to use an idea similar to the one for Cat to keep control over the images of constant maps. For CMon, I think the "subdirectly irreducible" property might have to do with limiting the number of maps to it - though I'm not yet at all sure how to translate that into a contradiction. And on locally ringed spaces, I have a vague idea that I might be able to define a functor whose L(T) would have a number of maps from Spec k which grows faster than possible for any single locally ringed space.

Anyway, no rush on reviewing this - I was just working on this off and on over the past week, and wanted to get the progress so far pushed before resuming work on the quasitopos PR.

[ScriptRaccoon]

It would be cool if we can merge this soon. The few remaining cases don't have to be dealt with at this moment.

[dschepler]

OK, what does have to be resolved before we can merge it: There are several places where references are missing or incomplete. And the current proof that total -> complete needs to be finished, or replaced with a reference if for some reason finishing off the proof that the construction does give a limit is too complex.

[ScriptRaccoon]

OK, what does have to be resolved before we can merge it: There are several places where references are missing or incomplete. And the current proof that total -> complete needs to be finished, or replaced with a reference if for some reason finishing off the proof that the construction does give a limit is too complex.

Oups I forgot that the proofs are incomplete.