proposition: Lemma invertible_commutation_plc : forall y, ob a y -> invertible b (commutation (point_functor a b y) plc (pointl y)).
proof: Proof. ir. assert (b = target (point_functor a b y)). rww target_point_functor. set (k:=point_functor a b y). rw H0. uf k. rw invertible_commutation_is_limit_cone_pushdown. rw cone_pushdown_point_functor_plc. app is_limit_pointl. am. ap is_cone_plc. app is_limit_pointl. rww source_point_functor. rww cone_target_plc. app point_functor_axioms. rw socle_plc. rww socle_pointl. tv. Qed.
imports: Arith colimits functor_cat