structure CategoryTheory.IsSLimit {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : Type (max (max u u₁) (v + 1))

A limit cone c in a simplicial category A is a simplicially enriched limit if for every X : C, the cone obtained by applying the simplicial coyoneda functor (X ⟶[A] -) to c is a limit cone in SSet.

• isLimit : CategoryTheory.Limits.IsLimit c
• isSLimit : (X : C) → CategoryTheory.Limits.IsLimit (((CategoryTheory.SimplicialCategory.sHomFunctor C).obj (Opposite.op X)).mapCone c)

def CategoryTheory.IsSLimit_islimit {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (slim : CategoryTheory.IsSLimit c) : CategoryTheory.Limits.IsLimit c

Conical simplicial limits are also limits in the unenriched sense.

Equations

• CategoryTheory.IsSLimit_islimit c slim = slim.isLimit

Characterization in terms of the comparison map.

There is a canonical comparison map with the limit in SSet, the following proves that a limit cone in A is a simplicially enriched limit if and only if the comparison map is an isomorphism for every X : A.

noncomputable def CategoryTheory.SimplicialCategory.limitComparison {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) [CategoryTheory.Limits.HasLimitsOfShape J SSet] (X : C) : CategoryTheory.SimplicialCategory.sHom X c.pt ⟶ CategoryTheory.Limits.limit (F.comp ((CategoryTheory.SimplicialCategory.sHomFunctor C).obj (Opposite.op X)))

Equations

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

theorem CategoryTheory.SimplicialCategory.limitComparison_eq_conePointUniqueUpToIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) [CategoryTheory.Limits.HasLimitsOfShape J SSet] (X : C) (h : CategoryTheory.IsSLimit c) [CategoryTheory.Limits.HasLimit (F.comp ((CategoryTheory.SimplicialCategory.sHomFunctor C).obj (Opposite.op X)))] : CategoryTheory.SimplicialCategory.limitComparison c X = ((h.isSLimit X).conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit (F.comp ((CategoryTheory.SimplicialCategory.sHomFunctor C).obj (Opposite.op X))))).hom

theorem CategoryTheory.SimplicialCategory.isIso_limitComparison {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) [CategoryTheory.Limits.HasLimitsOfShape J SSet] (X : C) (h : CategoryTheory.IsSLimit c) : CategoryTheory.IsIso (CategoryTheory.SimplicialCategory.limitComparison c X)

noncomputable def CategoryTheory.SimplicialCategory.limitComparisonIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) [CategoryTheory.Limits.HasLimitsOfShape J SSet] (X : C) (h : CategoryTheory.IsSLimit c) : CategoryTheory.SimplicialCategory.sHom X c.pt ≅ CategoryTheory.Limits.limit (F.comp ((CategoryTheory.SimplicialCategory.sHomFunctor C).obj (Opposite.op X)))

Equations

• CategoryTheory.SimplicialCategory.limitComparisonIso c X h = CategoryTheory.asIso (CategoryTheory.SimplicialCategory.limitComparison c X)

noncomputable def CategoryTheory.SimplicialCategory.isSLimitOfIsIsoLimitComparison {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) [CategoryTheory.Limits.HasLimitsOfShape J SSet] [∀ (X : C), CategoryTheory.IsIso (CategoryTheory.SimplicialCategory.limitComparison c X)] (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.IsSLimit c

Equations

• CategoryTheory.SimplicialCategory.isSLimitOfIsIsoLimitComparison c hc = { isLimit := hc, isSLimit := fun (X : C) => let_fun this := ⋯; Classical.choice ⋯ }

structure CategoryTheory.ConicalLimitCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) : Type (max (max u u₁) (v + 1))

ConicalLimitCone F contains a cone over F together with the information that it is a conical limit.

• cone : CategoryTheory.Limits.Cone F

  The cone itself

• isSLimit : CategoryTheory.IsSLimit self.cone

  The proof that is the limit cone

def CategoryTheory.ConicalLimitCone_isLimitCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (cone : CategoryTheory.Limits.Cone F) (slim : CategoryTheory.IsSLimit cone) : CategoryTheory.Limits.IsLimit cone

A conical limit cone is a limit cone.

Equations

• CategoryTheory.ConicalLimitCone_isLimitCone cone slim = slim.isLimit

class CategoryTheory.HasConicalLimit {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) : Prop

HasConicalLimit F represents the mere existence of a limit for F.

• mk' :: (
• exists_limit : Nonempty (CategoryTheory.ConicalLimitCone F)

  There is some limit cone for F

• )

theorem CategoryTheory.HasConicalLimit.mk {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (d : CategoryTheory.ConicalLimitCone F) : CategoryTheory.HasConicalLimit F

noncomputable def CategoryTheory.getConicalLimitCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) [CategoryTheory.HasConicalLimit F] : CategoryTheory.ConicalLimitCone F

Use the axiom of choice to extract explicit ConicalLimitCone F from HasConicalLimit F.

Equations

• CategoryTheory.getConicalLimitCone F = Classical.choice ⋯

