proposition: Lemma ob_pointv : forall x, ob a x -> ob b (pointv x).
proof: Proof. ir. uf pointv. assert (b = cone_target (pointl x)). uf cone_target. rw socle_pointl. rww target_pointf. am. rw H0. ap Limit.ob_vertex. cp (is_limit_pointl H). lu. Qed.
imports: Arith colimits functor_cat