proposition: Lemma catyd_arrow_compy_mor_lift : forall d u v (Hu : mor (catyd d) u) (Hv : mor (catyd d) v), source u = target v -> catyd_arrow (compy (mor_lift Hu) (mor_lift Hv)) = comp (catyd d) u v.
proof: Proof. ir. cp (catyd_arrow_mor_lift Hu). cp (catyd_arrow_mor_lift Hv). assert (comp (catyd d) u v = comp (catyd d) (catyd_arrow (d:=d) (mor_lift Hu)) (catyd_arrow (d:=d) (mor_lift Hv))). rw H0; rww H1. rw H2. rw comp_catyd. rw catyd_comp_catyd_arrow. tv. rww H0. rww H1. rw catyd_arrow_mor_lift. rww catyd_arrow_mor_lift. Qed.
imports: Arith cat_examples cardinal fc_limits