liftHom₂_congr — Mathlib

English

In the free bicategory, liftHom₂ is constant on related Hom₂ data: if η and θ are related, then liftHom₂ F η = liftHom₂ F θ.

Русский

В свободной биокатегории отображение liftHom₂ по двум данным Hom₂ одинаково, если эти данные связаны отношением Rel.

LaTeX

$$$Rel(\eta, \theta) \implies \mathrm{liftHom}_2 F \eta = \mathrm{liftHom}_2 F \theta$$$

Lean4

theorem liftHom₂_congr {a b : FreeBicategory B} {f g : a ⟶ b} {η θ : Hom₂ f g} (H : Rel η θ) :
    liftHom₂ F η = liftHom₂ F θ := by induction H <;> (dsimp [liftHom₂]; cat_disch)

Похожие утверждения