Theorems · Definition · category theory

CategoryTheory.Span.comp

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} →
      [Wₗ.HasPullbacksAgainst Wᵣ] →
        [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] →
          [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] →
            [Wₗ.IsStableUnderComposition] →
              [Wᵣ.IsStableUnderComposition] →
                {c c' c'' : C} →
                  CategoryTheory.Span Wₗ Wᵣ c c' → CategoryTheory.Span Wₗ Wᵣ c' c'' → CategoryTheory.Span Wₗ Wᵣ c c''

The composition of two spans: if the relevant pullback exists and if the morphism properties are stable under the relevant base change, it is given by the total span `` P / \ / \ X₁ X₂ / \ / \ c c' c'' `` where the top diamond is a pullback square

Defined in

Mathlib.CategoryTheory.Bicategory.Span.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.HasPullbacksAgainstCategoryTheory.MorphismProperty.IsStableUnderBaseChangeAgainstCategoryTheory.MorphismProperty.IsStableUnderBaseChangeAgainstCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.MorphismProperty.IsStableUnderComposition