proposition: Lemma comp_catyd : forall d u v, mor (catyd d) u -> mor (catyd d) v -> source u = target v -> comp (catyd d) u v = catyd_comp d u v.
proof: Proof. ir. uf catyd. rw comp_create. tv. app show_inc_catyd_arrow_set. app show_inc_catyd_arrow_set. am. Qed.
imports: Arith cat_examples cardinal fc_limits