equiv_quotient_functor' (f : A <~> B) (fresp : forall a b, R a b <-> S (f a) (f b)) : Quotient R <~> Quotient S := equiv_quotient_functor f fresp. End Functoriality. Section Kernel. Universes a r ar ar' b ab abr. Constraint a <= ar, r <= ar, ar < ar', a <= ab, b <= ab, ab <= abr, ar <= abr. Context `{Funext}. Context {A : Type@{a}} {B : Type@{b}} `{IsHSet B} (f : A -> B). Context (R : Relation@{a r} A) (is_ker : forall x y, f x = f y <~> R x y). Local quotient_kernel_factor_internal : exists (C : Type@{ar}) (e : A -> C) (m : C -> B), IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e). Proof. exists (Quotient R). exists (class_of R). srefine (_;_). { refine (Quotient_ind R (fun _ => B) f _). intros x y p. lhs nrapply transport_const. exact ((is_ker x y)^-1 p). } repeat split; try exact _. intro u. apply hprop_allpath. intros [x q] [y p']. apply path_sigma_hprop; simpl. revert x y q p'. srapply Quotient_ind. 2: intros; apply path_ishprop. intro a. srapply Quotient_ind. 2: intros; apply path_ishprop. intros a' p p'. apply qglue, is_ker. exact (p @ p'^). Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.