instance CategoryTheory.HasConicalLimit_hasLimit {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) [CategoryTheory.HasConicalLimit F] : CategoryTheory.Limits.HasLimit F

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.conicalLimit.cone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) [CategoryTheory.HasConicalLimit F] : CategoryTheory.Limits.Cone F

An arbitrary choice of limit cone for a functor.

Equations

• CategoryTheory.conicalLimit.cone F = (CategoryTheory.getConicalLimitCone F).cone

noncomputable def CategoryTheory.conicalLimit {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) [CategoryTheory.HasConicalLimit F] : C

An arbitrary choice of conical limit object of a functor.

Equations

• CategoryTheory.conicalLimit F = (CategoryTheory.conicalLimit.cone F).pt

noncomputable def CategoryTheory.conicalLimit.π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) [CategoryTheory.HasConicalLimit F] (j : J) : CategoryTheory.conicalLimit F ⟶ F.obj j

The projection from the conical limit object to a value of the functor.

Equations

• CategoryTheory.conicalLimit.π F j = (CategoryTheory.conicalLimit.cone F).π.app j

@[simp]

theorem CategoryTheory.conicalLimit.w {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) [CategoryTheory.HasConicalLimit F] {j j' : J} (f : j ⟶ j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.conicalLimit.π F j) (F.map f) = CategoryTheory.conicalLimit.π F j'

@[simp]

theorem CategoryTheory.conicalLimit.w_assoc {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) [CategoryTheory.HasConicalLimit F] {j j' : J} (f : j ⟶ j') {Z : C} (h : F.obj j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.conicalLimit.π F j) (CategoryTheory.CategoryStruct.comp (F.map f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.conicalLimit.π F j') h

noncomputable def CategoryTheory.conicalLimit.isConicalLimit {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) [CategoryTheory.HasConicalLimit F] : CategoryTheory.IsSLimit (CategoryTheory.conicalLimit.cone F)

Evidence that the arbitrary choice of cone provided by conicalLimit.cone F is a conical limit cone.

Equations

• CategoryTheory.conicalLimit.isConicalLimit F = (CategoryTheory.getConicalLimitCone F).isSLimit

noncomputable def CategoryTheory.conicalLimit.lift {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) [CategoryTheory.HasConicalLimit F] (c : CategoryTheory.Limits.Cone F) : c.pt ⟶ CategoryTheory.conicalLimit F

The morphism from the cone point of any other cone to the limit object.

Equations

• CategoryTheory.conicalLimit.lift F c = (CategoryTheory.conicalLimit.isConicalLimit F).isLimit.lift c

@[simp]

theorem CategoryTheory.conicalLimit.lift_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} [CategoryTheory.HasConicalLimit F] (c : CategoryTheory.Limits.Cone F) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.conicalLimit.lift F c) (CategoryTheory.conicalLimit.π F j) = c.π.app j

@[simp]

theorem CategoryTheory.conicalLimit.lift_π_assoc {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} [CategoryTheory.HasConicalLimit F] (c : CategoryTheory.Limits.Cone F) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.conicalLimit.lift F c) (CategoryTheory.CategoryStruct.comp (CategoryTheory.conicalLimit.π F j) h) = CategoryTheory.CategoryStruct.comp (c.π.app j) h

class CategoryTheory.HasConicalLimitsOfShape (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] : Prop

C has conical limits of shape J if there exists a conical limit for every functor F : J ⥤ C.

• has_conical_limit : ∀ (F : CategoryTheory.Functor J C), CategoryTheory.HasConicalLimit F

  All functors F : J ⥤ C from J have limits

@[instance 100]

instance CategoryTheory.hasConicalLimitOfHasConicalLimitsOfShape (C : Type u) [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimitsOfShape J C] (F : CategoryTheory.Functor J C) : CategoryTheory.HasConicalLimit F

Equations

• ⋯ = ⋯

instance CategoryTheory.HasConicalLimitsOfShape_hasLimitsOfShape (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J C

Equations

• ⋯ = ⋯

theorem CategoryTheory.hasConicalLimitOfIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F G : CategoryTheory.Functor J C} [CategoryTheory.HasConicalLimit F] (α : F ≅ G) : CategoryTheory.HasConicalLimit G

If a functor F has a conical limit, so does any naturally isomorphic functor.

