proposition: Lemma Product_univ_prop {C : HSET} : isweq (@Product_rec C).
proof: Proof. use isweq_iso. - exact (λ f a b, f (Pair a b)). - apply idpath. - apply Product_η. Defined.
imports: UniMath.Foundations.Init UniMath.Foundations.Preamble UniMath.Foundations.PartA UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Structures