Remove DecidableEq (#866)

* remove unused imports of Cubical.Relation.Nullary.DecidableEq * correct comment where to find Hedberg's theorem * delete DecidableEq
agda · Aug 10, 2022 · ff3a599 · ff3a599
1 parent 8a4a3eb
commit ff3a599
Show file tree

Hide file tree

Showing 15 changed files with 1 addition and 19 deletions.
diff --git a/Cubical/Data/Bool/Properties.agda b/Cubical/Data/Bool/Properties.agda
@@ -24,7 +24,6 @@ open import Cubical.Data.Unit using (Unit; isPropUnit)
 open import Cubical.HITs.PropositionalTruncation hiding (rec)
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 private
   variable

diff --git a/Cubical/Data/DescendingList/Examples.agda b/Cubical/Data/DescendingList/Examples.agda
@@ -19,7 +19,6 @@ open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Nat
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 open import Cubical.HITs.FiniteMultiset
 

diff --git a/Cubical/Data/DescendingList/Properties.agda b/Cubical/Data/DescendingList/Properties.agda
@@ -20,7 +20,6 @@ open import Cubical.Data.Unit
 open import Cubical.Data.List using (List ; [] ; _∷_)
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 open import Cubical.HITs.FiniteMultiset as FMSet hiding ([_])
 

diff --git a/Cubical/Data/DescendingList/Strict/Properties.agda b/Cubical/Data/DescendingList/Strict/Properties.agda
@@ -17,7 +17,6 @@ open import Cubical.Data.DescendingList.Strict A _>_
 open import Cubical.HITs.ListedFiniteSet as LFSet renaming (_∈_ to _∈ʰ_)
 
 import Cubical.Data.Empty as ⊥
-open import Cubical.Relation.Nullary.DecidableEq
 
 open import Cubical.Relation.Nullary using (Dec; Discrete) renaming (¬_ to Type¬_)
 

diff --git a/Cubical/Data/Fin/LehmerCode.agda b/Cubical/Data/Fin/LehmerCode.agda
@@ -18,7 +18,6 @@ open import Cubical.Functions.Embedding
 open import Cubical.Functions.Surjection
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 open import Cubical.Data.Unit as ⊤
 open import Cubical.Data.Empty as ⊥

diff --git a/Cubical/Data/Fin/Properties.agda b/Cubical/Data/Fin/Properties.agda
@@ -26,7 +26,6 @@ open import Cubical.Data.Sigma
 open import Cubical.Data.FinData.Base renaming (Fin to FinData) hiding (¬Fin0 ; toℕ)
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 open import Cubical.Induction.WellFounded
 

diff --git a/Cubical/Data/FinSet/Properties.agda b/Cubical/Data/FinSet/Properties.agda
@@ -23,7 +23,6 @@ open import Cubical.Data.SumFin
 open import Cubical.Data.FinSet.Base
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 open import Cubical.Relation.Nullary.HLevels
 
 private

diff --git a/Cubical/Data/Int/Properties.agda b/Cubical/Data/Int/Properties.agda
@@ -20,7 +20,6 @@ open import Cubical.Data.Sum
 open import Cubical.Data.Int.Base
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 sucPred : ∀ i → sucℤ (predℤ i) ≡ i
 sucPred (pos zero)    = refl

diff --git a/Cubical/Data/Nat/Properties.agda b/Cubical/Data/Nat/Properties.agda
@@ -13,7 +13,6 @@ open import Cubical.Data.Sigma
 open import Cubical.Data.Sum.Base
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 private
   variable

diff --git a/Cubical/Data/SumFin/Base.agda b/Cubical/Data/SumFin/Base.agda
@@ -10,7 +10,6 @@ open import Cubical.Data.Sum using (_⊎_; inl; inr) public
 open import Cubical.Data.Nat hiding (elim)
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 private
   variable

diff --git a/Cubical/Foundations/HLevels.agda b/Cubical/Foundations/HLevels.agda
@@ -4,7 +4,7 @@ Basic theory about h-levels/n-types:
 
 - Basic properties of isContr, isProp and isSet (definitions are in Prelude)
 
-- Hedberg's theorem can be found in Cubical/Relation/Nullary/DecidableEq
+- Hedberg's theorem can be found in Cubical/Relation/Nullary/Properties
 
 -}
 {-# OPTIONS --safe #-}

diff --git a/Cubical/HITs/AssocList/Properties.agda b/Cubical/HITs/AssocList/Properties.agda
@@ -11,7 +11,6 @@ open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.SIP
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 open import Cubical.Structures.MultiSet
 

diff --git a/Cubical/HITs/FiniteMultiset/CountExtensionality.agda b/Cubical/HITs/FiniteMultiset/CountExtensionality.agda
@@ -12,7 +12,6 @@ open import Cubical.Relation.Nullary
 open import Cubical.HITs.FiniteMultiset.Base
 open import Cubical.HITs.FiniteMultiset.Properties as FMS
 open import Cubical.Structures.MultiSet
-open import Cubical.Relation.Nullary.DecidableEq
 
 
 private

diff --git a/Cubical/HITs/FiniteMultiset/Properties.agda b/Cubical/HITs/FiniteMultiset/Properties.agda
@@ -8,7 +8,6 @@ open import Cubical.Data.Empty as ⊥
 open import Cubical.Relation.Nullary
 open import Cubical.HITs.FiniteMultiset.Base
 open import Cubical.Structures.MultiSet
-open import Cubical.Relation.Nullary.DecidableEq
 
 private
   variable

diff --git a/Cubical/Relation/Nullary/DecidableEq.agda b/Cubical/Relation/Nullary/DecidableEq.agda