English
The definition of the composite inclusions ιMapBifunctorBifunctor₂₃MapObj satisfies a convenient equality: there is an equality of two descriptive expressions using the index data and the morphisms ι maps.
Русский
Определение включений для композиции бинарных отображений удовлетворяет удобному равенству: существует равенство двух описательных выражений с использованием данных индексов и отображений ι.
LaTeX
$$$$ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i_1 i_2 i_3 j h = (F.obj (X_1 i_1)).map (ιMapBifunctorMapObj G₂₃ ρ₂₃.p X_2 X_3 i_2 i_3 i_2_3 h_2_3) ≫ ιMapBifunctorMapObj F ρ₂₃.q X_1 (mapBifunctorMapObj G₂₃ ρ₂₃.p X_2 X_3) i_1 (ρ₂₃.p ⟨i_2, i_3⟩) j (by rw [← h, ← h₂₃, ← ρ₂₃.hpq]) $$$$
Lean4
/-- Constructor for morphisms from
`mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j`. -/
noncomputable def mapBifunctor₁₂BifunctorDesc :
mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ A :=
Cofan.IsColimit.desc (isColimitCofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
(fun i ↦ f i.1.1 i.1.2.1 i.1.2.2 i.2)
