proposition: Lemma pointwise_same : forall y, ob a y -> ntrans another_map y = our_mval y.
proof: Proof. ir. assert (lem0: Nat_Trans.axioms another_map). cp mor_another. rwi mor_functor_cat H0. lu. am. am. assert (lem1: is_uni (pointl y)). cp (is_limit_pointl H). lu. uh lem1. ee. ap H1. uhg; ee. app is_cone_pointl. rw cone_target_pointl. ap mor_ntrans. am. rw osource_another. am. rww otarget_another. am. rw target_ntrans. rw target_another. rw fob_plv. rww vertex_pointl. am. am. rww osource_another. uhg; ee. app is_cone_pointl. rww cone_target_pointl. uf our_mval. ap mor_cone_to_limit. app is_cone_other_pt. app is_limit_pointl. rw socle_other_pt. rw socle_pointl. reflexivity. am. am. rww cone_target_pointl. rw target_our_mval. rw vertex_pointl. tv. am. ap cone_extensionality. rww is_cone_cone_compose. uhg; ee. app is_cone_pointl. rww cone_target_pointl. uf our_mval. ap mor_ntrans. am. rww osource_another. rww otarget_another. rww target_ntrans. rww target_another. rw fob_plv. rww vertex_pointl. am. rww osource_another. rww is_cone_cone_compose. uhg; ee. app is_cone_pointl. rww cone_target_pointl. uf our_mval. ap mor_cone_to_limit. app is_cone_other_pt. app is_limit_pointl. rw socle_other_pt. rw socle_pointl. reflexivity. am. am. rww cone_target_pointl. rww target_our_mval. rw vertex_cone_compose. rw vertex_cone_compose. rw source_ntrans. rw source_another. rw source_our_mval. reflexivity. am. am. rww osource_another. rw socle_cone_compose. rw socle_cone_compose. reflexivity. ir. rwi cone_source_cone_compose H2. rwi cone_source_pointl H2. wrr ntrans_edge_other. rw edge_cone_compose. rw cone_target_pointl. 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. rww socle_other_pt; rww socle_pointl. rww cone_target_pointl. rww cone_source_pointl. am. rww cone_source_pointl. uhg; ee. app is_cone_pointl. rww cone_target_pointl. uf our_mval. ap mor_cone_to_limit. app is_cone_other_pt. app is_limit_pointl. rw socle_other_pt. rw socle_pointl. reflexivity. am. am. rww cone_target_pointl. rww target_our_mval. am. Qed.
imports: Arith colimits functor_cat