proposition: Lemma is_limit_plc : is_limit plc.
proof: Proof. uhg; ee. uhg; ee; ir. ap is_cone_plc. rw (for_uni_plc H). rw H1. wr for_uni_plc. tv. am. uhg; ee. ap is_cone_plc. ir. sh (our_map b0). rwi socle_plc H0. cp (versal_summary H H0). ee. uhg; ee. ap is_cone_plc. rww cone_target_plc. rww vertex_plc. am. Qed.
imports: Arith colimits functor_cat