Dualization of missing combinations + Bugfix

[ScriptRaccoon]

On the page with missing data /missing there is a section with missing combinations of the form "p but not q". Missing means that they are consistent, but not yet witnessed by a category in the database. As of writing this, on the main branch there are 449 missing pairs.

Side note: it does not make sense to list missing combinations of the form "p and q", since the trivial category satisfies all properties, so no combination of this form will be missing

Bug

There was a massive bug in the code: It only checked pairs (p,q) where p < q lexicographically. This is not justified since our requirement "p but not q" is not symmetric. For example, neither (thin, but not generating set) nor its dual had been listed before, even though they are "missing". Actually, this combination is inconsistent, the trivial implication "thin => generating set" is missing! (Will be done in another PR.) A better example: "split abelian, but no generator" should be listed as missing.

After fixing this, many more combinations are displayed, their number has become 938.

Dualization

However, many combinations are already witnessed "up to dualization". For example, even though there is (currently) no category in the db which is complete but not cocomplete, there is one which is cocomplete but not complete (the partial order of ordinals). There is also (currently) no category in the db which has powers but not products, but there are categories which have copowers but not coproducts (poset of natural numbers; walking span). This dualization is also supported by the search feature (example).

Hence, it makes sense to list only those pairs of properties p,q where neither "p but not q" nor "p^op but not q^op" are witnessed by a category, where p^op, q^op are the duals of p,q (if they exist). Equivalently: when a combination is already witnessed by the dual of a category in the database, do not mark it as missing.

This brings the number down from 938 to only 465 combinations.

Remark

I have decided to not group or even deduplicate the remaining missing combinations if they are dual to each other. For example, both "cocomplete, but no pullbacks" and "complete, but no pushouts" are listed. The reason is that a user who is interested to add a category that fills this gap can decide which one to pick. But once a category has been added which is complete but has no pushouts, both combinations will disappear from the list.

What else

I have also refactored the code a bit and also added (back) the number of total unknown (category, property)-pairs.

Examples

Here is the list of all 473 combinations (938 = 465 + 473) that are consistent, not witnessed directly, but whose dual is witnessed. These are not shown anymore on the page. The first one of these, "additive but no coreflexive equalizers" is already witnessed by FreeAb^op for example.

473 combinations

