TODO: module docstring

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

HasPullback f g represents a particular choice of 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)

instance CategoryTheory.Enriched.HasConicalPullback_hasPullback (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) [HasConicalPullback V f g] : Limits.HasPullback 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 a choice of conical pullback for every pair of morphisms

Equations

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

instance CategoryTheory.Enriched.HasConicalPullbacks_hasPullbacks (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [hyp : HasConicalPullbacks V C] : Limits.HasPullbacks C