Documentation

InfinityCosmos.ForMathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal

TODO: module docstring

@[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] :

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})

Instances For

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

Limits.HasTerminal C

noncomputable def CategoryTheory.Enriched.HasConicalTerminal.conicalTerminal (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [HasConicalTerminal V C] :

C

Equations

CategoryTheory.Enriched.HasConicalTerminal.conicalTerminal V C = CategoryTheory.Enriched.HasConicalLimit.conicalLimit V (CategoryTheory.Functor.empty C)

Instances For

noncomputable def CategoryTheory.Enriched.HasConicalTerminal.conicalTerminalIsConicalTerminal (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [HasConicalTerminal V C] :

IsConicalTerminal V (conicalTerminal V C)

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def CategoryTheory.Enriched.HasConicalTerminal.isTerminalIsConicalTerminal (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [HasConicalTerminal V C] {T : C} (hT : Limits.IsTerminal T) :

IsConicalTerminal V T

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def CategoryTheory.Enriched.HasConicalTerminal.terminalIsConicalTerminal {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [HasConicalTerminal V C] :

IsConicalTerminal V (⊤_ C)

The terminal object is a conical terminal object.

Equations

CategoryTheory.Enriched.HasConicalTerminal.terminalIsConicalTerminal = CategoryTheory.Enriched.HasConicalTerminal.isTerminalIsConicalTerminal V CategoryTheory.Limits.terminalIsTerminal

Instances For

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] [hyp : HasConicalProducts V C] :

HasConicalTerminal V C

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

HasConicalTerminal V C