[
	["additive", "coreflexive equalizers"],
	["additive", "equalizers"],
	["additive", "finitely complete"],
	["additive", "kernels"],
	["additive", "Malcev"],
	["additive", "pullbacks"],
	["additive", "regular"],
	["additive", "unital"],
	["balanced", "generating set"],
	["balanced", "well-copowered"],
	["binary copowers", "binary powers"],
	["binary coproducts", "binary powers"],
	["binary coproducts", "binary products"],
	["biproducts", "generating set"],
	["biproducts", "kernels"],
	["cartesian closed", "well-powered"],
	["co-Malcev", "binary powers"],
	["co-Malcev", "binary products"],
	["co-Malcev", "coreflexive equalizers"],
	["co-Malcev", "equalizers"],
	["co-Malcev", "generating set"],
	["co-Malcev", "pullbacks"],
	["cocartesian coclosed", "coequalizers"],
	["cocartesian coclosed", "cofiltered limits"],
	["cocartesian coclosed", "cogenerator"],
	["cocartesian coclosed", "connected limits"],
	["cocartesian coclosed", "copowers"],
	["cocartesian coclosed", "coregular"],
	["cocartesian coclosed", "cosifted limits"],
	["cocartesian coclosed", "countable copowers"],
	["cocartesian coclosed", "directed limits"],
	["cocartesian coclosed", "filtered"],
	["cocartesian coclosed", "finitely cocomplete"],
	["cocartesian coclosed", "generating set"],
	["cocartesian coclosed", "generator"],
	["cocartesian coclosed", "locally cocartesian coclosed"],
	["cocartesian coclosed", "locally small"],
	["cocartesian coclosed", "pushouts"],
	["cocartesian coclosed", "reflexive coequalizers"],
	["cocartesian coclosed", "regular quotient object classifier"],
	["cocartesian coclosed", "sequential limits"],
	["cocartesian coclosed", "wide pullbacks"],
	["cocomplete", "generating set"],
	["codistributive", "cocomplete"],
	["codistributive", "coequalizers"],
	["codistributive", "cofiltered limits"],
	["codistributive", "complete"],
	["codistributive", "connected colimits"],
	["codistributive", "connected limits"],
	["codistributive", "copowers"],
	["codistributive", "coproducts"],
	["codistributive", "coreflexive equalizers"],
	["codistributive", "cosifted limits"],
	["codistributive", "countable copowers"],
	["codistributive", "countable coproducts"],
	["codistributive", "countable powers"],
	["codistributive", "countable products"],
	["codistributive", "directed colimits"],
	["codistributive", "directed limits"],
	["codistributive", "equalizers"],
	["codistributive", "filtered colimits"],
	["codistributive", "finitely cocomplete"],
	["codistributive", "finitely complete"],
	["codistributive", "generating set"],
	["codistributive", "generator"],
	["codistributive", "locally essentially small"],
	["codistributive", "locally small"],
	["codistributive", "Malcev"],
	["codistributive", "powers"],
	["codistributive", "products"],
	["codistributive", "pullbacks"],
	["codistributive", "pushouts"],
	["codistributive", "reflexive coequalizers"],
	["codistributive", "regular"],
	["codistributive", "sequential colimits"],
	["codistributive", "sequential limits"],
	["codistributive", "sifted colimits"],
	["codistributive", "well-copowered"],
	["codistributive", "wide pullbacks"],
	["codistributive", "wide pushouts"],
	["coequalizers", "generating set"],
	["coextensive", "cocomplete"],
	["coextensive", "coequalizers"],
	["coextensive", "cofiltered limits"],
	["coextensive", "complete"],
	["coextensive", "connected colimits"],
	["coextensive", "connected limits"],
	["coextensive", "copowers"],
	["coextensive", "coproducts"],
	["coextensive", "coreflexive equalizers"],
	["coextensive", "cosifted limits"],
	["coextensive", "countable copowers"],
	["coextensive", "countable coproducts"],
	["coextensive", "countable powers"],
	["coextensive", "countable products"],
	["coextensive", "directed colimits"],
	["coextensive", "directed limits"],
	["coextensive", "disjoint products"],
	["coextensive", "equalizers"],
	["coextensive", "filtered colimits"],
	["coextensive", "finitely cocomplete"],
	["coextensive", "finitely complete"],
	["coextensive", "generating set"],
	["coextensive", "generator"],
	["coextensive", "locally essentially small"],
	["coextensive", "locally small"],
	["coextensive", "Malcev"],
	["coextensive", "powers"],
	["coextensive", "products"],
	["coextensive", "pullbacks"],
	["coextensive", "pushouts"],
	["coextensive", "reflexive coequalizers"],
	["coextensive", "regular"],
	["coextensive", "sequential colimits"],
	["coextensive", "sequential limits"],
	["coextensive", "sifted colimits"],
	["coextensive", "well-copowered"],
	["coextensive", "wide pullbacks"],
	["coextensive", "wide pushouts"],
	["cofiltered limits", "generating set"],
	["cofiltered limits", "reflexive coequalizers"],
	["cogenerating set", "generating set"],
	["cogenerator", "generating set"],
	["cokernels", "binary powers"],
	["cokernels", "binary products"],
	["cokernels", "generating set"],
	["cokernels", "kernels"],
	["complete", "cocomplete"],
	["complete", "copowers"],
	["complete", "coproducts"],
	["complete", "countable copowers"],
	["complete", "countable coproducts"],
	["complete", "finite copowers"],
	["complete", "finite coproducts"],
	["complete", "finitely cocomplete"],
	["complete", "generating set"],
	["complete", "initial object"],
	["complete", "well-copowered"],
	["connected colimits", "generating set"],
	["connected limits", "generating set"],
	["connected limits", "reflexive coequalizers"],
	["coproducts", "filtered"],
	["coregular", "binary powers"],
	["coregular", "binary products"],
	["coregular", "coreflexive equalizers"],
	["coregular", "equalizers"],
	["coregular", "generating set"],
	["coregular", "pullbacks"],
	["cosifted limits", "generating set"],
	["cosifted limits", "reflexive coequalizers"],
	["counital", "binary powers"],
	["counital", "binary products"],
	["counital", "coreflexive equalizers"],
	["counital", "disjoint finite products"],
	["counital", "equalizers"],
	["counital", "finite powers"],
	["counital", "finite products"],
	["counital", "finitely complete"],
	["counital", "generating set"],
	["counital", "kernels"],
	["counital", "pullbacks"],
	["countable coproducts", "filtered"],
	["countable powers", "binary products"],
	["countable powers", "cosifted"],
	["countable powers", "countable products"],
	["countable powers", "finite products"],
	["countable powers", "generating set"],
	["countable powers", "well-copowered"],
	["countable products", "generating set"],
	["countable products", "well-copowered"],
	["direct", "left cancellative"],
	["directed colimits", "generating set"],
	["directed limits", "generating set"],
	["directed limits", "reflexive coequalizers"],
	["disjoint coproducts", "filtered"],
	["disjoint coproducts", "finite powers"],
	["disjoint coproducts", "finite products"],
	["disjoint coproducts", "terminal object"],
	["disjoint finite coproducts", "binary powers"],
	["disjoint finite coproducts", "binary products"],
	["disjoint finite coproducts", "filtered"],
	["disjoint finite coproducts", "finite powers"],
	["disjoint finite coproducts", "finite products"],
	["disjoint finite coproducts", "terminal object"],
	["disjoint finite products", "generating set"],
	["disjoint finite products", "locally essentially small"],
	["disjoint finite products", "locally small"],
	["disjoint finite products", "well-copowered"],
	["disjoint products", "generating set"],
	["disjoint products", "generator"],
	["disjoint products", "locally essentially small"],
	["disjoint products", "locally small"],
	["disjoint products", "well-copowered"],
	["epi-regular", "generating set"],
	["epi-regular", "reflexive coequalizers"],
	["epi-regular", "well-copowered"],
	["filtered", "cosifted"],
	["filtered colimits", "generating set"],
	["finite copowers", "binary powers"],
	["finite copowers", "binary products"],
	["finite coproducts", "binary powers"],
	["finite coproducts", "binary products"],
	["finite coproducts", "filtered"],
	["finite powers", "binary products"],
	["finite powers", "cosifted"],
	["finite powers", "finite products"],
	["finite powers", "well-copowered"],
	["finite products", "well-copowered"],
	["finitely cocomplete", "binary powers"],
	["finitely cocomplete", "binary products"],
	["finitely cocomplete", "coreflexive equalizers"],
	["finitely cocomplete", "equalizers"],
	["finitely cocomplete", "generating set"],
	["finitely cocomplete", "pullbacks"],
	["finitely complete", "initial object"],
	["finitely complete", "well-copowered"],
	["infinitary codistributive", "cocartesian coclosed"],
	["infinitary codistributive", "cocomplete"],
	["infinitary codistributive", "cogenerating set"],
	["infinitary codistributive", "cogenerator"],
	["infinitary codistributive", "complete"],
	["infinitary codistributive", "connected colimits"],
	["infinitary codistributive", "connected limits"],
	["infinitary codistributive", "copowers"],
	["infinitary codistributive", "coproducts"],
	["infinitary codistributive", "coreflexive equalizers"],
	["infinitary codistributive", "coregular"],
	["infinitary codistributive", "cosifted limits"],
	["infinitary codistributive", "countable copowers"],
	["infinitary codistributive", "countable coproducts"],
	["infinitary codistributive", "directed colimits"],
	["infinitary codistributive", "equalizers"],
	["infinitary codistributive", "filtered colimits"],
	["infinitary codistributive", "finitely complete"],
	["infinitary codistributive", "generating set"],
	["infinitary codistributive", "generator"],
	["infinitary codistributive", "locally cocartesian coclosed"],
	["infinitary codistributive", "locally essentially small"],
	["infinitary codistributive", "locally small"],
	["infinitary codistributive", "Malcev"],
	["infinitary codistributive", "pullbacks"],
	["infinitary codistributive", "regular"],
	["infinitary codistributive", "regular quotient object classifier"],
	["infinitary codistributive", "sequential colimits"],
	["infinitary codistributive", "sifted colimits"],
	["infinitary codistributive", "well-copowered"],
	["infinitary codistributive", "wide pullbacks"],
	["infinitary codistributive", "wide pushouts"],
	["infinitary coextensive", "balanced"],
	["infinitary coextensive", "cocartesian coclosed"],
	["infinitary coextensive", "cocomplete"],
	["infinitary coextensive", "cogenerating set"],
	["infinitary coextensive", "cogenerator"],
	["infinitary coextensive", "complete"],
	["infinitary coextensive", "connected colimits"],
	["infinitary coextensive", "connected limits"],
	["infinitary coextensive", "copowers"],
	["infinitary coextensive", "coproducts"],
	["infinitary coextensive", "coreflexive equalizers"],
	["infinitary coextensive", "coregular"],
	["infinitary coextensive", "cosifted limits"],
	["infinitary coextensive", "countable copowers"],
	["infinitary coextensive", "countable coproducts"],
	["infinitary coextensive", "directed colimits"],
	["infinitary coextensive", "epi-regular"],
	["infinitary coextensive", "equalizers"],
	["infinitary coextensive", "filtered colimits"],
	["infinitary coextensive", "finitely complete"],
	["infinitary coextensive", "generating set"],
	["infinitary coextensive", "generator"],
	["infinitary coextensive", "locally cocartesian coclosed"],
	["infinitary coextensive", "locally essentially small"],
	["infinitary coextensive", "locally small"],
	["infinitary coextensive", "Malcev"],
	["infinitary coextensive", "mono-regular"],
	["infinitary coextensive", "pullbacks"],
	["infinitary coextensive", "quotient object classifier"],
	["infinitary coextensive", "regular"],
	["infinitary coextensive", "regular quotient object classifier"],
	["infinitary coextensive", "semi-strongly connected"],
	["infinitary coextensive", "sequential colimits"],
	["infinitary coextensive", "sifted colimits"],
	["infinitary coextensive", "well-copowered"],
	["infinitary coextensive", "wide pullbacks"],
	["infinitary coextensive", "wide pushouts"],
	["inverse", "cofiltered limits"],
	["inverse", "cosifted limits"],
	["inverse", "direct"],
	["inverse", "directed limits"],
	["inverse", "essentially finite"],
	["inverse", "essentially small"],
	["inverse", "finite"],
	["inverse", "left cancellative"],
	["inverse", "sequential limits"],
	["inverse", "small"],
	["inverse", "well-powered"],
	["kernels", "binary powers"],
	["kernels", "binary products"],
	["kernels", "generating set"],
	["locally cocartesian coclosed", "locally essentially small"],
	["locally cocartesian coclosed", "locally small"],
	["locally cocartesian coclosed", "pullbacks"],
	["locally cocartesian coclosed", "well-powered"],
	["locally essentially small", "well-powered"],
	["locally small", "well-powered"],
	["Malcev", "initial object"],
	["Malcev", "locally essentially small"],
	["Malcev", "locally small"],
	["Malcev", "well-copowered"],
	["Malcev", "well-powered"],
	["mono-regular", "generating set"],
	["mono-regular", "reflexive coequalizers"],
	["mono-regular", "well-copowered"],
	["normal", "generating set"],
	["one-way", "cofiltered limits"],
	["one-way", "cosifted limits"],
	["one-way", "directed limits"],
	["one-way", "left cancellative"],
	["one-way", "sequential limits"],
	["one-way", "well-powered"],
	["pointed", "binary powers"],
	["pointed", "binary products"],
	["pointed", "disjoint finite products"],
	["pointed", "finite powers"],
	["pointed", "finite products"],
	["pointed", "generating set"],
	["pointed", "kernels"],
	["powers", "binary products"],
	["powers", "cosifted"],
	["powers", "countable products"],
	["powers", "finite products"],
	["powers", "generating set"],
	["powers", "products"],
	["powers", "well-copowered"],
	["preadditive", "coreflexive equalizers"],
	["products", "generating set"],
	["products", "well-copowered"],
	["pushouts", "generating set"],
	["quotient object classifier", "cocartesian coclosed"],
	["quotient object classifier", "cocomplete"],
	["quotient object classifier", "codistributive"],
	["quotient object classifier", "coextensive"],
	["quotient object classifier", "cofiltered limits"],
	["quotient object classifier", "cogenerator"],
	["quotient object classifier", "complete"],
	["quotient object classifier", "connected colimits"],
	["quotient object classifier", "connected limits"],
	["quotient object classifier", "copowers"],
	["quotient object classifier", "coproducts"],
	["quotient object classifier", "cosifted limits"],
	["quotient object classifier", "countable copowers"],
	["quotient object classifier", "countable coproducts"],
	["quotient object classifier", "countable powers"],
	["quotient object classifier", "countable products"],
	["quotient object classifier", "directed colimits"],
	["quotient object classifier", "directed limits"],
	["quotient object classifier", "disjoint products"],
	["quotient object classifier", "filtered colimits"],
	["quotient object classifier", "infinitary codistributive"],
	["quotient object classifier", "infinitary coextensive"],
	["quotient object classifier", "locally cocartesian coclosed"],
	["quotient object classifier", "locally small"],
	["quotient object classifier", "powers"],
	["quotient object classifier", "products"],
	["quotient object classifier", "semi-strongly connected"],
	["quotient object classifier", "sequential colimits"],
	["quotient object classifier", "sequential limits"],
	["quotient object classifier", "sifted colimits"],
	["quotient object classifier", "strict terminal object"],
	["quotient object classifier", "wide pullbacks"],
	["quotient object classifier", "wide pushouts"],
	["reflexive coequalizers", "generating set"],
	["regular", "initial object"],
	["regular", "well-copowered"],
	["regular quotient object classifier", "cofiltered limits"],
	["regular quotient object classifier", "cogenerator"],
	["regular quotient object classifier", "connected limits"],
	["regular quotient object classifier", "copowers"],
	["regular quotient object classifier", "coregular"],
	["regular quotient object classifier", "cosifted limits"],
	["regular quotient object classifier", "countable copowers"],
	["regular quotient object classifier", "directed limits"],
	["regular quotient object classifier", "locally small"],
	["regular quotient object classifier", "sequential limits"],
	["regular quotient object classifier", "wide pullbacks"],
	["regular subobject classifier", "coregular"],
	["regular subobject classifier", "finite copowers"],
	["regular subobject classifier", "finite coproducts"],
	["regular subobject classifier", "finitely cocomplete"],
	["regular subobject classifier", "initial object"],
	["regular subobject classifier", "well-powered"],
	["right cancellative", "generating set"],
	["right cancellative", "locally essentially small"],
	["right cancellative", "locally small"],
	["right cancellative", "well-powered"],
	["semi-strongly connected", "generating set"],
	["sequential colimits", "directed colimits"],
	["sequential colimits", "filtered colimits"],
	["sequential colimits", "generating set"],
	["sequential colimits", "sifted colimits"],
	["sequential limits", "generating set"],
	["sifted", "cosifted"],
	["sifted", "filtered"],
	["sifted colimits", "generating set"],
	["strict terminal object", "binary copowers"],
	["strict terminal object", "binary coproducts"],
	["strict terminal object", "binary powers"],
	["strict terminal object", "binary products"],
	["strict terminal object", "cocomplete"],
	["strict terminal object", "coequalizers"],
	["strict terminal object", "cofiltered"],
	["strict terminal object", "cofiltered limits"],
	["strict terminal object", "complete"],
	["strict terminal object", "connected colimits"],
	["strict terminal object", "connected limits"],
	["strict terminal object", "copowers"],
	["strict terminal object", "coproducts"],
	["strict terminal object", "coreflexive equalizers"],
	["strict terminal object", "cosifted"],
	["strict terminal object", "cosifted limits"],
	["strict terminal object", "countable copowers"],
	["strict terminal object", "countable coproducts"],
	["strict terminal object", "countable powers"],
	["strict terminal object", "countable products"],
	["strict terminal object", "directed colimits"],
	["strict terminal object", "directed limits"],
	["strict terminal object", "equalizers"],
	["strict terminal object", "filtered colimits"],
	["strict terminal object", "finite copowers"],
	["strict terminal object", "finite coproducts"],
	["strict terminal object", "finite powers"],
	["strict terminal object", "finite products"],
	["strict terminal object", "finitely cocomplete"],
	["strict terminal object", "finitely complete"],
	["strict terminal object", "generating set"],
	["strict terminal object", "generator"],
	["strict terminal object", "initial object"],
	["strict terminal object", "locally essentially small"],
	["strict terminal object", "locally small"],
	["strict terminal object", "Malcev"],
	["strict terminal object", "powers"],
	["strict terminal object", "products"],
	["strict terminal object", "pullbacks"],
	["strict terminal object", "pushouts"],
	["strict terminal object", "reflexive coequalizers"],
	["strict terminal object", "regular"],
	["strict terminal object", "sequential colimits"],
	["strict terminal object", "sequential limits"],
	["strict terminal object", "sifted colimits"],
	["strict terminal object", "well-copowered"],
	["strict terminal object", "well-powered"],
	["strict terminal object", "wide pullbacks"],
	["strict terminal object", "wide pushouts"],
	["strongly connected", "generating set"],
	["strongly connected", "well-copowered"],
	["terminal object", "cosifted"],
	["terminal object", "well-copowered"],
	["thin", "cofiltered limits"],
	["thin", "connected limits"],
	["thin", "cosifted limits"],
	["thin", "directed limits"],
	["thin", "pullbacks"],
	["thin", "sequential limits"],
	["thin", "well-powered"],
	["thin", "wide pullbacks"],
	["unital", "generating set"],
	["unital", "regular"],
	["well-copowered", "generating set"],
	["well-powered", "locally essentially small"],
	["wide pullbacks", "generating set"],
	["wide pullbacks", "reflexive coequalizers"],
	["wide pushouts", "generating set"],
	["zero morphisms", "generating set"]
]