English
The morphisms ιMapTrifunctorMapObj induce a map between mapTrifunctorMapObj constructions, reflecting the functoriality of the construction with respect to f, g, h.
Русский
Гомоморфизмы ιMapTrifunctorMapObj индуцируют отображение между конструкциями mapTrifunctorMapObj, отражая функториальность по f,g,h.
LaTeX
$$$ιMapTrifunctorMapMap F p f_1 f_2 f_3 j = \text{(composed with appropriate structure morphisms)}$$$
Lean4
/-- The natural isomorphism `mapTrifunctor F I₁ I₂ I₃ ≅ mapTrifunctor F' I₁ I₂ I₃`
induced by a natural isomorphism `F ≅ F` of trifunctors. -/
@[simps]
def mapTrifunctorMapIso (e : F ≅ F') (I₁ I₂ I₃ : Type*) : mapTrifunctor F I₁ I₂ I₃ ≅ mapTrifunctor F' I₁ I₂ I₃
where
hom := mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃
inv := mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃
hom_inv_id := by
ext X₁ X₂ X₃ ⟨i₁, i₂, i₃⟩
dsimp
simp only [← NatTrans.comp_app, e.hom_inv_id, NatTrans.id_app]
inv_hom_id := by
ext X₁ X₂ X₃ ⟨i₁, i₂, i₃⟩
dsimp
simp only [← NatTrans.comp_app, e.inv_hom_id, NatTrans.id_app]
