Bicategories of spans in a category

In this file, given a category C and two morphism properties Wₗ and Wᵣ in C that are stable under compositions, contain identities and such that for any morphism b : x₃ ⟶ x₄ in Wₗ and any morphism r : x₂ ⟶ x₃ in Wᵣ, there exists a pullback square

     t
  x₁ --> x₂
  |      |
l |      | r
  v      v
  x₃ --> x₄
     b

in C such that t satisfies Wₗ and l satisfies Wᵣ, we construct the bicategory of spans in C with left morphism in Wₗ and right morphism in Wᵣ.

structure CategoryTheory.Span {C : Type u_1} [Category.{v_1, u_1} C] (Wₗ Wᵣ : MorphismProperty C) (c c' : C) : Type (max u_1 v_1)

A (Wₗ, Wᵣ)-span from c to c' is the data of an object a : C, together with a morphism a ⟶ c in Wₗ, and a morphism a ⟶ c' in Wᵣ.

• apex : C

  the apex of the span

• l : self.apex ⟶ c

  the left map

• r : self.apex ⟶ c'

  the right map

• wl : Wₗ self.l
• wr : Wᵣ self.r

structure CategoryTheory.Span.Hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} (S₁ S₂ : Span Wₗ Wᵣ c c') : Type v_1

A morphism of spans is a morphism between the apices compatible with the projections.

• hom : S₁.apex ⟶ S₂.apex

  the map between the apices

• hom_l : CategoryStruct.comp self.hom S₂.l = S₁.l
• hom_r : CategoryStruct.comp self.hom S₂.r = S₁.r

@[simp]

theorem CategoryTheory.Span.Hom.hom_r_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S₁ S₂ : Span Wₗ Wᵣ c c'} (self : S₁.Hom S₂) {Z : C} (h : c' ⟶ Z) : CategoryStruct.comp self.hom (CategoryStruct.comp S₂.r h) = CategoryStruct.comp S₁.r h

@[simp]

theorem CategoryTheory.Span.Hom.hom_l_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S₁ S₂ : Span Wₗ Wᵣ c c'} (self : S₁.Hom S₂) {Z : C} (h : c ⟶ Z) : CategoryStruct.comp self.hom (CategoryStruct.comp S₂.l h) = CategoryStruct.comp S₁.l h

@[instance_reducible]

