∀ (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPairᵒᵖ CommRingCat),
  IsLocalHom
    (CommRingCat.Hom.hom (CategoryTheory.Limits.limit.π F (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one)))