proposition: Lemma R_trgy_mor_lift : forall d u (H:mor (catyd d) u), R (trgy (mor_lift H)) = target u.
proof: Proof. ir. cp (catyd_arrow_mor_lift H). assert (target u = target (catyd_arrow (d:=d) (mor_lift H))). rww H0. rw H1. rw target_catyd_arrow. tv. Qed.
imports: Arith cat_examples cardinal fc_limits