proposition: Lemma functor_umorphism_axioms : forall f, axioms f -> Umorphism.axioms f.
proof: Proof. ir. uhg; ee. uhg; ee. uhg; ee. ir. change (is_mor (target f) (fmor f x)). change (is_mor (source f) x) in H0. assert (mor (target f) (fmor f x)). ap mor_fmor. am. ap is_mor_mor. lu. am. lu. Qed.
imports: Arith category