proposition: Lemma funtyd_axioms : forall d (f:fun_type_data d), funtyd_property f -> Functor.axioms (funtyd f).
proof: Proof. ir. uhg; ee. uf funtyd. uf Functor.create. ap Umorphism.create_like. rw source_funtyd. ap catyd_axioms. uh H; ee; am. rw target_funtyd. uh H; ee; am. ir. rwi source_funtyd H0. rw target_funtyd. cp (R_ob_lift H0). wr H1. rw fob_funtyd_R. uh H; ee. ap H3. am. ir. rwi source_funtyd H0. rw target_funtyd. rw source_funtyd. cp (R_ob_lift H0). wr H1. rw fob_funtyd_R. rw id_catyd_R. rw fmor_funtyd_catyd_arrow. uh H; ee. ap H7. am. uh H; ee; am. am. ir. rwi source_funtyd H0. rw target_funtyd. cp (catyd_arrow_mor_lift H0). wr H1. rw fmor_funtyd_catyd_arrow. uh H; ee. ap H4. am. ir. rwi source_funtyd H0. cp (catyd_arrow_mor_lift H0). wr H1. rw fmor_funtyd_catyd_arrow. rw source_catyd_arrow. rw fob_funtyd_R. uh H; ee. ap H5. am. am. ir. rwi source_funtyd H0. cp (catyd_arrow_mor_lift H0). wr H1. rw fmor_funtyd_catyd_arrow. rw target_catyd_arrow. rw fob_funtyd_R. uh H; ee. ap H6. am. am. rw source_funtyd. rw target_funtyd. ir. cp (catyd_arrow_mor_lift H0). cp (catyd_arrow_mor_lift H1). wr H3; wr H4. rw fmor_funtyd_catyd_arrow. rw fmor_funtyd_catyd_arrow. rw comp_catyd_catyd_arrow. rw fmor_funtyd_catyd_arrow. uh H; ee. ap H11. ap R_inj. rw R_srcy_mor_lift. rw R_trgy_mor_lift. am. am. uh H; ee; am. ap R_inj. rw R_srcy_mor_lift. rw R_trgy_mor_lift. am. am. am. Qed.
imports: Arith cat_examples cardinal fc_limits