proposition: Lemma ump_prod_algebra `{!∀ i, IsHSetAlgebra (A i)} : (∀ (i:I), Homomorphism C (A i)) <~> Homomorphism C (ProdAlgebra I A).
proof: Proof. apply (equiv_adjointify hom_prod_algebra_mapin hom_prod_algebra_mapout). - intro f. by apply path_hset_homomorphism. - intro f. funext i. by apply path_hset_homomorphism. Defined.
imports: HoTT.Types.Bool HoTT.Types.Forall HoTT.Classes.theory.ua_homomorphism