R : Type := | class_of R : A -> R | qglue : forall x y, (R x y) -> class_of R x = class_of R y | ishset_quotient : IsHSet ( R) >> We do this by defining the quotient as a 0-truncated graph quotient.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.