Existence of conical pullbacks

@[reducible, inline]

abbrev CategoryTheory.Enriched.HasConicalPullback (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : Prop

HasConicalPullback f g represents the mere existence of a conical limit cone for the pair of morphisms f : X ⟶ Z and g : Y ⟶ Z

Equations

• CategoryTheory.Enriched.HasConicalPullback V f g = CategoryTheory.Enriched.HasConicalLimit V (CategoryTheory.Limits.cospan f g)

@[reducible, inline]

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

HasConicalPullbacks represents the existence of conical pullbacks for every pair of morphisms.

Equations

• CategoryTheory.Enriched.HasConicalPullbacks V C = CategoryTheory.Enriched.HasConicalLimitsOfShape CategoryTheory.Limits.WalkingCospan V C