instance CategoryTheory.hasConicalLimitEquivalenceComp {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (e : K ≌ J) [CategoryTheory.HasConicalLimit F] : CategoryTheory.HasConicalLimit (e.functor.comp F)

Equations

• ⋯ = ⋯

theorem CategoryTheory.hasConicalLimitOfEquivalenceComp {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (e : K ≌ J) [CategoryTheory.HasConicalLimit (e.functor.comp F)] : CategoryTheory.HasConicalLimit F

If a E ⋙ F has a limit, and E is an equivalence, we can construct a limit of F.

theorem CategoryTheory.hasConicalLimitsOfShape_of_equivalence {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {J' : Type u₂} [CategoryTheory.Category.{v₂, u₂} J'] (e : J ≌ J') [CategoryTheory.HasConicalLimitsOfShape J C] : CategoryTheory.HasConicalLimitsOfShape J' C

We can transport conical limits of shape J along an equivalence J ≌ J'.

class CategoryTheory.HasConicalLimitsOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] : Prop

C has all conical limits of size v₁ u₁ (HasLimitsOfSize.{v₁ u₁} C) if it has conical limits of every shape J : Type u₁ with [Category.{v₁} J].

• has_conical_limits_of_shape : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J], CategoryTheory.HasConicalLimitsOfShape J C

  All functors F : J ⥤ C from all small J have conical limits

@[instance 100]

instance CategoryTheory.hasConicalLimitsOfShapeOfHasLimits (C : Type u) [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimitsOfSize.{v₁, u₁, v, u} C] : CategoryTheory.HasConicalLimitsOfShape J C

Equations

• ⋯ = ⋯

instance CategoryTheory.HasConicalLimitsOfSize_hasLimitsOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimitsOfSize.{v₂, u₂, v, u} C] : CategoryTheory.Limits.HasLimitsOfSize.{v₂, u₂, v, u} C

Equations

• ⋯ = ⋯

theorem CategoryTheory.hasConicalLimitsOfSizeOfUnivLE (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [UnivLE.{v₂, v₁} ] [UnivLE.{u₂, u₁} ] [CategoryTheory.HasConicalLimitsOfSize.{v₁, u₁, v, u} C] : CategoryTheory.HasConicalLimitsOfSize.{v₂, u₂, v, u} C

A category that has larger conical limits also has smaller conical limits.

theorem CategoryTheory.hasConicalLimitsOfSizeShrink (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimitsOfSize.{max v₁ v₂, max u₁ u₂, v, u} C] : CategoryTheory.HasConicalLimitsOfSize.{v₁, u₁, v, u} C

hasConicalLimitsOfSizeShrink.{v u} C tries to obtain HasLimitsOfSize.{v u} C from some other HasLimitsOfSize C.

@[reducible, inline]

abbrev CategoryTheory.HasConicalLimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] : Prop

C has all (small) conical limits if it has limits of every shape that is as big as its hom-sets.

Equations

• CategoryTheory.HasConicalLimits C = CategoryTheory.HasConicalLimitsOfSize.{?u.23, ?u.23, ?u.23, ?u.22} C

@[instance 100]

instance CategoryTheory.hasSmallestConicalLimitsOfHasConicalLimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimits C] : CategoryTheory.HasConicalLimitsOfSize.{0, 0, v, u} C

Equations

• ⋯ = ⋯

instance CategoryTheory.HasConicalLimits_hasLimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimits C] : CategoryTheory.Limits.HasLimits C

Equations

• ⋯ = ⋯

instance CategoryTheory.HasConicalLimits.has_conical_limits_of_shape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimits C] (J : Type v) [CategoryTheory.Category.{v, v} J] : CategoryTheory.HasConicalLimitsOfShape J C

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.HasConicalTerminal (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.SimplicialCategory C] : Prop

An abbreviation for HasSLimit (Discrete.functor f).

Equations

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

instance CategoryTheory.HasConicalTerminal_hasTerminal (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [hyp : CategoryTheory.HasConicalTerminal C] : CategoryTheory.Limits.HasTerminal C

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.HasConicalProduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {I : Type w} (f : I → C) : Prop

An abbreviation for HasSLimit (Discrete.functor f).

Equations

• CategoryTheory.HasConicalProduct f = CategoryTheory.HasConicalLimit (CategoryTheory.Discrete.functor f)

instance CategoryTheory.HasConicalProduct_hasProduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {I : Type w} (f : I → C) [CategoryTheory.HasConicalProduct f] : CategoryTheory.Limits.HasProduct f

Equations

• ⋯ = ⋯

class CategoryTheory.HasConicalProducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] : Prop

• has_conical_limits_of_shape : ∀ (J : Type w), CategoryTheory.HasConicalLimitsOfShape (CategoryTheory.Discrete J) C

  All discrete diagrams of bounded size have conical products.

instance CategoryTheory.HasConicalProducts_hasProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [hyp : CategoryTheory.HasConicalProducts C] : CategoryTheory.Limits.HasProducts C

Equations

• ⋯ = ⋯

instance CategoryTheory.HasConicalProducts_hasConicalTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [hyp : CategoryTheory.HasConicalProducts C] : CategoryTheory.HasConicalTerminal C

Equations

• ⋯ = ⋯

instance CategoryTheory.HasConicalProducts_hasConicalTerminal' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [hyp : CategoryTheory.HasConicalProducts C] : CategoryTheory.HasConicalTerminal C

Equations

• ⋯ = ⋯

@[reducible, inline]

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

Equations

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

instance CategoryTheory.HasConicalPullback_hasPullback {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.HasConicalPullback f g] : CategoryTheory.Limits.HasPullback f g

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.HasConicalPullbacks (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] : Prop

Equations

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

instance CategoryTheory.HasConicalPullbacks_hasPullbacks {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalPullbacks C] : CategoryTheory.Limits.HasPullbacks C

Equations

• ⋯ = ⋯