qglue@{i j k} {A : Type@{i}} {R : Relation@{i j} A} {a b : A} : R a b -> class_of@{i j k} R a = class_of R b := fun p => ap tr (gqglue p).
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.