English
There is a canonical isomorphism between mapBifunctorMapObj F p X1 Y1 and mapBifunctorMapObj F p X2 Y2 induced by X1 ≅ X2 and Y1 ≅ Y2.
Русский
Существует каноническое изоморфизм между mapBifunctorMapObj F p X1 Y1 и mapBifunctorMapObj F p X2 Y2, индуцированный изоморфизмами X1 ≅ X2 и Y1 ≅ Y2.
LaTeX
$$$mapBifunctorMapObj F p X_1 Y_1 \cong mapBifunctorMapObj F p X_2 Y_2$$$
Lean4
@[reassoc (attr := simp, nolint unusedHavesSuffices)]
theorem ι_mapBifunctorAssociator_hom (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
(mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j =
((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h :=
by
dsimp [mapBifunctorAssociator]
rw [ι_mapBifunctorComp₁₂MapObjIso_inv_assoc, ιMapTrifunctorMapObj, ι_mapMap_assoc,
mapTrifunctorMapNatTrans_app_app_app]
erw [ι_mapBifunctorComp₂₃MapObjIso_hom]
