Lean/Mathlib: functors from a connected groupoid to SingleObj G = conjugacy classes

To classify C ⥤ SingleObj G up to iso for a connected groupoid C, restrict to Mathlib's End c (a structure with .asHom, mul f g = .of (g.asHom ≫ f.asHom)). SingleObj.comp_as_mul : f ≫ g = g * f uses the same order, so γ ↦ F.map γ.asHom is a genuine End c →* G with no MulOpposite. The inverse is f ↦ φ (.of (p x ≫ f ≫ inv (p y))) for chosen p x : c ⟶ x, and its restriction is conjugate to φ, so you never need p c = 𝟙. Gotcha: rw [F.map_inv] and IsIso.hom_inv_id fail to match inv in a groupoid (instance mismatch). Prove F.map (inv f) = (F.map f)⁻¹ as eq_inv_of_mul_eq_one_left (by rw [← SingleObj.comp_as_mul, ← F.map_comp]; simp [SingleObj.id_as_one]), then let the group tactic finish the naturality algebra. Also: SingleObj G : Type always, so statements involving BG are stuck in universe 0.