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)
:
HasPullback f g represents the mere existence of a conical limit cone for the pair
of morphisms f : X ⟶ Z and g : Y ⟶ Z
Instances For
@[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]
:
HasConicalPullbacks represents the existence of conical pullbacks for every pair of
morphisms.