proposition: Lemma isCoeqKernelPairSet (hf: issurjective f) : isCoequalizer _ _ _ (PullbackSqrCommutes g).
proof: Proof. intros. red. intros C u equ. assert (hcompat : ∏ x y : pr1 A, f x = f y → u x = u y). { intros x y eqfxy. assert (hpb:=pullback_HSET_univprop_elements (PullbackSqrCommutes g) (isPullback_Pullback g) x y eqfxy). assert( hpb' := pr2 (pr1 hpb)); simpl in hpb'. etrans. eapply pathsinv0. apply maponpaths. exact (pr1 hpb'). eapply pathscomp0. apply toforallpaths in equ. apply equ. cbn. apply maponpaths. exact (pr2 hpb'). } use (unique_exists (univ_surj (setproperty C) _ _ _ hf)). - exact u. - exact hcompat. - simpl. apply funextfun. intro. apply univ_surj_ax. - intro. apply has_homsets_HSET. - intros ??; simpl. apply funextfun. use univ_surj_unique. simpl in X. apply toforallpaths in X. exact X. Qed.
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