instance CategoryTheory.Span.instCategory {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} : Category.{v_1, max u_1 v_1} (Span Wₗ Wᵣ c c')

Equations

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

@[simp]

theorem CategoryTheory.Span.id_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} (S : Span Wₗ Wᵣ c c') : (CategoryStruct.id S).hom = CategoryStruct.id S.apex

@[simp]

theorem CategoryTheory.Span.comp_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {X✝ Y✝ Z✝ : Span Wₗ Wᵣ c c'} (φ : X✝.Hom Y✝) (φ' : Y✝.Hom Z✝) : (CategoryStruct.comp φ φ').hom = CategoryStruct.comp φ.hom φ'.hom

theorem CategoryTheory.Span.hom_ext {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S S' : Span Wₗ Wᵣ c c'} {f g : S ⟶ S'} (h : f.hom = g.hom) : f = g

theorem CategoryTheory.Span.hom_ext_iff {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S S' : Span Wₗ Wᵣ c c'} {f g : S ⟶ S'} : f = g ↔ f.hom = g.hom

@[implicit_reducible]

def CategoryTheory.Span.mkIso {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S S' : Span Wₗ Wᵣ c c'} (e : S.apex ≅ S'.apex) (hₗ : CategoryStruct.comp e.hom S'.l = S.l := by cat_disch) (hᵣ : CategoryStruct.comp e.hom S'.r = S.r := by cat_disch) : S ≅ S'

Construct an isomorphism of spans from an isomorphism between the apices that is compatible with the projections.

Equations

• CategoryTheory.Span.mkIso e hₗ hᵣ = { hom := { hom := e.hom, hom_l := ⋯, hom_r := ⋯ }, inv := { hom := e.inv, hom_l := ⋯, hom_r := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Span.mkIso_inv_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S S' : Span Wₗ Wᵣ c c'} (e : S.apex ≅ S'.apex) (hₗ : CategoryStruct.comp e.hom S'.l = S.l := by cat_disch) (hᵣ : CategoryStruct.comp e.hom S'.r = S.r := by cat_disch) : (mkIso e hₗ hᵣ).inv.hom = e.inv

@[simp]

theorem CategoryTheory.Span.mkIso_hom_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S S' : Span Wₗ Wᵣ c c'} (e : S.apex ≅ S'.apex) (hₗ : CategoryStruct.comp e.hom S'.l = S.l := by cat_disch) (hᵣ : CategoryStruct.comp e.hom S'.r = S.r := by cat_disch) : (mkIso e hₗ hᵣ).hom.hom = e.hom

instance CategoryTheory.Span.instHasPullbackRL {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.HasPullbacksAgainst Wᵣ] {c c' c'' : C} (S₁ : Span Wₗ Wᵣ c c') (S₂ : Span Wₗ Wᵣ c' c'') : Limits.HasPullback S₁.r S₂.l

instance CategoryTheory.Span.instIsStableUnderBaseChangeAlongR {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] (S₁ : Span Wₗ Wᵣ c c') : Wₗ.IsStableUnderBaseChangeAlong S₁.r

instance CategoryTheory.Span.instIsStableUnderBaseChangeAlongL {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] (S₁ : Span Wₗ Wᵣ c c') : Wᵣ.IsStableUnderBaseChangeAlong S₁.l

@[implicit_reducible]

def CategoryTheory.Span.id {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] (c : C) : Span Wₗ Wᵣ c c

The identity span, where both legs are identity morphisms.

Equations

• CategoryTheory.Span.id c = { apex := c, l := CategoryTheory.CategoryStruct.id c, r := CategoryTheory.CategoryStruct.id c, wl := ⋯, wr := ⋯ }

@[simp]

theorem CategoryTheory.Span.id_apex {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] (c : C) : (id c).apex = c

@[simp]

theorem CategoryTheory.Span.id_l {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] (c : C) : (id c).l = CategoryStruct.id c

@[simp]

theorem CategoryTheory.Span.id_r {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] (c : C) : (id c).r = CategoryStruct.id c

@[implicit_reducible]

noncomputable def CategoryTheory.Span.comp {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {c c' c'' : C} (S₁ : Span Wₗ Wᵣ c c') (S₂ : Span Wₗ Wᵣ c' c'') : 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

Equations

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

@[simp]

theorem CategoryTheory.Span.comp_r {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {c c' c'' : C} (S₁ : Span Wₗ Wᵣ c c') (S₂ : Span Wₗ Wᵣ c' c'') : (S₁.comp S₂).r = CategoryStruct.comp (Limits.pullback.snd S₁.r S₂.l) S₂.r

@[simp]

theorem CategoryTheory.Span.comp_apex {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {c c' c'' : C} (S₁ : Span Wₗ Wᵣ c c') (S₂ : Span Wₗ Wᵣ c' c'') : (S₁.comp S₂).apex = Limits.pullback S₁.r S₂.l

@[simp]

theorem CategoryTheory.Span.comp_l {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {c c' c'' : C} (S₁ : Span Wₗ Wᵣ c c') (S₂ : Span Wₗ Wᵣ c' c'') : (S₁.comp S₂).l = CategoryStruct.comp (Limits.pullback.fst S₁.r S₂.l) S₁.l

structure CategoryTheory.Span.SpanBicat (C : Type u_1) [Category.{v_1, u_1} C] (Wₗ Wᵣ : MorphismProperty C) : Type u_1

The bicategory of spans of C with left/right legs satisfying given morphism properties. This is a one-field structure wrapper around C.

• of : C

  the underlying object of C of a term in SpanBicat C _ _

@[instance_reducible]

noncomputable instance CategoryTheory.Span.SpanBicat.instCategoryStruct {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] : CategoryStruct.{max u_1 v_1, u_1} (SpanBicat C Wₗ Wᵣ)

Equations

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

@[simp]

theorem CategoryTheory.Span.SpanBicat.id_apex {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] (X : SpanBicat C Wₗ Wᵣ) : (CategoryStruct.id X).apex = X.of

@[simp]

theorem CategoryTheory.Span.SpanBicat.id_l {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X : SpanBicat C Wₗ Wᵣ} : (CategoryStruct.id X).l = CategoryStruct.id X.of

@[simp]

theorem CategoryTheory.Span.SpanBicat.id_r {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X : SpanBicat C Wₗ Wᵣ} : (CategoryStruct.id X).r = CategoryStruct.id X.of

@[instance_reducible]

instance CategoryTheory.Span.SpanBicat.instCategoryHom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} : Category.{v_1, max u_1 v_1} (X ⟶ Y)

Equations

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

@[simp]

theorem CategoryTheory.Span.SpanBicat.hom₂_comp_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' S'' : X ⟶ Y} (f : S ⟶ S') (g : S' ⟶ S'') : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

@[simp]

theorem CategoryTheory.Span.SpanBicat.hom₂_id_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) : (CategoryStruct.id S).hom = CategoryStruct.id S.apex

theorem CategoryTheory.Span.SpanBicat.hom₂_ext {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} {f g : S ⟶ S'} (h : f.hom = g.hom) : f = g

theorem CategoryTheory.Span.SpanBicat.hom₂_ext_iff {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} {f g : S ⟶ S'} : f = g ↔ f.hom = g.hom

@[reducible, inline]

abbrev CategoryTheory.Span.SpanBicat.mkHom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {apex : C} (l : apex ⟶ X.of) (r : apex ⟶ Y.of) (wl : Wₗ l) (wr : Wᵣ r) : X ⟶ Y

Constructor for 1-morphisms in SpanBicat C _ _

Equations

• CategoryTheory.Span.SpanBicat.mkHom l r wl wr = { apex := apex, l := l, r := r, wl := wl, wr := wr }

@[implicit_reducible]

def CategoryTheory.Span.SpanBicat.mkHom₂ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} (e : S.apex ⟶ S'.apex) (hₗ : CategoryStruct.comp e S'.l = S.l := by cat_disch) (hᵣ : CategoryStruct.comp e S'.r = S.r := by cat_disch) : S ⟶ S'

Constructor for 2-morphisms in SpanBicat C _ _

Equations

• CategoryTheory.Span.SpanBicat.mkHom₂ e hₗ hᵣ = { hom := e, hom_l := ⋯, hom_r := ⋯ }

@[simp]

theorem CategoryTheory.Span.SpanBicat.mkHom₂_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} (e : S.apex ⟶ S'.apex) (hₗ : CategoryStruct.comp e S'.l = S.l := by cat_disch) (hᵣ : CategoryStruct.comp e S'.r = S.r := by cat_disch) : (mkHom₂ e hₗ hᵣ).hom = e

@[reducible, inline]

abbrev CategoryTheory.Span.SpanBicat.mkIso₂ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} (e : S.apex ≅ S'.apex) (hₗ : CategoryStruct.comp e.hom S'.l = S.l := by cat_disch) (hᵣ : CategoryStruct.comp e.hom S'.r = S.r := by cat_disch) : S ≅ S'

Constructor for 2-isomorphisms in SpanBicat C _ _

Equations

• CategoryTheory.Span.SpanBicat.mkIso₂ e hₗ hᵣ = { hom := { hom := e.hom, hom_l := ⋯, hom_r := ⋯ }, inv := { hom := e.inv, hom_l := ⋯, hom_r := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

The goal of this section is to abstract as much as possible the fact that the composition uses an arbitrary pullback, and provides some "proxy" for working with the fact that apices of compositions of spans are pullbacks.

This way, if spans ever get refactored in a way that uses chosen pullbacks instead of arbitrary ones, most downstream applications will not be affected as long as they are careful to use the API provided here.

The primitives of this API are the data of the two projections πₗ : (S₁ ≫ S₂).apex ⟶ S₁.apex and πᵣ : (S₁ ≫ S₂).apex ⟶ S₂.apex, the equalities (S₁ ≫ S₂).l = πₗ ≫ S₁.l and (S₁ ≫ S₂).r = πᵣ ≫ S₂.r, the commutative square πₗ ≫ S₁.r = πᵣ ≫ S₂.l and the fact that this defines a pullback square.

noncomputable def CategoryTheory.Span.SpanBicat.πₗ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) : (CategoryStruct.comp S₁ S₂).apex ⟶ S₁.apex

The left projection πₗ : (S₁ ≫ S₂).apex ⟶ S₁.apex.

Equations

• CategoryTheory.Span.SpanBicat.πₗ S₁ S₂ = CategoryTheory.Limits.pullback.fst S₁.r S₂.l

noncomputable def CategoryTheory.Span.SpanBicat.πᵣ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) : (CategoryStruct.comp S₁ S₂).apex ⟶ S₂.apex

The right projection πᵣ : (S₁ ≫ S₂).apex ⟶ S₂.apex.

Equations

• CategoryTheory.Span.SpanBicat.πᵣ S₁ S₂ = CategoryTheory.Limits.pullback.snd S₁.r S₂.l

@[simp]

theorem CategoryTheory.Span.SpanBicat.comp_l {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) : (CategoryStruct.comp S₁ S₂).l = CategoryStruct.comp (πₗ S₁ S₂) S₁.l

theorem CategoryTheory.Span.SpanBicat.comp_l_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) {Z✝ : C} (h : X.of ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp S₁ S₂).l h = CategoryStruct.comp (πₗ S₁ S₂) (CategoryStruct.comp S₁.l h)

@[simp]

theorem CategoryTheory.Span.SpanBicat.comp_r {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) : (CategoryStruct.comp S₁ S₂).r = CategoryStruct.comp (πᵣ S₁ S₂) S₂.r

theorem CategoryTheory.Span.SpanBicat.comp_r_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) {Z✝ : C} (h : Z.of ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp S₁ S₂).r h = CategoryStruct.comp (πᵣ S₁ S₂) (CategoryStruct.comp S₂.r h)

@[simp]

theorem CategoryTheory.Span.SpanBicat.comp_comm {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) : CategoryStruct.comp (πₗ S₁ S₂) S₁.r = CategoryStruct.comp (πᵣ S₁ S₂) S₂.l

@[simp]

theorem CategoryTheory.Span.SpanBicat.comp_comm_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) {Z✝ : C} (h : Y.of ⟶ Z✝) : CategoryStruct.comp (πₗ S₁ S₂) (CategoryStruct.comp S₁.r h) = CategoryStruct.comp (πᵣ S₁ S₂) (CategoryStruct.comp S₂.l h)

@[implicit_reducible]

noncomputable def CategoryTheory.Span.SpanBicat.compPullbackCone {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) : Limits.PullbackCone S₁.r S₂.l

The pullback cone that defines the apex for the composition of spans.

Equations

• CategoryTheory.Span.SpanBicat.compPullbackCone S₁ S₂ = CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Span.SpanBicat.πₗ S₁ S₂) (CategoryTheory.Span.SpanBicat.πᵣ S₁ S₂) ⋯

@[simp]

theorem CategoryTheory.Span.SpanBicat.compPullbackCone_pt {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) : (compPullbackCone S₁ S₂).pt = (CategoryStruct.comp S₁ S₂).apex

@[simp]

theorem CategoryTheory.Span.SpanBicat.compPullbackCone_fst {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) : (compPullbackCone S₁ S₂).fst = πₗ S₁ S₂

@[simp]

theorem CategoryTheory.Span.SpanBicat.compPullbackCone_snd {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) : (compPullbackCone S₁ S₂).snd = πᵣ S₁ S₂

noncomputable def CategoryTheory.Span.SpanBicat.isLimitCompPullbackCone {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : X ⟶ Y) (S₂ : Y ⟶ Z) : Limits.IsLimit (compPullbackCone S₁ S₂)

The pullback cone that defines the apex for the composition of spans is a limit cone.

Equations

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

theorem CategoryTheory.Span.SpanBicat.comp_hom_ext_apex {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ : X ⟶ Y} {S₂ : Y ⟶ Z} {c : C} {f g : c ⟶ (CategoryStruct.comp S₁ S₂).apex} (hₗ : CategoryStruct.comp f (πₗ S₁ S₂) = CategoryStruct.comp g (πₗ S₁ S₂)) (hᵣ : CategoryStruct.comp f (πᵣ S₁ S₂) = CategoryStruct.comp g (πᵣ S₁ S₂)) : f = g

theorem CategoryTheory.Span.SpanBicat.comp_hom_ext_apex_iff {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ : X ⟶ Y} {S₂ : Y ⟶ Z} {c : C} {f g : c ⟶ (CategoryStruct.comp S₁ S₂).apex} : f = g ↔ CategoryStruct.comp f (πₗ S₁ S₂) = CategoryStruct.comp g (πₗ S₁ S₂) ∧ CategoryStruct.comp f (πᵣ S₁ S₂) = CategoryStruct.comp g (πᵣ S₁ S₂)

noncomputable def CategoryTheory.Span.SpanBicat.compLiftApex {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ : X ⟶ Y} {S₂ : Y ⟶ Z} {c : C} (fₗ : c ⟶ S₁.apex) (fᵣ : c ⟶ S₂.apex) (hₘ : CategoryStruct.comp fₗ S₁.r = CategoryStruct.comp fᵣ S₂.l := by cat_disch) : c ⟶ (CategoryStruct.comp S₁ S₂).apex

A restatement of the universal property of (S₁ ≫ S₂).apex as coming from a pullback. This is the main intended way to produce morphisms towards the apex of a composition of spans.

Equations

• CategoryTheory.Span.SpanBicat.compLiftApex fₗ fᵣ hₘ = CategoryTheory.Limits.PullbackCone.IsLimit.lift (CategoryTheory.Span.SpanBicat.isLimitCompPullbackCone S₁ S₂) fₗ fᵣ hₘ

@[simp]

theorem CategoryTheory.Span.SpanBicat.compLiftApex_πₗ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ : X ⟶ Y} {S₂ : Y ⟶ Z} {c : C} (fₗ : c ⟶ S₁.apex) (fᵣ : c ⟶ S₂.apex) (hₘ : CategoryStruct.comp fₗ S₁.r = CategoryStruct.comp fᵣ S₂.l := by cat_disch) : CategoryStruct.comp (compLiftApex fₗ fᵣ hₘ) (πₗ S₁ S₂) = fₗ

@[simp]

theorem CategoryTheory.Span.SpanBicat.compLiftApex_πₗ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ : X ⟶ Y} {S₂ : Y ⟶ Z} {c : C} (fₗ : c ⟶ S₁.apex) (fᵣ : c ⟶ S₂.apex) (hₘ : CategoryStruct.comp fₗ S₁.r = CategoryStruct.comp fᵣ S₂.l := by cat_disch) {Z✝ : C} (h : S₁.apex ⟶ Z✝) : CategoryStruct.comp (compLiftApex fₗ fᵣ hₘ) (CategoryStruct.comp (πₗ S₁ S₂) h) = CategoryStruct.comp fₗ h

@[simp]

theorem CategoryTheory.Span.SpanBicat.compLiftApex_πᵣ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ : X ⟶ Y} {S₂ : Y ⟶ Z} {c : C} (fₗ : c ⟶ S₁.apex) (fᵣ : c ⟶ S₂.apex) (hₘ : CategoryStruct.comp fₗ S₁.r = CategoryStruct.comp fᵣ S₂.l := by cat_disch) : CategoryStruct.comp (compLiftApex fₗ fᵣ hₘ) (πᵣ S₁ S₂) = fᵣ

@[simp]

theorem CategoryTheory.Span.SpanBicat.compLiftApex_πᵣ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ : X ⟶ Y} {S₂ : Y ⟶ Z} {c : C} (fₗ : c ⟶ S₁.apex) (fᵣ : c ⟶ S₂.apex) (hₘ : CategoryStruct.comp fₗ S₁.r = CategoryStruct.comp fᵣ S₂.l := by cat_disch) {Z✝ : C} (h : S₂.apex ⟶ Z✝) : CategoryStruct.comp (compLiftApex fₗ fᵣ hₘ) (CategoryStruct.comp (πᵣ S₁ S₂) h) = CategoryStruct.comp fᵣ h

@[implicit_reducible]

noncomputable def CategoryTheory.Span.SpanBicat.compLift {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ : X ⟶ Y} {S₂ : Y ⟶ Z} {S : X ⟶ Z} (fₗ : S.apex ⟶ S₁.apex) (fᵣ : S.apex ⟶ S₂.apex) (hₗ : CategoryStruct.comp fₗ S₁.l = S.l := by cat_disch) (hₘ : CategoryStruct.comp fₗ S₁.r = CategoryStruct.comp fᵣ S₂.l := by cat_disch) (hᵣ : CategoryStruct.comp fᵣ S₂.r = S.r := by cat_disch) : S ⟶ CategoryStruct.comp S₁ S₂

A restatement of the universal property of S₁ ≫ S₂ as coming from a pullback. This is the main intended way to produce morphisms towards a composition of spans.

Equations

• CategoryTheory.Span.SpanBicat.compLift fₗ fᵣ hₗ hₘ hᵣ = { hom := CategoryTheory.Span.SpanBicat.compLiftApex fₗ fᵣ ⋯, hom_l := ⋯, hom_r := ⋯ }

@[simp]

theorem CategoryTheory.Span.SpanBicat.compLift_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ : X ⟶ Y} {S₂ : Y ⟶ Z} {S : X ⟶ Z} (fₗ : S.apex ⟶ S₁.apex) (fᵣ : S.apex ⟶ S₂.apex) (hₗ : CategoryStruct.comp fₗ S₁.l = S.l := by cat_disch) (hₘ : CategoryStruct.comp fₗ S₁.r = CategoryStruct.comp fᵣ S₂.l := by cat_disch) (hᵣ : CategoryStruct.comp fᵣ S₂.r = S.r := by cat_disch) : (compLift fₗ fᵣ hₗ hₘ hᵣ).hom = compLiftApex fₗ fᵣ ⋯

theorem CategoryTheory.Span.SpanBicat.compLift_hom_πₗ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ : X ⟶ Y} {S₂ : Y ⟶ Z} (S : X ⟶ Z) (fₗ : S.apex ⟶ S₁.apex) (fᵣ : S.apex ⟶ S₂.apex) (hₗ : CategoryStruct.comp fₗ S₁.l = S.l := by cat_disch) (hₘ : CategoryStruct.comp fₗ S₁.r = CategoryStruct.comp fᵣ S₂.l := by cat_disch) (hᵣ : CategoryStruct.comp fᵣ S₂.r = S.r := by cat_disch) : CategoryStruct.comp (compLift fₗ fᵣ hₗ hₘ hᵣ).hom (πₗ S₁ S₂) = fₗ

theorem CategoryTheory.Span.SpanBicat.compLift_hom_πᵣ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ : X ⟶ Y} {S₂ : Y ⟶ Z} (S : X ⟶ Z) (fₗ : S.apex ⟶ S₁.apex) (fᵣ : S.apex ⟶ S₂.apex) (hₗ : CategoryStruct.comp fₗ S₁.l = S.l := by cat_disch) (hₘ : CategoryStruct.comp fₗ S₁.r = CategoryStruct.comp fᵣ S₂.l := by cat_disch) (hᵣ : CategoryStruct.comp fᵣ S₂.r = S.r := by cat_disch) : CategoryStruct.comp (compLift fₗ fᵣ hₗ hₘ hᵣ).hom (πᵣ S₁ S₂) = fᵣ

noncomputable def CategoryTheory.Span.SpanBicat.associator {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {c₁ c₂ c₃ c₄ : SpanBicat C Wₗ Wᵣ} (S₁ : c₁ ⟶ c₂) (S₂ : c₂ ⟶ c₃) (S₃ : c₃ ⟶ c₄) : CategoryStruct.comp (CategoryStruct.comp S₁ S₂) S₃ ≅ CategoryStruct.comp S₁ (CategoryStruct.comp S₂ S₃)

The associator isomorphisms for the bicategory structure on spans.

Equations

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

noncomputable def CategoryTheory.Span.SpanBicat.rightUnitor {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {c c' : SpanBicat C Wₗ Wᵣ} (S₁ : c ⟶ c') : CategoryStruct.comp S₁ (CategoryStruct.id c') ≅ S₁

The right unitor for the bicategory structure on spans.

Equations

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

noncomputable def CategoryTheory.Span.SpanBicat.leftUnitor {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {c c' : SpanBicat C Wₗ Wᵣ} (S₁ : c ⟶ c') : CategoryStruct.comp (CategoryStruct.id c) S₁ ≅ S₁

The left unitor for the bicategory structure on spans.

Equations

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

@[instance_reducible]

noncomputable instance CategoryTheory.Span.SpanBicat.instBicategory {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] : Bicategory (SpanBicat C Wₗ Wᵣ)

Equations

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

@[simp]

theorem CategoryTheory.Span.SpanBicat.whiskerLeft_hom_πₗ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) {S₁ S₂ : Y ⟶ Z} (f : S₁ ⟶ S₂) : CategoryStruct.comp (Bicategory.whiskerLeft S f).hom (πₗ S S₂) = πₗ S S₁

@[simp]

theorem CategoryTheory.Span.SpanBicat.whiskerLeft_hom_πₗ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) {S₁ S₂ : Y ⟶ Z} (f : S₁ ⟶ S₂) {Z✝ : C} (h : S.apex ⟶ Z✝) : CategoryStruct.comp (Bicategory.whiskerLeft S f).hom (CategoryStruct.comp (πₗ S S₂) h) = CategoryStruct.comp (πₗ S S₁) h

@[simp]

theorem CategoryTheory.Span.SpanBicat.whiskerLeft_hom_πᵣ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) {S₁ S₂ : Y ⟶ Z} (f : S₁ ⟶ S₂) : CategoryStruct.comp (Bicategory.whiskerLeft S f).hom (πᵣ S S₂) = CategoryStruct.comp (πᵣ S S₁) f.hom

@[simp]

theorem CategoryTheory.Span.SpanBicat.whiskerLeft_hom_πᵣ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) {S₁ S₂ : Y ⟶ Z} (f : S₁ ⟶ S₂) {Z✝ : C} (h : S₂.apex ⟶ Z✝) : CategoryStruct.comp (Bicategory.whiskerLeft S f).hom (CategoryStruct.comp (πᵣ S S₂) h) = CategoryStruct.comp (πᵣ S S₁) (CategoryStruct.comp f.hom h)

@[simp]

theorem CategoryTheory.Span.SpanBicat.whiskerRight_hom_πₗ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ S₂ : X ⟶ Y} (f : S₁ ⟶ S₂) (S : Y ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight f S).hom (πₗ S₂ S) = CategoryStruct.comp (πₗ S₁ S) f.hom

@[simp]

theorem CategoryTheory.Span.SpanBicat.whiskerRight_hom_πₗ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ S₂ : X ⟶ Y} (f : S₁ ⟶ S₂) (S : Y ⟶ Z) {Z✝ : C} (h : S₂.apex ⟶ Z✝) : CategoryStruct.comp (Bicategory.whiskerRight f S).hom (CategoryStruct.comp (πₗ S₂ S) h) = CategoryStruct.comp (πₗ S₁ S) (CategoryStruct.comp f.hom h)

@[simp]

theorem CategoryTheory.Span.SpanBicat.whiskerRight_hom_πᵣ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ S₂ : X ⟶ Y} (f : S₁ ⟶ S₂) (S : Y ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight f S).hom (πᵣ S₂ S) = πᵣ S₁ S

@[simp]

theorem CategoryTheory.Span.SpanBicat.whiskerRight_hom_πᵣ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y Z : SpanBicat C Wₗ Wᵣ} {S₁ S₂ : X ⟶ Y} (f : S₁ ⟶ S₂) (S : Y ⟶ Z) {Z✝ : C} (h : S.apex ⟶ Z✝) : CategoryStruct.comp (Bicategory.whiskerRight f S).hom (CategoryStruct.comp (πᵣ S₂ S) h) = CategoryStruct.comp (πᵣ S₁ S) h

@[simp]

theorem CategoryTheory.Span.SpanBicat.associator_hom_hom_πₗ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {W X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : W ⟶ X) (S₂ : X ⟶ Y) (S₃ : Y ⟶ Z) : CategoryStruct.comp (Bicategory.associator S₁ S₂ S₃).hom.hom (πₗ S₁ (CategoryStruct.comp S₂ S₃)) = CategoryStruct.comp (πₗ (CategoryStruct.comp S₁ S₂) S₃) (πₗ S₁ S₂)

@[simp]

theorem CategoryTheory.Span.SpanBicat.associator_hom_hom_πₗ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {W X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : W ⟶ X) (S₂ : X ⟶ Y) (S₃ : Y ⟶ Z) {Z✝ : C} (h : S₁.apex ⟶ Z✝) : CategoryStruct.comp (Bicategory.associator S₁ S₂ S₃).hom.hom (CategoryStruct.comp (πₗ S₁ (CategoryStruct.comp S₂ S₃)) h) = CategoryStruct.comp (πₗ (CategoryStruct.comp S₁ S₂) S₃) (CategoryStruct.comp (πₗ S₁ S₂) h)

@[simp]

theorem CategoryTheory.Span.SpanBicat.associator_hom_hom_πᵣ_πₗ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {W X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : W ⟶ X) (S₂ : X ⟶ Y) (S₃ : Y ⟶ Z) : CategoryStruct.comp (Bicategory.associator S₁ S₂ S₃).hom.hom (CategoryStruct.comp (πᵣ S₁ (CategoryStruct.comp S₂ S₃)) (πₗ S₂ S₃)) = CategoryStruct.comp (πₗ (CategoryStruct.comp S₁ S₂) S₃) (πᵣ S₁ S₂)

@[simp]

theorem CategoryTheory.Span.SpanBicat.associator_hom_hom_πᵣ_πₗ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {W X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : W ⟶ X) (S₂ : X ⟶ Y) (S₃ : Y ⟶ Z) {Z✝ : C} (h : S₂.apex ⟶ Z✝) : CategoryStruct.comp (Bicategory.associator S₁ S₂ S₃).hom.hom (CategoryStruct.comp (πᵣ S₁ (CategoryStruct.comp S₂ S₃)) (CategoryStruct.comp (πₗ S₂ S₃) h)) = CategoryStruct.comp (πₗ (CategoryStruct.comp S₁ S₂) S₃) (CategoryStruct.comp (πᵣ S₁ S₂) h)

@[simp]

theorem CategoryTheory.Span.SpanBicat.associator_hom_hom_πᵣ_πᵣ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {W X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : W ⟶ X) (S₂ : X ⟶ Y) (S₃ : Y ⟶ Z) : CategoryStruct.comp (Bicategory.associator S₁ S₂ S₃).hom.hom (CategoryStruct.comp (πᵣ S₁ (CategoryStruct.comp S₂ S₃)) (πᵣ S₂ S₃)) = πᵣ (CategoryStruct.comp S₁ S₂) S₃

@[simp]

theorem CategoryTheory.Span.SpanBicat.associator_hom_hom_πᵣ_πᵣ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {W X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : W ⟶ X) (S₂ : X ⟶ Y) (S₃ : Y ⟶ Z) {Z✝ : C} (h : S₃.apex ⟶ Z✝) : CategoryStruct.comp (Bicategory.associator S₁ S₂ S₃).hom.hom (CategoryStruct.comp (πᵣ S₁ (CategoryStruct.comp S₂ S₃)) (CategoryStruct.comp (πᵣ S₂ S₃) h)) = CategoryStruct.comp (πᵣ (CategoryStruct.comp S₁ S₂) S₃) h

@[simp]

theorem CategoryTheory.Span.SpanBicat.associator_inv_hom_πᵣ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {W X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : W ⟶ X) (S₂ : X ⟶ Y) (S₃ : Y ⟶ Z) : CategoryStruct.comp (Bicategory.associator S₁ S₂ S₃).inv.hom (πᵣ (CategoryStruct.comp S₁ S₂) S₃) = CategoryStruct.comp (πᵣ S₁ (CategoryStruct.comp S₂ S₃)) (πᵣ S₂ S₃)

@[simp]

theorem CategoryTheory.Span.SpanBicat.associator_inv_hom_πᵣ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {W X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : W ⟶ X) (S₂ : X ⟶ Y) (S₃ : Y ⟶ Z) {Z✝ : C} (h : S₃.apex ⟶ Z✝) : CategoryStruct.comp (Bicategory.associator S₁ S₂ S₃).inv.hom (CategoryStruct.comp (πᵣ (CategoryStruct.comp S₁ S₂) S₃) h) = CategoryStruct.comp (πᵣ S₁ (CategoryStruct.comp S₂ S₃)) (CategoryStruct.comp (πᵣ S₂ S₃) h)

@[simp]

theorem CategoryTheory.Span.SpanBicat.associator_inv_hom_πₗ_πₗ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {W X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : W ⟶ X) (S₂ : X ⟶ Y) (S₃ : Y ⟶ Z) : CategoryStruct.comp (Bicategory.associator S₁ S₂ S₃).inv.hom (CategoryStruct.comp (πₗ (CategoryStruct.comp S₁ S₂) S₃) (πₗ S₁ S₂)) = πₗ S₁ (CategoryStruct.comp S₂ S₃)

@[simp]

theorem CategoryTheory.Span.SpanBicat.associator_inv_hom_πₗ_πₗ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {W X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : W ⟶ X) (S₂ : X ⟶ Y) (S₃ : Y ⟶ Z) {Z✝ : C} (h : S₁.apex ⟶ Z✝) : CategoryStruct.comp (Bicategory.associator S₁ S₂ S₃).inv.hom (CategoryStruct.comp (πₗ (CategoryStruct.comp S₁ S₂) S₃) (CategoryStruct.comp (πₗ S₁ S₂) h)) = CategoryStruct.comp (πₗ S₁ (CategoryStruct.comp S₂ S₃)) h

@[simp]

theorem CategoryTheory.Span.SpanBicat.associator_inv_hom_πₗ_πᵣ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {W X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : W ⟶ X) (S₂ : X ⟶ Y) (S₃ : Y ⟶ Z) : CategoryStruct.comp (Bicategory.associator S₁ S₂ S₃).inv.hom (CategoryStruct.comp (πₗ (CategoryStruct.comp S₁ S₂) S₃) (πᵣ S₁ S₂)) = CategoryStruct.comp (πᵣ S₁ (CategoryStruct.comp S₂ S₃)) (πₗ S₂ S₃)

@[simp]

theorem CategoryTheory.Span.SpanBicat.associator_inv_hom_πₗ_πᵣ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {W X Y Z : SpanBicat C Wₗ Wᵣ} (S₁ : W ⟶ X) (S₂ : X ⟶ Y) (S₃ : Y ⟶ Z) {Z✝ : C} (h : S₂.apex ⟶ Z✝) : CategoryStruct.comp (Bicategory.associator S₁ S₂ S₃).inv.hom (CategoryStruct.comp (πₗ (CategoryStruct.comp S₁ S₂) S₃) (CategoryStruct.comp (πᵣ S₁ S₂) h)) = CategoryStruct.comp (πᵣ S₁ (CategoryStruct.comp S₂ S₃)) (CategoryStruct.comp (πₗ S₂ S₃) h)

@[simp]

theorem CategoryTheory.Span.SpanBicat.leftUnitor_hom_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) : (Bicategory.leftUnitor S).hom.hom = πᵣ (CategoryStruct.id X) S

@[simp]

theorem CategoryTheory.Span.SpanBicat.leftUnitor_inv_hom_πₗ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) : CategoryStruct.comp (Bicategory.leftUnitor S).inv.hom (πₗ (CategoryStruct.id X) S) = S.l

@[simp]

theorem CategoryTheory.Span.SpanBicat.leftUnitor_inv_hom_πᵣ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) : CategoryStruct.comp (Bicategory.leftUnitor S).inv.hom (πᵣ (CategoryStruct.id X) S) = CategoryStruct.id S.apex

