proposition: Lemma vertex_other_pt : forall y, ob a y -> vertex (other_pt y) = fob otherv y.
proof: Proof. ir. uf other_pt. rw vertex_cone_pushdown. rw fob_point_functor. tv. am. am. wr cone_target_other. app Limit.ob_vertex. am. Qed.
imports: Arith colimits functor_cat