proposition: Lemma comp_catyd_catyd_arrow : forall d (u v:morsy d), catyd_property d -> srcy u = trgy v -> comp (catyd d) (catyd_arrow u) (catyd_arrow v) = catyd_arrow (compy u v).
proof: Proof. ir. rw comp_catyd. rw catyd_comp_catyd_arrow. tv. rw mor_catyd. sh u; tv. am. rw mor_catyd. sh v; tv. am. rw source_catyd_arrow. rw target_catyd_arrow. rww H0. Qed.
imports: Arith cat_examples cardinal fc_limits