Limit-creating functor

A functor creates categorical limits of a specified shape when every given limiting categorical cone over an image diagram uniquely lifts to a categorical cone over the original diagram, and the lift is limiting. This is stronger than just being a limit-reflecting functor. Forgetting arrows from a functor category creates its pointwise limits in a functor category.

An equivalence-invariant lifting property permits the underlying cone of the lift to be identified with the chosen cone by an isomorphism, rather than requiring literal equality. Lifts are unique up to a unique isomorphism compatible with that identification. A monadic adjunction defined by equivalence of its comparison functor has this property by monad algebra forgetful functor creates limits. Literal creation follows if the comparison is an isomorphism over the base, or suitable strict transport of objects is part of the convention. An equivalence alone does not guarantee a literally prescribed underlying object lies in the image.