existence of conical terminal objects

@[reducible, inline]

abbrev CategoryTheory.Enriched.HasConicalTerminal (V : outParam (Type u_1)) [Category.{u_2, u_1} V] [MonoidalCategory V] (C : Type u_3) [Category.{u_4, u_3} C] [EnrichedOrdinaryCategory V C] : Prop

A category has a conical terminal object if it has a conical limit over the empty diagram.

Equations

• CategoryTheory.Enriched.HasConicalTerminal = CategoryTheory.Enriched.HasConicalLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})

Conical Products

instance CategoryTheory.Enriched.HasConicalProducts.hasConicalTerminal (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [HasConicalProducts V C] : HasConicalTerminal V C