Homomorphism C A * Homomorphism C B <~> Homomorphism C (A × B). Proof. set (k := λ (b:Bool), Homomorphism C (bin_prod_algebras A B b)). exact (equiv_compose (ump_prod_algebra Bool (bin_prod_algebras A B) C) (equiv_bool_forall_prod k)^-1). Defined.
Require Import Import algebra_notations ne_list.notations. Import prod_algebra_notations.