objEqToHom_refl — Mathlib

English

In a differential object, the naturality of objEqToHom with respect to changing index is coherent with the differential d

Русский

В дифференциальном объекте естественность objEqToHom относительно смены индекса согласована с дифференциалом d.

LaTeX

$$$\forall x,y,\; X.objEqToHom h \;\circ\; X.d y = X.d x \;\circ\; X.objEqToHom h$ for h: x = y$$

Lean4

@[simp]
theorem objEqToHom_refl (i : β) : X.objEqToHom (refl i) = 𝟙 _ :=
  rfl

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