Lemma BinProductsHSET : BinProducts HSET. Proof. intros A B. use make_BinProduct. - apply (A × B)%set. - simpl in *; apply pr1. - simpl in *; intros x; apply (pr2 x). - apply make_isBinProduct. intros C f g; use tpair. * exists (prodtofuntoprod (f,,g)); abstract (split; apply idpath). * abstract (intros [t [ht1 ht2]]; apply subtypePath; [ intros x; apply isapropdirprod; apply has_homsets_HSET | now apply funextfun; intro x; rewrite <- ht2, <- ht1 ]). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.WeakEquivalences. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Graphs.Equalizers. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Categories.HSET.Core.