Quotient@{i j k} {A : Type@{i}} (R : Relation@{i j} A) : Type@{k} := Trunc@{k} 0 (GraphQuotient@{i j k} R).
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.