proposition: Lemma hasBinProducts_WOSET (AC : AxiomOfChoice) : hasBinProducts WOSET.
proof: Proof. intros A B. set (AB := BinProductObject _ (BinProductsHSET (pr1 A) (pr1 B)) : hSet). apply (squash_to_hProp (@ZermeloWellOrdering AB AC)); intros R. apply hinhpr. use make_BinProduct. - exists AB. exact R. - apply (BinProductPr1 _ (BinProductsHSET _ _)). - apply (BinProductPr2 _ (BinProductsHSET _ _)). - intros H. apply (isBinProduct_BinProduct _ (BinProductsHSET _ _) (pr1 H)). Defined.
imports: UniMath.MoreFoundations.All UniMath.Combinatorics.OrderedSets UniMath.Combinatorics.WellOrderedSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.exponentials