{A : Type} {R : Relation A} : Quotient_functor R R idmap (fun x y => idmap) == idmap. Proof. by srapply Quotient_ind_hprop. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.