proposition: Lemma pointf_axioms : forall x, ob a x -> Functor.axioms (pointf x).
proof: Proof. ir. uf pointf. ap fcompose_axioms. app point_functor_axioms. am. rww source_point_functor. sy; am. Qed.
imports: Arith colimits functor_cat