proposition: Lemma mor_our_map : mor (functor_cat a b) our_map.
proof: Proof. rw mor_functor_cat. uf our_map. uhg; ee. ap create_axioms. uhg; ee. ap axioms_otherv. ap plv_axioms. ir. uf our_mval. rww source_otherv. rww source_plv. rw target_otherv; rww target_plv. ir. rwi source_otherv H. uf our_mval. ap mor_cone_to_limit. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt; rww socle_pointl. rww cone_target_pointl. rww target_plv. ir. rwi source_otherv H. rww source_our_mval. ir. rwi source_otherv H. rww target_our_mval. rww fob_plv. ir. rwi source_otherv H. rw target_plv. sy; app our_mval_carre. rw osource_create. rww source_otherv. rw otarget_create. rww target_plv. am. am. Qed.
imports: Arith colimits functor_cat