English
Two morphisms f and g from the same source factor through the universal family that defines ιMapBifunctorBifunctor₂₃MapObj; their equality is controlled by the cofinal description of the colimit.
Русский
Два морфизма f и g из одного и того же источника факторизуются через описатель-универсал, задающий ιMapBifunctorBifunctor₂₃MapObj; их равенство управляется описанием колимита.
LaTeX
$$$$f = g \\;\\Rightarrow\\; ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i_1 i_2 i_3 j h = ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i_1 i_2 i_3 j h$$$$
Lean4
/-- The inclusion of `(F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃))` in
`mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j`
when `r (i₁, i₂, i₃) = j`. -/
noncomputable def ιMapBifunctorBifunctor₂₃MapObj (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
(F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶
mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j :=
(F.obj (X₁ i₁)).map (ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ _ rfl) ≫
ιMapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ (ρ₂₃.p ⟨i₂, i₃⟩) j (by rw [← h, ← ρ₂₃.hpq])
