feat(data/quot): make trunc a quotient (#18320)

astrainfinita · eric-wieser · astrainfinita · commit 6ed6abbde29b · 2023-01-31T16:05:41.000Z
This allows us to use `quotient` lemmas for `trunc`. mathlib4 PR: leanprover-community/mathlib4#1924 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
diff --git a/src/data/quot.lean b/src/data/quot.lean
@@ -365,15 +365,21 @@ lemma nonempty_quotient_iff (s : setoid α) : nonempty (quotient s) ↔ nonempty
 
 /-! ### Truncation -/
 
+theorem true_equivalence : @equivalence α (λ _ _, true) :=
+⟨λ _, trivial, λ _ _ _, trivial, λ _ _ _ _ _, trivial⟩
+
+/-- Always-true relation as a `setoid`.
+
+Note that in later files the preferred spelling is `⊤ : setoid α`. -/
+def true_setoid : setoid α :=
+⟨_, true_equivalence⟩
+
 /-- `trunc α` is the quotient of `α` by the always-true relation. This
   is related to the propositional truncation in HoTT, and is similar
   in effect to `nonempty α`, but unlike `nonempty α`, `trunc α` is data,
   so the VM representation is the same as `α`, and so this can be used to
   maintain computability. -/
-def {u} trunc (α : Sort u) : Sort u := @quot α (λ _ _, true)
-
-theorem true_equivalence : @equivalence α (λ _ _, true) :=
-⟨λ _, trivial, λ _ _ _, trivial, λ _ _ _ _ _, trivial⟩
+def {u} trunc (α : Sort u) : Sort u := @quotient α true_setoid
 
 namespace trunc
 
