Theorems · Inductive type · category theory

CategoryTheory.Limits.HasFiniteCoproducts

(C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop

A category has finite coproducts if there exists a 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.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts

Cited by

110 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.Category