Lemma pullback_HSET_univprop_elements {P A B C : HSET} {p1 : HSET ⟦ P, A ⟧} {p2 : HSET ⟦ P, B ⟧} {f : HSET ⟦ A, C ⟧} {g : HSET ⟦ B, C ⟧} (ep : p1 · f = p2 · g) (pb : isPullback ep) : (∏ a b (e : f a = g b), ∃! ab, p1 ab = a × p2 ab = b). Proof. intros a b e. set (Pb := (make_Pullback _ pb)). apply iscontraprop1. - apply invproofirrelevance; intros [ab [ea eb]] [ab' [ea' eb']]. apply subtypePath; simpl. intros x; apply isapropdirprod; apply setproperty. use (@toforallpaths unitset _ (λ _, ab) (λ _, ab') _ tt). use (MorphismsIntoPullbackEqual pb); apply funextsec; intros []; cbn; (eapply @pathscomp0; [ eassumption | apply pathsinv0; eassumption]). - use (_,,_). use (_ tt). use (PullbackArrow Pb (unitset : HSET) (λ _, a) (λ _, b)). apply funextsec; intro; exact e. simpl; split. + generalize tt; apply toforallpaths. apply (PullbackArrow_PullbackPr1 Pb unitset). + generalize tt; apply toforallpaths. apply (PullbackArrow_PullbackPr2 Pb unitset). 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.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Arithmetic.NNO. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.Categories.Type.Core. Require Import UniMath.CategoryTheory.Categories.Type.MonoEpiIso. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.EpiFacts. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.SplitMonicsAndEpis. Require Import UniMath.CategoryTheory.ElementaryTopos. Require Import UniMath.CategoryTheory.PowerObject. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. assert (p : (BinProductsFromPullbacks PullbacksHSET TerminalHSET) = BinProductsHSET).