Lemma coequalizer_out_hSet_equality (Z : hSet) (h : Y → Z) (p : ∏ (x : X), h(f x) = h(g x)) : iscomprelfun coequalizer_eqrel h. Proof. intros y₁ y₂ q. cbn in *. use (q (make_eqrel (λ y₁ y₂, make_hProp (h y₁ = h y₂) _) _)). - apply setproperty. - repeat split. + exact (λ _ _ _ r₁ r₂, r₁ @ r₂). + exact (λ _ _ r, !r). - intros x y ; cbn. use factor_through_squash. { apply setproperty. } intros r. rewrite <- (pr12 r). rewrite <- (pr22 r). apply p. 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.Tactics. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Coproducts. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Pushouts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.MoreFoundations.Subtypes.