Simplify discreteSetQuotients

Cubical/Data/Int/MoreInts/DiffInt/Properties.agda

@@ -44,11 +44,8 @@ relIsEquiv = equivRel {A = ℕ × ℕ} relIsRefl relIsSym relIsTrans
             b0 +ℕ (b1 +ℕ (c0 +ℕ a1)) ≡⟨ ℕ.+-assoc b0 b1 (c0 +ℕ a1)⟩
             (b0 +ℕ b1) +ℕ (c0 +ℕ a1) ∎ )
 
-relIsProp : BinaryRelation.isPropValued rel
-relIsProp a b x y = isSetℕ _ _ _ _
-
 discreteℤ : Discrete ℤ
-discreteℤ = discreteSetQuotients (discreteΣ discreteℕ λ _ → discreteℕ) relIsProp relIsEquiv (λ _ _ → discreteℕ _ _)
+discreteℤ = discreteSetQuotients relIsEquiv (λ _ _ → discreteℕ _ _)
 
 private
   _ : Dec→Bool (discreteℤ [ (3 , 5) ] [ (4 , 6) ]) ≡ true

Cubical/HITs/Rationals/QuoQ/Base.agda

@@ -59,8 +59,7 @@ eq/⁻¹ : ∀ x y → Path ℚ [ x ] [ y ] → x ∼ y
 eq/⁻¹ = SetQuotient.effective (λ _ _ → isSetℤ _ _) isEquivRel∼
 
 discreteℚ : Discrete ℚ
-discreteℚ = discreteSetQuotients (discreteΣ discreteℤ (λ _ → subst Discrete 1+Path discreteℕ))
-                                 (λ _ _ → isSetℤ _ _) isEquivRel∼ (λ _ _ → discreteℤ _ _)
+discreteℚ = discreteSetQuotients isEquivRel∼ (λ _ _ → discreteℤ _ _)
 
 
 -- Natural number and negative integer literals for ℚ

Cubical/HITs/SetQuotients/Properties.agda

@@ -278,36 +278,6 @@ isEquivRel→isEffective : isPropValued R → isEquivRel R → isEffective R
 isEquivRel→isEffective Rprop Req a b =
   isoToIsEquiv (invIso (isEquivRel→effectiveIso Rprop Req a b))
 
-discreteSetQuotients : Discrete A → isPropValued R → isEquivRel R
-  → (∀ a₀ a₁ → Dec (R a₀ a₁))
-  → Discrete (A / R)
-discreteSetQuotients {A = A} {R = R} Adis Rprop Req Rdec =
-  elim (λ a₀ → isSetΠ (λ a₁ → isProp→isSet (isPropDec (squash/ a₀ a₁))))
-    discreteSetQuotients' discreteSetQuotients'-eq
-  where
-  discreteSetQuotients' : (a : A) (y : A / R) → Dec ([ a ] ≡ y)
-  discreteSetQuotients' a₀ =
-    elim (λ a₁ → isProp→isSet (isPropDec (squash/ [ a₀ ] a₁))) dis dis-eq
-    where
-    dis : (a₁ : A) → Dec ([ a₀ ] ≡ [ a₁ ])
-    dis a₁ with Rdec a₀ a₁
-    ... | (yes p) = yes (eq/ a₀ a₁ p)
-    ... | (no ¬p) = no λ eq → ¬p (effective Rprop Req a₀ a₁ eq )
-
-    dis-eq : (a b : A) (r : R a b) →
-      PathP (λ i → Dec ([ a₀ ] ≡ eq/ a b r i)) (dis a) (dis b)
-    dis-eq a b ab = J (λ b ab → ∀ k → PathP (λ i → Dec ([ a₀ ] ≡ ab i)) (dis a) k)
-                      (λ k → isPropDec (squash/ _ _) _  _) (eq/ a b ab) (dis b)
-
-  discreteSetQuotients'-eq : (a b : A) (r : R a b) →
-    PathP (λ i → (y : A / R) → Dec (eq/ a b r i ≡ y))
-          (discreteSetQuotients' a) (discreteSetQuotients' b)
-  discreteSetQuotients'-eq a b ab =
-    J (λ b ab → ∀ k → PathP (λ i → (y : A / R) → Dec (ab i ≡ y))
-                            (discreteSetQuotients' a) k)
-      (λ k → funExt (λ x → isPropDec (squash/ _ _) _ _)) (eq/ a b ab) (discreteSetQuotients' b)
-
-
 -- Quotienting by the truncated relation is equivalent to quotienting by untruncated relation
 truncRelIso : Iso (A / R) (A / (λ a b → ∥ R a b ∥₁))
 Iso.fun truncRelIso = rec squash/ [_] λ _ _ r → eq/ _ _ ∣ r ∣₁
@@ -335,6 +305,16 @@ isEquivRel→TruncIso {A = A} {R = R} Req a b =
   symmetric ∥R∥eq a b = PropTrunc.map (symmetric Req a b)
   transitive ∥R∥eq a b c = PropTrunc.map2 (transitive Req a b c)
 
+discreteSetQuotients : isEquivRel R
+  → (∀ a₀ a₁ → Dec (R a₀ a₁))
+  → Discrete (A / R)
+discreteSetQuotients {A = A} {R = R} Req Rdec =
+  elimProp2
+    (λ _ _ → isPropDec (squash/ _ _))
+    λ _ _ → EquivPresDec
+              (isoToEquiv (invIso (isEquivRel→TruncIso Req _ _)))
+              (Dec∥∥ (Rdec _ _))
+
 -- quotienting by 'logically equivalent' relations gives the same quotient
 relBiimpl→TruncIso : ({a b : A} → R a b → S a b) → ({a b : A} → S a b → R a b) → Iso (A / R) (A / S)
 Iso.fun (relBiimpl→TruncIso R→S S→R) = rec squash/ [_] λ _ _ Rab → eq/ _ _ (R→S Rab)