Type := | class_of : A -> | related_classes_eq : forall x y, (R x y), class_of x = class_of y | quotient_set : IsHSet >> *) (** TODO: This development should be further connected with the sections in the book; see below.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.