CommGrpCat.fullyFaithfulForget₂ToGrp =
  { preimage := fun {X Y} f => CommGrpCat.ofHom (GrpCat.Hom.hom f),
    map_preimage := @CommGrpCat.fullyFaithfulForget₂ToGrp._proof_1,
    preimage_map := @CommGrpCat.fullyFaithfulForget₂ToGrp._proof_2 }