More examples of categories that are not Cauchy complete (WIP)

[ScriptRaccoon]

WIP

This PR adresses all unwitnessed property combinations involving Cauchy completeness. It contributes to this milestone.

First, three results are added:

• one-way ===> Cauchy complete
• pullbacks ===> Cauchy complete
• coequalizers of kernel pairs ===> Cauchy complete

These make it possible to remove some previous proofs for categories. They also imply that the 7 combinations

• one-way ∧ ¬Cauchy complete
• pullbacks ∧ ¬Cauchy complete
• locally cartesian closed ∧ ¬Cauchy complete
• pushouts ∧ ¬Cauchy complete
• locally cocartesian coclosed ∧ ¬Cauchy complete
• coequalizers of kernel pairs ∧ ¬Cauchy complete
• equalizers of cokernel pairs ∧ ¬Cauchy complete

are inconsistent, and therefore do not need any witnesses. They are removed from the list.

Next, the PR adds two categories and decides their properties (TODO).

• The category Euclid_⊔ of coproducts of Euclidean spaces as an example of an infinitary distributive category that is not Cauchy complete.
• The category Free_fg(Z x Z) of finitely generated free Z x Z-modules as an example of an additive category that is not Cauchy complete.

Number of unwitnessed property combinations before the PR: 668. After: TODO