∀ {G : Type v} [inst : Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u))
  (a : MulAction.orbitRel.Quotient G (J.obj (CategoryTheory.SingleObj.star G))),
  (CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient J).symm a =
    (CategoryTheory.Limits.Types.colimitEquivColimitType J).symm
      (Quot.lift (fun x => Quot.mk J.ColimitTypeRel ⟨CategoryTheory.SingleObj.star G, x⟩) ⋯ a)