proposition: Lemma funtyd_lift_property : forall d g, Functor.axioms g -> catyd_property d -> source g = catyd d -> funtyd_property (funtyd_lift d g).
proof: Proof. ir. uhg; ee; ir. rw ft_funtyd_lift. uh H; ee; am. am. rw ft_funtyd_lift; rw fo_funtyd_lift. ap ob_fob. am. rw H1. ap ob_catyd_R. am. rw ft_funtyd_lift; rw fm_funtyd_lift. ap mor_fmor. am. rw H1. ap mor_catyd_catyd_arrow. am. rw fm_funtyd_lift; rw fo_funtyd_lift. rw source_fmor. ap uneq. rw source_catyd_arrow. tv. am. rw H1. ap mor_catyd_catyd_arrow. am. rw fm_funtyd_lift. rw fo_funtyd_lift. rw target_fmor. rw target_catyd_arrow. tv. am. rw H1. ap mor_catyd_catyd_arrow. am. rw ft_funtyd_lift. rw fo_funtyd_lift. rw fm_funtyd_lift. rw id_fob. rw H1. rw id_catyd_R. reflexivity. am. am. rw H1. ap ob_catyd_R. am. rw ft_funtyd_lift. rw fm_funtyd_lift. rw fm_funtyd_lift. rw comp_fmor. rw fm_funtyd_lift. rw H1. rw comp_catyd_catyd_arrow. tv. am. am. am. rw H1. app mor_catyd_catyd_arrow. rw H1. app mor_catyd_catyd_arrow. rw source_catyd_arrow. rw target_catyd_arrow. rww H2. Qed.
imports: Arith cat_examples cardinal fc_limits