proposition: Lemma edge_other_pt : forall x y, ob a y -> ob c x -> edge (other_pt y) x = ntrans (edge other x) y.
proof: Proof. ir. uf other_pt. rw edge_cone_pushdown. rw fmor_point_functor. tv. wr cone_target_other. ap mor_edge. rww cone_source_other. am. rww cone_source_other. am. Qed.
imports: Arith colimits functor_cat