∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C) (X_1 : D),
  (CategoryTheory.Functor.constCompEvaluationObj D X).hom.app X_1 = CategoryTheory.CategoryStruct.id X_1