proposition: Lemma invertible_commutation_point_functor_limit : forall y, ob a y -> invertible b (commutation (point_functor a b y) (limit f) (pointl y)).
proof: Proof. ir. rw invertible_commutation_is_limit_cone_pushdown. ap is_limit_cone_pushdown_point_functor. am. assert (is_limit (limit f)). app is_limit_limit. ap presheaf_limit_criterion. lu. app is_limit_pointl. rww source_point_functor. uf cone_target. rww socle_limit. sy; am. ap presheaf_limit_criterion. app point_functor_axioms. rww socle_limit. rww socle_pointl. ap presheaf_limit_criterion. rww target_point_functor. Qed.
imports: Arith colimits functor_cat