Existence of conical products

class CategoryTheory.Enriched.HasConicalProducts (V : outParam (Type u')) [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] : Prop

Has conical products if all discrete diagrams of bounded size have conical products.

• hasConicalLimitsOfShape (J : Type w) : HasConicalLimitsOfShape (Discrete J) V C

  A family of objects (parametrized by any J : Type w) has a conical product.

@[reducible, inline]

abbrev CategoryTheory.Enriched.HasConicalProduct (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {I : Type w} (f : I → C) : Prop

An abbreviation for HasConicalLimit V (Discrete.functor f).

Equations

• CategoryTheory.Enriched.HasConicalProduct V f = CategoryTheory.Enriched.HasConicalLimit V (CategoryTheory.Discrete.functor f)