Categories with finite (co)products #
Typeclasses representing categories with (co)products over finite indexing types.
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.
- out : ∀ (n : ℕ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete (Fin n)) C
C
has finite products
Instances
C
has finite products
If C
has finite limits then it has finite products.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If a category has all products then in particular it has finite products.
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.
- out : ∀ (n : ℕ), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (Fin n)) C
C
has all finite coproducts
Instances
C
has all finite coproducts
Equations
- ⋯ = ⋯
If C
has finite colimits then it has finite coproducts.
Equations
- ⋯ = ⋯
If a category has all coproducts then in particular it has finite coproducts.