∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] (T : CategoryTheory.Functor C₁ C₂) (X : C₁),
  (CategoryTheory.CatCommSq.iso T (CategoryTheory.Functor.id C₁) (CategoryTheory.Functor.id C₂) T).inv.app X =
    CategoryTheory.CategoryStruct.id (T.obj X)