Theorems · Inductive type · category theory

CategoryTheory.Limits.HasFiniteProducts

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

A category has finite products if there exists a limit for every diagram with shape Discrete J, where we have [Finite 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

142 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category