proposition: Theorem sets_exact : forall x y, (class_of R x = class_of R y) <~> R x y.
proof: Proof. intros ??. apply equiv_iff_hprop. - apply classes_eq_related. - apply related_classes_eq. Defined.
imports: HoTT.Basics HoTT.Types HSet TruncType Truncations.Core