proposition: Corollary generate_comp `{@Monoidal C} `{@SemicocartesianMonoidal _} `{f : A ~> B} : f ∘ generate ≈ generate.
proof: Proof. intros; apply unit_initial. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Monoidal Category.Structure.Terminal