∀ {U : Type u_1} {V : Type u_2} {inst : Quiver U} {inst_1 : Quiver V} {inst_2 : Quiver.HasReverse U}
  {inst_3 : Quiver.HasReverse V} {φ : U ⥤q V} [self : φ.MapReverse] {u v : U} (e : u ⟶ v),
  φ.map (Quiver.reverse e) = Quiver.reverse (φ.map e)