From 71ffdb9cece028306c0925f8e5c621e2775961f0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= <vi.hdz.p@gmail.com>
Date: Tue, 14 Jan 2025 09:49:53 -0600
Subject: [PATCH] Update Core.lean

---
 src/Init/Core.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index ff6638b4773d..1b3b83415677 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1913,7 +1913,7 @@ theorem true_equivalence (α : Sort u) : Equivalence fun _ _ : α ↦ True :=
 
 /-- Always-true relation as a `Setoid`. -/
 def trueSetoid (α : Sort u) : Setoid α :=
-  ⟨_, true_equivalence⟩
+  ⟨_, true_equivalence α⟩
 
 /--
 `Squash α` is the quotient of `α` by the always true relation.