∀ {X Y : GrpCat} (f : X ⟶ Y),
  ProfiniteGrp.profiniteCompletion.map f =
    ProfiniteGrp.ProfiniteCompletion.lift
      (CategoryTheory.CategoryStruct.comp f (ProfiniteGrp.ProfiniteCompletion.eta Y))