Heterogeneous multiplication of chain colimits

The colimit multiplication of ChainAlgebra generalises to three chains: stagewise multiplications B i ⊗ C j ⟶ F (i + 1 + j) compatible with the three transition families assemble into a morphism chainColimit B δB ⊗ chainColimit C δC ⟶ chainColimit F δF. The construction is the two-pass colimit.desc of the homogeneous case, verbatim up to the substitution of the three chains: partial cocones against a fixed stage of C in the second slot, then the total cocone over the second slot through the preservation isomorphisms. The defining equation on a pair of stages is cast-free because the stage inclusions absorb the index transports.

theorem RS.mulHet_chainMap_ι_left {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) {i i' : ℕ} (h : i ≤ i') (j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainMap B δB h) (C j)) (CategoryTheory.CategoryStruct.comp (mu i' j) (chainColimitι F δF (i' + 1 + j))) = CategoryTheory.CategoryStruct.comp (mu i j) (chainColimitι F δF (i + 1 + j))

Multiplying after a chain morphism in the first slot agrees with multiplying first, once both land in the colimit.

theorem RS.mulHet_chainMap_ι_right {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δC : (n : ℕ) → C n ⟶ C (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δC j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δF (i + 1 + j))) (i : ℕ) {j j' : ℕ} (h : j ≤ j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (chainMap C δC h)) (CategoryTheory.CategoryStruct.comp (mu i j') (chainColimitι F δF (i + 1 + j'))) = CategoryTheory.CategoryStruct.comp (mu i j) (chainColimitι F δF (i + 1 + j))

Multiplying after a chain morphism in the second slot agrees with multiplying first, once both land in the colimit.

noncomputable def RS.chainMulHetCocone {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) (j : ℕ) : CategoryTheory.Limits.Cocone ((chainDiagram B δB).comp (CategoryTheory.MonoidalCategory.tensorRight (C j)))

The multiply-then-include maps against a fixed stage of C in the second slot form a cocone on the first chain diagram tensored on the right with that stage.

Equations

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

noncomputable def RS.chainMulHetStage {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] (j : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainColimit B δB) (C j) ⟶ chainColimit F δF

Partial multiplication of the first chain colimit against a fixed stage of C in the second slot.

Equations

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

theorem RS.ι_chainMulHetStage {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainColimitι B δB i) (C j)) (chainMulHetStage B C F δB δF mu hδl j) = CategoryTheory.CategoryStruct.comp (mu i j) (chainColimitι F δF (i + 1 + j))

On a stage, the partial multiplication is multiply-then-include.

theorem RS.ι_chainMulHetStage_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] (i j : ℕ) {Z : E} (h : chainColimit F δF ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainColimitι B δB i) (C j)) (CategoryTheory.CategoryStruct.comp (chainMulHetStage B C F δB δF mu hδl j) h) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (chainColimitι F δF (i + 1 + j)) h)

On a stage, the partial multiplication is multiply-then-include.

theorem RS.chainMulHetStage_natural {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δC : (n : ℕ) → C n ⟶ C (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δC j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δF (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] {j j' : ℕ} (h : j ≤ j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainColimit B δB) (chainMap C δC h)) (chainMulHetStage B C F δB δF mu hδl j') = chainMulHetStage B C F δB δF mu hδl j

The partial multiplications are natural in the stage.

theorem RS.chainMulHetStage_natural_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δC : (n : ℕ) → C n ⟶ C (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δC j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δF (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] {j j' : ℕ} (h : j ≤ j') {Z : E} (h✝ : chainColimit F δF ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainColimit B δB) (chainMap C δC h)) (CategoryTheory.CategoryStruct.comp (chainMulHetStage B C F δB δF mu hδl j') h✝) = CategoryTheory.CategoryStruct.comp (chainMulHetStage B C F δB δF mu hδl j) h✝

The partial multiplications are natural in the stage.

noncomputable def RS.chainMulHetTotalCocone {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δC : (n : ℕ) → C n ⟶ C (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δC j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δF (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.Limits.Cocone ((chainDiagram C δC).comp (CategoryTheory.MonoidalCategory.tensorLeft (chainColimit B δB)))

The partial multiplications form a cocone on the second chain diagram tensored on the left with the first chain colimit.

Equations

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

noncomputable def RS.chainColimitMulHet {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δC : (n : ℕ) → C n ⟶ C (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δC j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δF (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainColimit B δB) (chainColimit C δC) ⟶ chainColimit F δF

The heterogeneous colimit multiplication: the partial multiplications assembled over the second slot.

Equations

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

theorem RS.whiskerLeft_ι_chainColimitMulHet {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δC : (n : ℕ) → C n ⟶ C (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δC j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δF (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainColimit B δB) (chainColimitι C δC j)) (chainColimitMulHet B C F δB δC δF mu hδl hδr) = chainMulHetStage B C F δB δF mu hδl j

On a stage in the second slot, the heterogeneous colimit multiplication is the partial multiplication.

theorem RS.whiskerLeft_ι_chainColimitMulHet_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δC : (n : ℕ) → C n ⟶ C (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δC j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δF (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (j : ℕ) {Z : E} (h : chainColimit F δF ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainColimit B δB) (chainColimitι C δC j)) (CategoryTheory.CategoryStruct.comp (chainColimitMulHet B C F δB δC δF mu hδl hδr) h) = CategoryTheory.CategoryStruct.comp (chainMulHetStage B C F δB δF mu hδl j) h

On a stage in the second slot, the heterogeneous colimit multiplication is the partial multiplication.

theorem RS.ι_tensorHom_chainColimitMulHet {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δC : (n : ℕ) → C n ⟶ C (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δC j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δF (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainColimitι B δB i) (chainColimitι C δC j)) (chainColimitMulHet B C F δB δC δF mu hδl hδr) = CategoryTheory.CategoryStruct.comp (mu i j) (chainColimitι F δF (i + 1 + j))

Defining equation of the heterogeneous colimit multiplication: on a pair of stages it is multiply-then-include.

theorem RS.ι_tensorHom_chainColimitMulHet_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δC : (n : ℕ) → C n ⟶ C (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (C j) ⟶ F (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δB i) (C j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δF (i + 1 + j)) (chainCast F ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δC j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δF (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (i j : ℕ) {Z : E} (h : chainColimit F δF ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainColimitι B δB i) (chainColimitι C δC j)) (CategoryTheory.CategoryStruct.comp (chainColimitMulHet B C F δB δC δF mu hδl hδr) h) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (chainColimitι F δF (i + 1 + j)) h)

Defining equation of the heterogeneous colimit multiplication: on a pair of stages it is multiply-then-include.