proposition: Lemma catyd_arrow_mor_lift : forall d u (H: mor (catyd d) u), catyd_arrow (mor_lift H) = u.
proof: Proof. ir. assert (mor (catyd d) u). am. uh H0; ee. ufi catyd H1. rwi is_mor_create H1. ufi catyd_arrow_set H1. assert (mor_lift H = IM_lift (B H1)). uf mor_lift. apply unIM_lift. ap B_irrelevant. tv. rw H2. rw IM_lift_pr. rw B_eq. tv. Qed.
imports: Arith cat_examples cardinal fc_limits