mathlib documentation

category_theory.limits.shapes.finite_products

Categories with finite (co)products #

Typeclasses representing categories with (co)products over finite indexing types.

@[class]

A category has finite coproducts if there is a chosen colimit for every diagram with shape discrete J, where we have [fintype J].

We require this condition only for J = fin n in the definition, then deduce a version for any J : Type* as a corollary of this definition.

Instances of this typeclass