proposition: Lemma funtyd_funtyd_lift : forall d g, Functor.axioms g -> catyd_property d -> source g = catyd d -> funtyd (funtyd_lift d g) = g.
proof: Proof. ir. ap Functor.axioms_extensionality. ap funtyd_axioms. app funtyd_lift_property. am. rww source_funtyd. sy; am. rw target_funtyd. rw ft_funtyd_lift. tv. ir. cp H2. rwi source_funtyd H2. rw fmor_funtyd. rww funtyd_fmor_funtyd_lift. rww H1. am. Qed.
imports: Arith cat_examples cardinal fc_limits