class_of@{i j k} {A : Type@{i}} (R : Relation@{i j} A) : A -> Quotient@{i j k} R := tr o gq.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.