proposition: Theorem from_free_unique (f g : AlgHom Free A) : (∀ x : X, f (generator x) = g (generator x)) → f ≈ g.
proof: Proof. intros eq_gen t. induction t. - now apply eq_gen. - rewrite 2 op_commute. f_equal. extensionality x. now apply H. Qed.
imports: Category.Lib Category.Theory.Category Category.Structure.Terminal Category.Structure.Initial Category.Structure.Cartesian