@[simp]

theorem CategoryTheory.Span.SpanBicat.rightUnitor_hom_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) : (Bicategory.rightUnitor S).hom.hom = πₗ S (CategoryStruct.id Y)

@[simp]

theorem CategoryTheory.Span.SpanBicat.rightUnitor_inv_hom_πₗ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) : CategoryStruct.comp (Bicategory.rightUnitor S).inv.hom (πₗ S (CategoryStruct.id Y)) = CategoryStruct.id S.apex

@[simp]

theorem CategoryTheory.Span.SpanBicat.rightUnitor_inv_hom_πₗ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) {Z : C} (h : S.apex ⟶ Z) : CategoryStruct.comp (Bicategory.rightUnitor S).inv.hom (CategoryStruct.comp (πₗ S (CategoryStruct.id Y)) h) = h

@[simp]

theorem CategoryTheory.Span.SpanBicat.rightUnitor_inv_hom_πᵣ {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) : CategoryStruct.comp (Bicategory.rightUnitor S).inv.hom (πᵣ S (CategoryStruct.id Y)) = S.r

@[simp]

theorem CategoryTheory.Span.SpanBicat.rightUnitor_inv_hom_πᵣ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) {Z : C} (h : (CategoryStruct.id Y).apex ⟶ Z) : CategoryStruct.comp (Bicategory.rightUnitor S).inv.hom (CategoryStruct.comp (πᵣ S (CategoryStruct.id Y)) h) = CategoryStruct.comp S.r h

