proposition: Lemma ob_functor_cat : forall a b x, Category.axioms a -> Category.axioms b -> ob (functor_cat a b) x = fhom a b x.
proof: Proof. ir. app iff_eq; ir. wr is_ob_functor_cat. lu. uhg; ee. app functor_cat_axioms. rww is_ob_functor_cat. Qed.
imports: Arith nat_trans