Fix result on regular extensive categories

[ScriptRaccoon]

There is an implication in the database saying that an extensive, regular, and epi-regular category is co-Malvev and has effective cocongruences. However, this is (probably) not correct, since it was not shown that the category is finitely cocomplete, which is part of the definition of being co-Malcev. We need to add the assumption "finitely cocomplete" (or relax the definition of co-Malvev, but this is a whole other topic), and this has been done here.

This brings several changes.

1. The category Quiv_fc of quivers with finite components has an undecided property: if it is regular. Indeed, it is regular, the proof has been added, whereas before it was incorrectly deduced that it is not regular.

2. For this reason, the two combinations

subobject classifier ∧ ¬regular
quotient object classifier ∧ ¬coregular

which were only witnessed by Quiv_fc (or its dual) before, have no witness anymore. They appear in the list of missing combinations now.

3. The incorrect implication has incorrectly deduced that every pretopos is finitely cocomplete:

pretopos ⟹ Barr-exact
Barr-exact ⟹ effective congruences
pretopos ⟹ extensive
effective congruences ∧ extensive ⟹ mono-regular
mono-regular ⟹ balanced
Barr-exact ⟹ regular
balanced ∧ regular ⟹ epi-regular
epi-regular ∧ extensive ∧ regular ⟹ co-Malcev
co-Malcev ⟹ finitely cocomplete

With the fix, we get new potentially consistent combinations. They appear in the list of missing combinations now.

pretopos ∧ ¬co-Malcev
pretopos ∧ ¬coequalizers
pretopos ∧ ¬cokernel pairs
pretopos ∧ ¬effective cocongruences
pretopos ∧ ¬equalizers of cokernel pairs
pretopos ∧ ¬finitely cocomplete
pretopos ∧ ¬pushouts
pretopos ∧ ¬reflexive coequalizers

Indeed, I asked Claude and it quickly came up with a pretopos that does not have coequalizers.

As a result, the number of missing combinations grows from 249 to 259.

FYI @dschepler