proposition: Lemma catyd_arrow_idy_ob_lift : forall d x (H:ob (catyd d) x), catyd_arrow (idy (ob_lift H)) = id (catyd d) x.
proof: Proof. ir. cp (R_ob_lift H). assert (id (catyd d) x = id (catyd d) (R (ob_lift H))). rww H0. rw H1. uf catyd. rw Category.id_create. rw catyd_id_R. tv. rw H0. cp H. app inc_obsy. Qed.
imports: Arith cat_examples cardinal fc_limits