Theorems · Definition · category theory

CategoryTheory.Limits.PullbackCone.ofCone

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} →
      CategoryTheory.Limits.Cone F →
        CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
          (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr)

Given F : WalkingCospan ⥤ C, which is really the same as cospan (F.map inl) (F.map inr), and a cone on F, we get a pullback cone on F.map inl and F.map inr.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Cited by

2 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category