proposition: Lemma nttyd_ntrans_R : forall d (f g:fun_type_data d) u, Nat_Trans.axioms u -> funtyd_property f -> funtyd_property g -> source u = funtyd f -> target u = funtyd g -> nttyd f g (fun (x:obsy d) => ntrans u (R x)) = u.
proof: Proof. ir. assert (lem0:catyd_property d). uh H0; ee; am. assert (lem1 : ft f = otarget u). wr target_source. rw H2. rww target_funtyd. am. assert (lem2 : ft g = otarget u). uf otarget. rw H3. rww target_funtyd. assert (lem3 : osource u = catyd d). uf osource. rw H2. rww source_funtyd. ap Nat_Trans.axioms_extensionality. ap nttyd_axioms. app nttyd_property_ntrans_R. am. rw source_nttyd. sy; am. rw target_nttyd. sy; am. ir. rwi osource_nttyd H4. cp H4. rwi ob_catyd H5. nin H5. rw H5. rw ntrans_nttyd_R. tv. am. am. Qed.
imports: Arith cat_examples cardinal fc_limits