proposition: Lemma mor_functor_cat : forall a b u, Category.axioms a -> Category.axioms b -> mor (functor_cat a b) u = nt2hom a b u.
proof: Proof. ir. app iff_eq; ir. wr is_mor_functor_cat. lu. uhg; ee. app functor_cat_axioms. rww is_mor_functor_cat. Qed.
imports: Arith nat_trans