proposition: Lemma ump_bin_prod_algebra : Homomorphism C A * Homomorphism C B <~> Homomorphism C (A × B).
proof: 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.
imports: HoTT.Types.Bool HoTT.Types.Forall HoTT.Classes.theory.ua_homomorphism