proposition: Corollary eliminate_comp `{@Monoidal C} `{@SemicartesianMonoidal _} `{f : A ~> B} : eliminate ∘ f ≈ eliminate.
proof: Proof. intros; apply unit_terminal. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Monoidal