proposition: Lemma target_restr : forall u, mor a u -> target (restr u) = pointv (target u).
proof: Proof. ir. uf restr. rw target_cone_to_limit. tv. 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