proposition: Lemma comp_functor_cat : forall a b u v, Category.axioms a -> Category.axioms b -> mor (functor_cat a b) u -> mor (functor_cat a b) v -> source u = target v -> comp (functor_cat a b) u v = vcompose u v.
proof: Proof. ir. uf functor_cat. rw comp_create. tv. rw inc_nt2_set. wrr mor_functor_cat. rw inc_nt2_set. wrr mor_functor_cat. am. Qed.
imports: Arith nat_trans