English
Explicit inclusions into the object map from the two-step construction F and G at indices i₂, i₃ yield a canonical morphism between the composite object and the mapped object.
Русский
Явные включения в отображение объектов из двухступенчатой конструкции F и G по индексам i₂, i₃ дают каноническую морфизм между составным объектом и отображённым объектом.
LaTeX
$$$$ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i_1 i_2 i_3 j h : (F.obj (X_1 i_1)).obj ((G₂₃.obj (X_2 i_2)).obj (X_3 i_3)) \to mapBifunctorMapObj F ρ₂₃.q X_1 (mapBifunctorMapObj G₂₃ ρ₂₃.p X_2 X_3) j$$$$
Lean4
/-- The cofan consisting of the inclusions given by `ιMapBifunctorBifunctor₂₃MapObj`. -/
noncomputable def cofan₃MapBifunctorBifunctor₂₃MapObj (j : J) :
((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).CofanMapObjFun r j :=
Cofan.mk (mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
(fun ⟨⟨i₁, i₂, i₃⟩, (hi : r ⟨i₁, i₂, i₃⟩ = j)⟩ => ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi)
