∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D} (η : X ⟶ Y) (X_1 : C),
  (CategoryTheory.WithTerminal.equivComma.functor.map η).left.app X_1 = η.app (CategoryTheory.WithTerminal.incl.obj X_1)