FCG (finite coproduct generated) needs to track property of generators

[MxmUrw]

Our current definition of fcg is:

module _ (𝒞 : Category 𝑖) {{_ : hasFiniteCoproducts 𝒞}} where
  record isFiniteCoproductGenerated : 𝒰 𝑖 where
    field fcgSize : ⟨ 𝒞 ⟩ -> 人ℕ
    field fcg : (a : ⟨ 𝒞 ⟩) -> 𝐅𝐮𝐧𝐜 [ fcgSize a ]ᶠ 𝒞
    field fcgIso : ∀ (a : ⟨ 𝒞 ⟩) -> a ≅ ⨆ᶠ (fcg a)

The two options of adding a type family tracking a proposition on the generators would be in the signature or as a field. Since adding it as a field is infrastructurally simpler, and there is currently no other constraint, we do it this way.

What we have keep in mind is that with the current design "fcg" is a structure, the property which the elements have can be different in different situtations, one might think about how to formulate this in a way that the property does not have to be chosen and inherited, but is something which expresses "smallness", maybe something like this.

EDIT The next problem is that this property needs to be stable under isomorphisms of 𝒞, in order to have inheritance by coproduct preserving, eso functors.

[MxmUrw]

This is actually the notion of atoms and atomic categories, as described here