Escaping the trunc?

[Vtec234]

In finite_products.lean we show that a category has all finite products given all binary products and a terminal object, but this construction is done on pfin n (which is a universe-polymorphic fin n). Transporting it to arbitrary fintypes seems to only be doable up-to-ordering, so we really get an exists-kind-result wrapped in trunc. It is not clear to me whether it is constructively provable at all that has_binary_products.{v} C -> has_terminal.{v} C -> has_finite_products.{v} C, because it seems to postulate that some canonical ordering exists on all fintypes, which sounds classical (and classically we get trunc α → α).

[b-mehta]

It is not clear to me whether it is constructively provable at all that has_binary_products.{v} C -> has_terminal.{v} C -> has_finite_products.{v} C, because it seems to postulate that some canonical ordering exists on all fintypes, which sounds classical (and classically we get trunc α → α).

This is an interesting question... I don't think it postulates that a canonical ordering exists though, just that an ordering exists for each fintype (for instance, if we have two fintypes of the same cardinality it might not give the same ordering on each...)

[b-mehta]

Hmm so in lean, there's no strength difference between LEM, AC, finite choice and unique choice... I'm less hesitant about having noncomputable results in that case

[b-mehta]

On this note, I modified the proof that Type has a subobject classifier to use unique choice instead of full choice (in beck, by the way)