proposition: Lemma Product_η {C : HSET} (g : Product → pr1hSet C): Product_rec (λ a b, g (Pair a b)) = g.
proof: Proof. eapply pathscomp0. - apply (Product_com_con (C := Product_as_set) Pair). - apply funextfun; intro p. simpl. apply maponpaths. apply Product_weak_η. 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