eqToHom_app — Mathlib

English

Equality of morphisms in Cat is compatible with app at objects under eqToHom.

Русский

Равенство морфизмов в Cat совместимо с действием app на объекты через eqToHom.

LaTeX

$$$$\\forall F,G: C \\to D, \\; h:F=G \\Rightarrow (h).\\_\\text{app} = \\text{eqToHom}(\\dots).$$$$

Lean4

@[simp]
theorem eqToHom_app {C D : Cat} (F G : C ⟶ D) (h : F = G) (X : C) :
    (eqToHom h).app X = eqToHom (Functor.congr_obj h X) :=
  CategoryTheory.eqToHom_app h X

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