proposition: Lemma comp_ntrans_pointl_our_mval : forall x y, ob c x -> ob a y -> comp b (edge (pointl y) x) (our_mval y) = edge (other_pt y) x.
proof: Proof. ir. uf our_mval. rw comp_edge_cone_to_limit. tv. app is_limit_pointl. app is_cone_other_pt. rw socle_other_pt. rw socle_pointl. tv. am. am. rww cone_target_pointl. rww cone_source_pointl. Qed.
imports: Arith colimits functor_cat