How to get small coproducts from a bigger class?

Stream: new members

[Fernando Chu]

I implemented having all coproducts up to size κ as having all coproducts of shapes of a subset of κ. This however makes it hard to actually get even initial objects as the empty set is not the same as PEmpty. I'm wondering if there's a nice way around this? Or should my implementation be different? E.g. require coproducts for any $J$ with $|J| \leq |\kappa|$? This last option may make proving that a category satisfies this condition harder.

import Mathlib

open CategoryTheory Limits
universe u v w
namespace CategoryTheory

variable (κ : Type w) (C : Type u) [Category.{v} C]
  [has_coprods : (I : Set κ) → HasCoproductsOfShape I C]

instance : HasInitial C := by
  sorry

[Robert Maxton]

It's usually not a great idea to mix the set theory library with other libraries; the set theory library relies heavily on propositional membership that can't be e.g. matched on
Though I suppose if you really want coproducts up to a specific cardinality, there's probably not a lot of better ways...

[Robert Maxton]

That said, while the empty set is not the same as PEmpty, it(s coercion to a type) is equivalent: you can use docs#Equiv.Set.pempty and docs#CategoryTheory.Limits.hasCoproduct_of_equiv_of_iso

[Robert Maxton]

Or directly use docs#CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty

[Adrian Marti]

I would actually argue for using $|J| < \kappa$ for a cardinal $\kappa$ (using the cardinal API, which merely gives types up to equivalence). The reason is that when setting $\kappa = |\mathbb{N}|$, it allows indexing coproducts by all finite sets instead of subsets of $\mathbb{N}$, which might be useful in some cases.

As for proving that a category satisfies this condition, you could still prove a lemma stating that your first condition (or something similar) implies the second stronger one.

[Fernando Chu]

Thanks for the comments. I think using the cardinal API is indeed better. It has also been used here. The problem is that the condition (hA : HasCardinalLT (Arrow A) κ) can not be automatically inferred, so I'm thinking that maybe we have to bundle these things.