∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {S S' : C} (q : S' ⟶ S) (T : (CategoryTheory.Over S')ᵒᵖ),
  CategoryTheory.CategoryStruct.comp q.op.toLoc (Opposite.unop T).hom.op.toLoc =
    ((CategoryTheory.Over.map q).obj (Opposite.unop T)).hom.op.toLoc