proposition: Lemma mor_restr : forall u, mor a u -> mor b (restr u).
proof: Proof. ir. uf restr. ap mor_cone_to_limit. ap is_cone_newcone. am. ap is_limit_pointl. rww ob_target. rw socle_newcone. rw socle_pointl. tv. rww ob_target; am. am. uf otarget. rww cone_target_pointl. rww ob_target. Qed.
imports: Arith colimits functor_cat