English
The congruence is compatible with composition: combining α1, α2 and β1, β2 as trans of isomorphisms yields the composite congruence equal to the composite of the individual congruences.
Русский
Соотношение конгруэнтности совместимо с композициями: если взять α1, α2 и β1, β2 как композиции изоморфизмов, то получаем равенство конгруэнтностей.
LaTeX
$$$\mathrm{eHomCongr}(V, \alpha_1 \mathbin{\vdash} \alpha_2,\ \beta_1 \mathbin{\vdash} \beta_2) = \mathrm{eHomCongr}(V, \alpha_1, \beta_1) \circ \mathrm{eHomCongr}(V, \alpha_2, \beta_2).$$$
Lean4
theorem eHomCongr_trans {X₁ Y₁ X₂ Y₂ X₃ Y₃ : C} (α₁ : X₁ ≅ X₂) (β₁ : Y₁ ≅ Y₂) (α₂ : X₂ ≅ X₃) (β₂ : Y₂ ≅ Y₃) :
eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂) = eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂ := by ext;
simp [eHom_whisker_exchange_assoc]
