proposition: Lemma invertible_cone_to_limit_plc : invertible (functor_cat a b) (cone_to_limit plc (limit f)).
proof: Proof. ir. ap invertible_cone_to_limit. ap is_limit_plc. ap is_limit_limit. ap presheaf_limit_criterion. rww socle_plc. rww socle_limit. ap presheaf_limit_criterion. rww cone_target_plc. Qed.
imports: Arith colimits functor_cat