proposition: Lemma source_restr : forall u, mor a u -> source (restr u) = pointv (source u).
proof: Proof. ir. uf restr. rw source_cone_to_limit. rw vertex_newcone. tv. am. ap is_cone_newcone. am. ap is_limit_pointl. rww ob_target. rw socle_newcone. rw socle_pointl. tv. rww ob_target. am. Qed.
imports: Arith colimits functor_cat