Lemma isCoeqKernelPairSet (hf: issurjective f) : isCoequalizer _ _ _ (PullbackSqrCommutes g). 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.
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).