∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {X : C}
  (R : F.RepresentableBy X) {X_1 X' : C} (f : X_1 ⟶ X') (g : X' ⟶ X),
  (R.homEquiv.trans Equiv.ulift.symm) (CategoryTheory.CategoryStruct.comp f g) =
    (F.comp CategoryTheory.uliftFunctor.{u_2, u_1}).map f.op ((R.homEquiv.trans Equiv.ulift.symm) g)