proposition: Lemma ntrans_edge_other : forall x y, ob c x -> ob a y -> ntrans (edge other x) y = edge (cone_compose (pointl y) (ntrans another_map y)) x.
proof: Proof. ir. assert (lem1: Nat_Trans.axioms another_map). cp mor_another. rwi mor_functor_cat H1. lu. am. am. wr cone_compose_another. rw edge_cone_compose. rw edge_cone_compose. rw cone_target_plc. rw comp_functor_cat. rw cone_target_pointl. rw ntrans_vcompose. rw edge_plc. rw ntrans_ple. rw otarget_ple. tv. am. am. am. am. rww osource_another. am. am. am. rw edge_plc. rw mor_functor_cat. uhg; ee. ap nat_trans_axioms_ple. am. rww osource_ple. rww otarget_ple. am. am. am. am. rw target_another. rw edge_plc. rww source_ple. am. rww cone_source_pointl. uhg; ee. app is_cone_pointl. rw cone_target_pointl. ap mor_ntrans. am. rww osource_another. rww otarget_another. am. rw target_ntrans. rw target_another. rw vertex_pointl. rw fob_plv. tv. am. am. rw osource_another. am. rww cone_source_plc. uhg; ee. app is_cone_plc. rww cone_target_plc. rww target_another. rww vertex_plc. Qed.
imports: Arith colimits functor_cat