proposition: Lemma funtyd_fmor_funtyd_lift : forall d g u, Functor.axioms g -> catyd_property d -> source g = catyd d -> mor (source g) u -> funtyd_fmor (funtyd_lift d g) u = fmor g u.
proof: Proof. ir. uf funtyd_fmor. cp H2. rwi H1 H3. rwi mor_catyd H3. nin H3. rw H3. rw arrow_catyd_arrow. rw X_rewrite. rw fm_funtyd_lift. tv. am. Qed.
imports: Arith cat_examples cardinal fc_limits