Categories with finite (co)products #
Typeclasses representing categories with (co)products over finite indexing types.
- out : ∀ (J : Type ?) [_inst_2 : decidable_eq J] [_inst_3 : fintype J], category_theory.limits.has_limits_of_shape (category_theory.discrete J) C
C has finite limits then it has finite products.
If a category has all products then in particular it has finite products.
- out : ∀ (J : Type ?) [_inst_2 : decidable_eq J] [_inst_3 : fintype J], category_theory.limits.has_colimits_of_shape (category_theory.discrete J) C
C has finite colimits then it has finite coproducts.
If a category has all coproducts then in particular it has finite coproducts.