diff --git a/Batteries.lean b/Batteries.lean
index ebd3048cd9..c987926b24 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -34,7 +34,6 @@ import Batteries.Data.PairingHeap
 import Batteries.Data.RBMap
 import Batteries.Data.Range
 import Batteries.Data.Rat
-import Batteries.Data.Sigma
 import Batteries.Data.String
 import Batteries.Data.Sum
 import Batteries.Data.UInt
diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
index 2c42c4a1f0..881cc25324 100644
--- a/Batteries/Data/DArray.lean
+++ b/Batteries/Data/DArray.lean
@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
 
-import Batteries.Data.Sigma
-
 namespace Batteries
 
 /-- `DArray` is a heterogenous array with element types given by `type`. -/
diff --git a/Batteries/Data/Sigma.lean b/Batteries/Data/Sigma.lean
deleted file mode 100644
index e55c1a008d..0000000000
--- a/Batteries/Data/Sigma.lean
+++ /dev/null
@@ -1,29 +0,0 @@
-/-
-Copyright (c) 2024 François G. Dorais. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: François G. Dorais
--/
-
-namespace Sigma
-
-/-- Type value of a `Sigma` object. -/
-protected abbrev type (a : Sigma α) : Type _ := α a.fst
-
-/-- Casts an `Sigma` object to  a value of compatible type. -/
-protected def cast : (a : Sigma α) → a.type = β → β
-  | {snd := a}, rfl => a
-
-/-- Casts an `Sigma` object to  a value of compatible index. -/
-protected def castIdx : (a : Sigma α) → a.fst = i → α i
-  | {snd := a}, rfl => a
-
-@[simp]
-theorem mk_val (a : Sigma α) : ⟨_, a.snd⟩ = a := rfl
-
-@[simp]
-theorem cast_heq_val : (a : Sigma α) → (h : a.type = β) → HEq (a.cast h) a.snd
-  | {..}, rfl => .rfl
-
-@[simp]
-theorem castIdx_heq_val : (a : Sigma α) → (h : a.fst = i) → HEq (a.castIdx h) a.snd
-  | {..}, rfl => .rfl