mathlib documentation


Categories with finite (co)products #

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


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