proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.AxiomOfChoice UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.NNO UniMath.CategoryTheory.SubobjectClassifier UniMath.CategoryTheory.Categories.Type.Core UniMath.CategoryTheory.Categories.Type.MonoEpiIso UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.covyoneda UniMath.CategoryTheory.EpiFacts UniMath.CategoryTheory.Monics UniMath.CategoryTheory.SplitMonicsAndEpis UniMath.CategoryTheory.ElementaryTopos UniMath.CategoryTheory.PowerObject UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.Categories.HSET.Univalence