dec_class@{} : forall q r, Decidable (class q = class r). Proof. intros q r. destruct (dec (equiv q r)) as [E|E]. - left. apply path,E. - right. intros E'. apply E. apply (classes_eq_related _ _ E'). Defined.
Require Import HoTT.HIT.quotient. Require Import Import Frac.