congr_whiskerLeft — Mathlib

English

Alternate statement of congruence on left whisker in a bicategory; equality propagates through whiskering.

Русский

Альтернативное утверждение согласованности слева по whisker: равенство распространяется через whiskering.

LaTeX

$$$f \\1 η = eqToHom(·) ≫ f' \\1 η ≫ eqToHom(·)$$$

Lean4

theorem congr_whiskerLeft {x y : B} {f f' : x ⟶ y} (h : f = f') {z : B} {g g' : y ⟶ z} (η : g ⟶ g') :
    f ◁ η = eqToHom (by rw [h]) ≫ f' ◁ η ≫ eqToHom (by rw [h]) :=
  by
  subst h
  simp

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