proposition: Lemma is_cone_newcone : forall u, mor a u -> is_cone (newcone u).
proof: Proof. ir. uf newcone. ap is_cone_cone_transform. uhg; ee. ap is_cone_pointl. rww ob_source. ap htrans_right_axioms. am. ap point_trans_axioms. am. am. rw osource_point_trans. sy; am. rw socle_pointl. rw source_htrans_right. rw source_point_trans. uf pointf. tv. rww ob_source; am. Qed.
imports: Arith colimits functor_cat