English
The inclusions ιMapTrifunctorMapObj satisfy extensionality: two morphisms from mapTrifunctorMapObj F p X₁ X₂ X₃ j are equal if they agree after precomposition with every component ιMapTrifunctorMapObj.
Русский
Инклюзии ιMapTrifunctorMapObj удовлетворяют экстенсиональности: морфизмы из mapTrifunctorMapObj равны, если совпадают после предварительной композиции с каждым компонентом ιMapTrifunctorMapObj.
LaTeX
$$$\forall f,g:\, mapTrifunctorMapObj F p X_1 X_2 X_3 j \to Y,\; (\forall i_1,i_2,i_3,h,\; ιMapTrifunctorMapObj F p X_1 X_2 X_3 i_1 i_2 i_3 j h ≫ f = ιMapTrifunctorMapObj F p X_1 X_2 X_3 i_1 i_2 i_3 j h ≫ g) \Rightarrow f=g$$$
Lean4
/-- The maps `mapTrifunctorMapObj F p X₁ X₂ X₃ ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃` which
express the functoriality of `mapTrifunctorMapObj`, see `mapTrifunctorMap` -/
noncomputable def mapTrifunctorMapMap {X₁ Y₁ : GradedObject I₁ C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : GradedObject I₂ C₂}
(f₂ : X₂ ⟶ Y₂) {X₃ Y₃ : GradedObject I₃ C₃} (f₃ : X₃ ⟶ Y₃)
[HasMap ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃) p]
[HasMap ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃) p] :
mapTrifunctorMapObj F p X₁ X₂ X₃ ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ :=
GradedObject.mapMap
((((mapTrifunctor F I₁ I₂ I₃).map f₁).app X₂).app X₃ ≫
(((mapTrifunctor F I₁ I₂ I₃).obj Y₁).map f₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).map f₃)
p
