proposition: Lemma fcompose_twoarrow_functor : forall a u v f, twoarrow_hypothesis a u v -> Functor.axioms f -> source f = a -> fcompose f (twoarrow_functor a u v) = twoarrow_functor (target f) (fmor f u) (fmor f v).
proof: Proof. ir. ap functor_twoarrow_eq2. app fcompose_axioms. app twoarrow_functor_axioms. rww target_twoarrow_functor. rww source_fcompose. rww source_twoarrow_functor. rww target_fcompose. rww fmor_fcompose. rww fmor_twoarrow_functor_catyd_arrow. app twoarrow_functor_axioms. rww target_twoarrow_functor. rww source_twoarrow_functor. ap mor_twoarrow_cat. rww fmor_fcompose. rww fmor_twoarrow_functor_catyd_arrow. app twoarrow_functor_axioms. rww target_twoarrow_functor. rww source_twoarrow_functor. ap mor_twoarrow_cat. Qed.
imports: Arith cat_examples cardinal fc_limits