proposition: Lemma fcompose_vee_functor : forall a u v f, vee_hypothesis a u v -> Functor.axioms f -> source f = a -> fcompose f (vee_functor a u v) = vee_functor (target f) (fmor f u) (fmor f v).
proof: Proof. ir. ap functor_vee_eq2. app fcompose_axioms. app vee_functor_axioms. rww target_vee_functor. rww source_fcompose. rww source_vee_functor. rww target_fcompose. rww fmor_fcompose. rww fmor_vee_functor_catyd_arrow. app vee_functor_axioms. rww target_vee_functor. rww source_vee_functor. ap mor_vee_cat. rww fmor_fcompose. rww fmor_vee_functor_catyd_arrow. app vee_functor_axioms. rww target_vee_functor. rww source_vee_functor. ap mor_vee_cat. Qed.
imports: Arith cat_examples cardinal fc_limits