proposition: Lemma cone_compose_our_map : cone_compose plc our_map = other.
proof: Proof. ap cone_extensionality. rww is_cone_cone_compose. uhg; ee. ap is_cone_plc. rww cone_target_plc. ap mor_our_map. rww target_our_map. rww vertex_plc. am. rww vertex_cone_compose. rww source_our_map. rww socle_cone_compose. rww socle_other. rww socle_plc. ir. rwi cone_source_cone_compose H. rwi cone_source_plc H. rw edge_cone_compose. rw cone_target_plc. rw comp_functor_cat. ap Nat_Trans.axioms_extensionality. rww vcompose_axioms. rw edge_plc. ap nat_trans_axioms_ple. am. am. cp mor_our_map. rwi mor_functor_cat H0. lu. am. am. rw edge_plc. rw source_ple. rww target_our_map. am. assert (mor (cone_target other) (edge other x)). ap mor_edge. rww cone_source_other. am. rwi cone_target_other H0. rwi mor_functor_cat H0. lu. am. am. rw source_vcompose. rw source_edge. rw source_our_map. tv. rww cone_source_other. am. rw target_vcompose. rw edge_plc. rw target_edge. rw socle_other. rw target_ple. tv. rww cone_source_other. am. am. ir. rwi osource_vcompose H0. ufi osource H0. rwi source_our_map H0. rwi source_otherv H0. rw ntrans_vcompose. rw edge_plc. rw otarget_ple. assert (ntrans our_map x0 = our_mval x0). rww ntrans_our_map. rw H1. rw ntrans_ple. uf our_mval. rw comp_edge_cone_to_limit. rw edge_other_pt. tv. am. am. app is_limit_pointl. app is_cone_other_pt. rw socle_other_pt. rww socle_pointl. am. rww cone_target_pointl. rww cone_source_pointl. am. am. am. am. uf osource. rw source_our_map. rww source_otherv. am. am. rw mor_functor_cat. uhg; ee. rw edge_plc. ap nat_trans_axioms_ple. am. am. rw edge_plc. rww osource_ple. am. rw edge_plc. rww otarget_ple. am. am. am. ap mor_our_map. rw edge_plc. rw target_our_map. rww source_ple. am. rww cone_source_plc. uhg; ee. ap is_cone_plc. rw cone_target_plc. ap mor_our_map. rw target_our_map. rww vertex_plc. Qed.
imports: Arith colimits functor_cat