Lemma hasBinProducts_WOSET (AC : AxiomOfChoice) : hasBinProducts WOSET. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.exponentials.