proposition: Lemma fmor_twoarrow_functor_catyd_arrow :forall a u v (y:morsy twoarrow_data), twoarrow_hypothesis a u v -> fmor (twoarrow_functor a u v) (catyd_arrow y) = match y with i1 => id a (source u) | i2 => id a (target u) | a0 => u | a1 => v end.
proof: Proof. ir. cp (twoarrow_fun_data_property H). uf twoarrow_functor. nin y; rww fmor_funtyd_catyd_arrow. Qed.
imports: Arith cat_examples cardinal fc_limits