@[simp]

theorem CategoryTheory.Span.SpanBicat.hom_inv_id_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} (e : S ≅ S') : CategoryStruct.comp e.hom.hom e.inv.hom = CategoryStruct.id S.apex

@[simp]

theorem CategoryTheory.Span.SpanBicat.hom_inv_id_hom_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} (e : S ≅ S') {Z : C} (h : S.apex ⟶ Z) : CategoryStruct.comp e.hom.hom (CategoryStruct.comp e.inv.hom h) = h

@[simp]

theorem CategoryTheory.Span.SpanBicat.inv_hom_id_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} (e : S ≅ S') : CategoryStruct.comp e.inv.hom e.hom.hom = CategoryStruct.id S'.apex

@[simp]

theorem CategoryTheory.Span.SpanBicat.inv_hom_id_hom_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} (e : S ≅ S') {Z : C} (h : S'.apex ⟶ Z) : CategoryStruct.comp e.inv.hom (CategoryStruct.comp e.hom.hom h) = h

@[reducible, inline]

abbrev CategoryTheory.Span.SpanBicat.apexIso {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} (e : S ≅ S') : S.apex ≅ S'.apex

Extract the isomorphism between the apices from the data of an isomorphism of 1-morphisms in SpanBicat C _ _.

Equations

• CategoryTheory.Span.SpanBicat.apexIso e = { hom := e.hom.hom, inv := e.inv.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Span.SpanBicat.apexIso_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} (e : S ≅ S') : (apexIso e).hom = e.hom.hom

@[simp]

theorem CategoryTheory.Span.SpanBicat.apexIso_inv {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} (e : S ≅ S') : (apexIso e).inv = e.inv.hom

@[simp]

theorem CategoryTheory.Span.SpanBicat.apexIso_refl {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) : apexIso (Iso.refl S) = Iso.refl S.apex

instance CategoryTheory.Span.SpanBicat.instIsIsoHomOfHom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} (e : S ⟶ S') [IsIso e] : IsIso e.hom

@[simp]

theorem CategoryTheory.Span.SpanBicat.inv_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} {S S' : X ⟶ Y} (e : S ⟶ S') [IsIso e] : (inv e).hom = inv e.hom

theorem CategoryTheory.Span.SpanBicat.eqToHom_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S S' : X ⟶ Y) (h : S = S') : (eqToHom h).hom = eqToHom ⋯

instance CategoryTheory.Span.SpanBicat.instIsIsoRId {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X : SpanBicat C Wₗ Wᵣ} : IsIso (CategoryStruct.id X).r

instance CategoryTheory.Span.SpanBicat.instIsIsoLId {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X : SpanBicat C Wₗ Wᵣ} : IsIso (CategoryStruct.id X).l

instance CategoryTheory.Span.SpanBicat.instIsIsoπᵣId {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) : IsIso (πᵣ (CategoryStruct.id X) S)

instance CategoryTheory.Span.SpanBicat.instIsIsoπₗId {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {X Y : SpanBicat C Wₗ Wᵣ} (S : X ⟶ Y) : IsIso (πₗ S (CategoryStruct.id Y))