proposition: Lemma axioms_otherv : Functor.axioms otherv.
proof: Proof. uf otherv. assert (ob (functor_cat a b) otherv). wr cone_target_other. uf otherv. app Limit.ob_vertex. rwi ob_functor_cat H. lu. am. am. Qed.
imports: Arith colimits functor_cat