proposition: Lemma is_cone_other_pt : forall y, ob a y -> is_cone (other_pt y).
proof: Proof. ir. uf other_pt. ap is_cone_cone_pushdown. am. app point_functor_axioms. rww source_point_functor. rww cone_target_other. Qed.
imports: Arith colimits functor_cat