Remove mentions of the Id type (#1005)

agda · Sep 14, 2023 · f697467 · f697467
1 parent 7bf8d3d
commit f697467
Show file tree

Hide file tree

Showing 4 changed files with 0 additions and 35 deletions.
diff --git a/Cubical/Core/Everything.agda b/Cubical/Core/Everything.agda
@@ -6,6 +6,3 @@ open import Cubical.Core.Primitives public
 
 -- Definition of equivalences and Glue types
 open import Cubical.Core.Glue public
-
--- Definition of cubical Identity types
-open import Cubical.Core.Id
diff --git a/Cubical/Core/Id.agda b/Cubical/Core/Id.agda
diff --git a/Cubical/Foundations/Everything.agda b/Cubical/Foundations/Everything.agda
@@ -13,7 +13,6 @@ open import Cubical.Foundations.Equiv.BiInvertible public
 open import Cubical.Foundations.Equiv.HalfAdjoint
 open import Cubical.Foundations.Equiv.Dependent
 open import Cubical.Foundations.HLevels public
-open import Cubical.Foundations.Id public
 open import Cubical.Foundations.Path public
 open import Cubical.Foundations.Pointed public
 open import Cubical.Foundations.RelationalStructure public

diff --git a/Cubical/Foundations/Id.agda b/Cubical/Foundations/Id.agda