proposition: Lemma is_cone_plc : is_cone plc.
proof: Proof. uf plc. ap is_cone_cone_create2. am. rw F2. rw ob_functor_cat. uhg; ee. app plv_axioms. rww source_plv. rww target_plv. am. am. ir. rw F2; rw mor_functor_cat. uhg; ee. app nat_trans_axioms_ple. rww osource_ple. rww otarget_ple. am. am. ir. rww source_ple. ir. rww target_ple. ir. rw F2. rw comp_functor_cat. ap ple_commutation. am. am. am. wr F2; app mor_fmor. rww mor_functor_cat. uhg; ee. app nat_trans_axioms_ple. rww ob_source. rww osource_ple. rww otarget_ple. rww ob_source. rww source_fmor. rww target_ple. Qed.
imports: Arith colimits functor_cat