proposition: Lemma is_limit_cone_pushdown_point_functor : forall y, ob a y -> is_limit (cone_pushdown (point_functor a b y) (limit f)).
proof: Proof. ir. assert (has_limit f). ap presheaf_limit_criterion. apply limit_preservation_invariance with plc. app point_functor_axioms. app is_limit_limit. ap is_limit_plc. rww socle_limit. rww socle_plc. rww source_point_functor. rww cone_target_plc. rww cone_pushdown_point_functor_plc. app is_limit_pointl. Qed.
imports: Arith colimits functor_cat