proposition: Lemma restr_id : forall x, ob a x -> restr (id a x) = id b (pointv x).
proof: Proof. ir. uf restr. rw cone_to_limit_id. rw cone_target_pointl. rw vertex_pointl. rw target_id. tv. am. rw target_id. am. am. uf newcone. wr vident_point_functor. rw htrans_right_vident. rw cone_transform_vident. ap is_limit_pointl. rw source_id. am. am. assert (is_limit (pointl (source (id a x)))). ap is_limit_pointl. rww source_id. rw socle_pointl. rw source_id. tv. am. rww source_id. app is_cone_pointl. rww source_id. ap point_functor_axioms. am. am. am. rw source_point_functor. sy; am. am. am. uf newcone. rww source_id. rww target_id. wr vident_point_functor. rw htrans_right_vident. rw cone_transform_vident. tv. rw socle_pointl. tv. am. app is_cone_pointl. app point_functor_axioms. am. rww source_point_functor. sy; am. am. am. Qed.
imports: Arith colimits functor_cat