Negated equality (#822)

Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>

src/elementary-number-theory/addition-natural-numbers.lagda.md

@@ -19,7 +19,7 @@ open import foundation.function-types
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.interchange-law
-open import foundation.negation
+open import foundation.negated-equality
 ```
 
 </details>
@@ -181,7 +181,7 @@ is-zero-sum-is-zero-summand-ℕ .zero-ℕ .zero-ℕ (pair refl refl) = refl
 
 ```agda
 neq-add-ℕ :
-  (m n : ℕ) → ¬ (m ＝ m +ℕ (succ-ℕ n))
+  (m n : ℕ) → m ≠ m +ℕ (succ-ℕ n)
 neq-add-ℕ (succ-ℕ m) n p =
   neq-add-ℕ m n
     ( ( is-injective-succ-ℕ p) ∙

src/elementary-number-theory/divisibility-natural-numbers.lagda.md

@@ -20,6 +20,7 @@ open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.identity-types
 open import foundation.logical-equivalences
+open import foundation.negated-equality
 open import foundation.negation
 open import foundation.propositional-maps
 open import foundation.propositions
@@ -178,10 +179,10 @@ leq-quotient-div-ℕ' d (succ-ℕ x) f H =
 
 ```agda
 le-div-succ-ℕ :
-  (d x : ℕ) → div-ℕ d (succ-ℕ x) → ¬ (d ＝ succ-ℕ x) → le-ℕ d (succ-ℕ x)
+  (d x : ℕ) → div-ℕ d (succ-ℕ x) → d ≠ succ-ℕ x → le-ℕ d (succ-ℕ x)
 le-div-succ-ℕ d x H f = le-leq-neq-ℕ (leq-div-succ-ℕ d x H) f
 
-le-div-ℕ : (d x : ℕ) → is-nonzero-ℕ x → div-ℕ d x → ¬ (d ＝ x) → le-ℕ d x
+le-div-ℕ : (d x : ℕ) → is-nonzero-ℕ x → div-ℕ d x → d ≠ x → le-ℕ d x
 le-div-ℕ d x H K f = le-leq-neq-ℕ (leq-div-ℕ d x H K) f
 ```
 

src/elementary-number-theory/integers.lagda.md

@@ -20,7 +20,7 @@ open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.injective-maps
-open import foundation.negation
+open import foundation.negated-equality
 open import foundation.propositions
 open import foundation.sets
 open import foundation.unit-type
@@ -201,7 +201,7 @@ is-injective-succ-ℤ : is-injective succ-ℤ
 is-injective-succ-ℤ {x} {y} p =
   inv (is-retraction-pred-ℤ x) ∙ (ap pred-ℤ p ∙ is-retraction-pred-ℤ y)
 
-has-no-fixed-points-succ-ℤ : (x : ℤ) → ¬ (succ-ℤ x ＝ x)
+has-no-fixed-points-succ-ℤ : (x : ℤ) → succ-ℤ x ≠ x
 has-no-fixed-points-succ-ℤ (inl zero-ℕ) ()
 has-no-fixed-points-succ-ℤ (inl (succ-ℕ x)) ()
 has-no-fixed-points-succ-ℤ (inr (inl star)) ()

src/elementary-number-theory/modular-arithmetic.lagda.md

@@ -32,6 +32,7 @@ open import foundation.equivalences
 open import foundation.function-types
 open import foundation.identity-types
 open import foundation.injective-maps
+open import foundation.negated-equality
 open import foundation.negation
 open import foundation.sets
 open import foundation.surjective-maps
@@ -768,12 +769,12 @@ is-one-is-fixed-point-succ-ℤ-Mod k x p =
                 ( ap (succ-ℤ-Mod k) (is-section-int-ℤ-Mod k x))))))))
 
 has-no-fixed-points-succ-ℤ-Mod :
-  (k : ℕ) (x : ℤ-Mod k) → is-not-one-ℕ k → ¬ (succ-ℤ-Mod k x ＝ x)
+  (k : ℕ) (x : ℤ-Mod k) → is-not-one-ℕ k → succ-ℤ-Mod k x ≠ x
 has-no-fixed-points-succ-ℤ-Mod k x =
   map-neg (is-one-is-fixed-point-succ-ℤ-Mod k x)
 
 has-no-fixed-points-succ-Fin :
-  {k : ℕ} (x : Fin k) → is-not-one-ℕ k → ¬ (succ-Fin k x ＝ x)
+  {k : ℕ} (x : Fin k) → is-not-one-ℕ k → succ-Fin k x ≠ x
 has-no-fixed-points-succ-Fin {succ-ℕ k} x =
   has-no-fixed-points-succ-ℤ-Mod (succ-ℕ k) x
 ```

src/elementary-number-theory/multiplication-natural-numbers.lagda.md

@@ -17,8 +17,7 @@ open import foundation.embeddings
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.interchange-law
-open import foundation.negation
-open import foundation.universe-levels
+open import foundation.negated-equality
 ```
 
 </details>
@@ -230,7 +229,7 @@ is-one-left-is-one-mul-ℕ x y p =
   is-one-right-is-one-mul-ℕ y x (commutative-mul-ℕ y x ∙ p)
 
 neq-mul-ℕ :
-  (m n : ℕ) → ¬ (succ-ℕ m ＝ (succ-ℕ m) *ℕ (succ-ℕ (succ-ℕ n)))
+  (m n : ℕ) → succ-ℕ m ≠ (succ-ℕ m *ℕ (succ-ℕ (succ-ℕ n)))
 neq-mul-ℕ m n p =
   neq-add-ℕ
     ( succ-ℕ m)

src/elementary-number-theory/natural-numbers.lagda.md

@@ -15,6 +15,7 @@ open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.logical-equivalences
+open import foundation.negated-equality
 open import foundation.negation
 open import foundation.unit-type
 open import foundation.universe-levels
@@ -113,14 +114,14 @@ is-nonzero-succ-ℕ : (x : ℕ) → is-nonzero-ℕ (succ-ℕ x)
 is-nonzero-succ-ℕ x ()
 
 is-nonzero-is-successor-ℕ : {x : ℕ} → is-successor-ℕ x → is-nonzero-ℕ x
-is-nonzero-is-successor-ℕ (pair x refl) ()
+is-nonzero-is-successor-ℕ (x , refl) ()
 
 is-successor-is-nonzero-ℕ : {x : ℕ} → is-nonzero-ℕ x → is-successor-ℕ x
 is-successor-is-nonzero-ℕ {zero-ℕ} H = ex-falso (H refl)
 pr1 (is-successor-is-nonzero-ℕ {succ-ℕ x} H) = x
 pr2 (is-successor-is-nonzero-ℕ {succ-ℕ x} H) = refl
 
-has-no-fixed-points-succ-ℕ : (x : ℕ) → ¬ (succ-ℕ x ＝ x)
+has-no-fixed-points-succ-ℕ : (x : ℕ) → succ-ℕ x ≠ x
 has-no-fixed-points-succ-ℕ x ()
 ```
 

src/elementary-number-theory/nonzero-integers.lagda.md

@@ -27,7 +27,7 @@ An [integer](elementary-number-theory.integers.md) `k` is said to be **nonzero**
 if the [proposition](foundation.propositions.md)
 
 ```text
-  ¬ (k ＝ 0)
+  k ≠ 0
 ```
 
 holds.

src/elementary-number-theory/nonzero-natural-numbers.lagda.md

@@ -11,6 +11,7 @@ open import elementary-number-theory.divisibility-natural-numbers
 open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
+open import foundation.negated-equality
 open import foundation.universe-levels
 ```
 
@@ -22,7 +23,7 @@ A [natural number](elementary-number-theory.natural-numbers.md) `n` is said to
 be **nonzero** if the [proposition](foundation.propositions.md)
 
 ```text
-  ¬ (n ＝ 0)
+  n ≠ 0
 ```
 
 holds. This condition was already defined in the file

src/elementary-number-theory/prime-numbers.lagda.md

@@ -26,6 +26,7 @@ open import foundation.empty-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
 open import foundation.logical-equivalences
+open import foundation.negated-equality
 open import foundation.negation
 open import foundation.propositions
 open import foundation.transport-along-identifications
@@ -95,8 +96,8 @@ is-nonzero-is-prime-ℕ n H p =
   is-not-one-two-ℕ
     ( pr1
       ( H 2)
-      ( tr (λ n → ¬ (2 ＝ n)) (inv (p)) ( is-nonzero-two-ℕ) ,
-        tr (λ n → div-ℕ 2 n) (inv p) (0 , refl)))
+      ( tr (λ k → 2 ≠ k) (inv p) ( is-nonzero-two-ℕ) ,
+        tr (div-ℕ 2) (inv p) (0 , refl)))
 ```
 
 ### The number `1` is not a prime

src/elementary-number-theory/proper-divisors-natural-numbers.lagda.md

@@ -20,6 +20,7 @@ open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.identity-types
+open import foundation.negated-equality
 open import foundation.negation
 open import foundation.propositions
 open import foundation.type-arithmetic-empty-type
@@ -35,7 +36,7 @@ divides `n`.
 
 ```agda
 is-proper-divisor-ℕ : ℕ → ℕ → UU lzero
-is-proper-divisor-ℕ n d = ¬ (d ＝ n) × div-ℕ d n
+is-proper-divisor-ℕ n d = (d ≠ n) × (div-ℕ d n)
 
 is-decidable-is-proper-divisor-ℕ :
   (n d : ℕ) → is-decidable (is-proper-divisor-ℕ n d)
@@ -83,7 +84,7 @@ pr2 (pr2 (is-proper-divisor-one-is-proper-divisor-ℕ {n} {x} H)) =
 ```agda
 le-one-quotient-div-is-proper-divisor-ℕ :
   (d x : ℕ) → is-nonzero-ℕ x → (H : div-ℕ d x) →
-  ¬ (d ＝ x) → le-ℕ 1 (quotient-div-ℕ d x H)
+  d ≠ x → le-ℕ 1 (quotient-div-ℕ d x H)
 le-one-quotient-div-is-proper-divisor-ℕ d x f H g =
   map-left-unit-law-coprod-is-empty
     ( is-one-ℕ (quotient-div-ℕ d x H))

src/elementary-number-theory/relatively-prime-natural-numbers.lagda.md

@@ -23,6 +23,7 @@ open import foundation.decidable-propositions
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.identity-types
+open import foundation.negated-equality
 open import foundation.negation
 open import foundation.propositions
 open import foundation.transport-along-identifications
@@ -156,7 +157,7 @@ module _
   (a b : ℕ)
   (pa : is-prime-ℕ a)
   (pb : is-prime-ℕ b)
-  (n : ¬ (a ＝ b))
+  (n : a ≠ b)
   where
 
   is-one-is-common-divisor-is-prime-ℕ :

src/elementary-number-theory/repeating-element-standard-finite-type.lagda.md

@@ -13,7 +13,7 @@ open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types
 open import foundation.empty-types
 open import foundation.identity-types
-open import foundation.negation
+open import foundation.negated-equality
 
 open import univalent-combinatorics.equality-standard-finite-types
 open import univalent-combinatorics.standard-finite-types
@@ -32,7 +32,7 @@ repeat-Fin (succ-ℕ k) (inr star) (inr star) = inr star
 abstract
   is-almost-injective-repeat-Fin :
     (k : ℕ) (x : Fin k) {y z : Fin (succ-ℕ k)} →
-    ¬ (inl x ＝ y) → ¬ (inl x ＝ z) →
+    inl x ≠ y → inl x ≠ z →
     repeat-Fin k x y ＝ repeat-Fin k x z → y ＝ z
   is-almost-injective-repeat-Fin (succ-ℕ k) (inl x) {inl y} {inl z} f g p =
     ap

src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md

@@ -20,6 +20,7 @@ open import foundation.empty-types
 open import foundation.function-types
 open import foundation.functoriality-coproduct-types
 open import foundation.identity-types
+open import foundation.negated-equality
 open import foundation.negation
 open import foundation.propositions
 open import foundation.transport-along-identifications
@@ -122,7 +123,7 @@ anti-reflexive-le-ℕ (succ-ℕ n) = anti-reflexive-le-ℕ n
 ### If `x < y` then `x ≠ y`
 
 ```agda
-neq-le-ℕ : {x y : ℕ} → le-ℕ x y → ¬ (x ＝ y)
+neq-le-ℕ : {x y : ℕ} → le-ℕ x y → x ≠ y
 neq-le-ℕ {zero-ℕ} {succ-ℕ y} H = is-nonzero-succ-ℕ y ∘ inv
 neq-le-ℕ {succ-ℕ x} {succ-ℕ y} H p = neq-le-ℕ H (is-injective-succ-ℕ p)
 ```
@@ -309,7 +310,7 @@ leq-eq-or-le-ℕ x y (inr l) = leq-le-ℕ x y l
 ### If `x ≤ y` and `x ≠ y` then `x < y`
 
 ```agda
-le-leq-neq-ℕ : {x y : ℕ} → x ≤-ℕ y → ¬ (x ＝ y) → le-ℕ x y
+le-leq-neq-ℕ : {x y : ℕ} → x ≤-ℕ y → x ≠ y → le-ℕ x y
 le-leq-neq-ℕ {zero-ℕ} {zero-ℕ} l f = ex-falso (f refl)
 le-leq-neq-ℕ {zero-ℕ} {succ-ℕ y} l f = star
 le-leq-neq-ℕ {succ-ℕ x} {succ-ℕ y} l f =

src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md

@@ -16,7 +16,7 @@ open import foundation.empty-types
 open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
-open import foundation.negation
+open import foundation.negated-equality
 open import foundation.pairs-of-distinct-elements
 open import foundation.unit-type
 open import foundation.universe-levels
@@ -65,7 +65,7 @@ pair-of-distinct-elements-strictly-ordered-pair-ℕ (a , b , H) =
 
 ```agda
 strictly-ordered-pair-pair-of-distinct-elements-ℕ' :
-  (a b : ℕ) → ¬ (a ＝ b) → strictly-ordered-pair-ℕ
+  (a b : ℕ) → a ≠ b → strictly-ordered-pair-ℕ
 strictly-ordered-pair-pair-of-distinct-elements-ℕ' zero-ℕ zero-ℕ H =
   ex-falso (H refl)
 strictly-ordered-pair-pair-of-distinct-elements-ℕ' zero-ℕ (succ-ℕ b) H =

src/finite-group-theory/delooping-sign-homomorphism.lagda.md

@@ -44,6 +44,7 @@ open import foundation.injective-maps
 open import foundation.involutions
 open import foundation.logical-equivalences
 open import foundation.mere-equivalences
+open import foundation.negated-equality
 open import foundation.negation
 open import foundation.propositional-truncations
 open import foundation.propositions
@@ -1512,17 +1513,17 @@ module _
       ( Q ( n +ℕ 2)
           ( raise l1 (Fin (n +ℕ 2)) ,
             unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))) →
-    ¬ ( x ＝
-        ( map-equiv
-          ( action-equiv-family-over-subuniverse
-            ( mere-equiv-Prop (Fin (n +ℕ 2)))
-            ( type-UU-Fin 2 ∘ Q (n +ℕ 2))
-            ( raise l1 (Fin (n +ℕ 2)) ,
-              unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2)))
-            ( raise l1 (Fin (n +ℕ 2)) ,
-              unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2)))
-            ( transposition Y))
-          ( x))))
+    ( x) ≠
+    ( map-equiv
+      ( action-equiv-family-over-subuniverse
+        ( mere-equiv-Prop (Fin (n +ℕ 2)))
+        ( type-UU-Fin 2 ∘ Q (n +ℕ 2))
+        ( raise l1 (Fin (n +ℕ 2)) ,
+          unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2)))
+        ( raise l1 (Fin (n +ℕ 2)) ,
+          unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2)))
+        ( transposition Y))
+      ( x)))
   where
 
   private

src/finite-group-theory/orbits-permutations.lagda.md

@@ -43,6 +43,7 @@ open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.iterating-functions
 open import foundation.logical-equivalences
+open import foundation.negated-equality
 open import foundation.negation
 open import foundation.propositional-truncations
 open import foundation.propositions
@@ -145,7 +146,7 @@ module _
       ( succ-ℕ (number-of-elements-count eX))
       ( pr1 (pr2 (pr1 repetition-iterate-automorphism-Fin)))
 
-  neq-points-iterate-ℕ : ¬ (Id point1-iterate-ℕ point2-iterate-ℕ)
+  neq-points-iterate-ℕ : point1-iterate-ℕ ≠ point2-iterate-ℕ
   neq-points-iterate-ℕ p =
     pr2
       ( pr2 (pr1 repetition-iterate-automorphism-Fin))
@@ -637,7 +638,7 @@ module _
 
 ```agda
 module _
-  {l1 : Level} (X : UU l1) (eX : count X) (a b : X) (np : ¬ (Id a b))
+  {l1 : Level} (X : UU l1) (eX : count X) (a b : X) (np : a ≠ b)
   where
 
   composition-transposition-a-b : (X ≃ X) → (X ≃ X)
@@ -712,8 +713,8 @@ module _
       {l2 : Level} (x : X) (g : X ≃ X) (C : ℕ → UU l2)
       ( F :
         (k : ℕ) → C k →
-        ( ¬ (Id (iterate k (map-equiv g) x) a)) ×
-        ( ¬ (Id (iterate k (map-equiv g) x) b)))
+        ( iterate k (map-equiv g) x ≠ a) ×
+        ( iterate k (map-equiv g) x ≠ b))
       ( Ind :
         (n : ℕ) → C (succ-ℕ n) → is-nonzero-ℕ n → C n) →
       (k : ℕ) → (is-zero-ℕ k + C k) →
@@ -874,7 +875,7 @@ module _
         ( pa : Σ ℕ (λ k → Id (iterate k (map-equiv g) a) b))
         ( k : ℕ) →
         ( is-nonzero-ℕ k × le-ℕ k (pr1 (minimal-element-iterate g a b pa))) →
-        ¬ (iterate k (map-equiv g) a ＝ a) × ¬ (iterate k (map-equiv g) a ＝ b)
+        ( iterate k (map-equiv g) a ≠ a) × (iterate k (map-equiv g) a ≠ b)
       pr1 (neq-iterate-nonzero-le-minimal-element pa k (pair nz ineq)) q =
         contradiction-le-ℕ
           ( pr1 pair-k2)
@@ -1011,7 +1012,7 @@ module _
           ( mult-lemma2 pa k))
       lemma3 :
         ( pa : Σ ℕ (λ k → Id (iterate k (map-equiv g) a) b)) (k : ℕ) →
-        ¬ (Id (iterate k (map-equiv (composition-transposition-a-b g)) a) b)
+        iterate k (map-equiv (composition-transposition-a-b g)) a ≠ b
       lemma3 pa k q =
         contradiction-le-ℕ
           ( r)
@@ -2185,8 +2186,7 @@ module _
       neq-iterate-nonzero-le-minimal-element :
         (k : ℕ) →
         is-nonzero-ℕ k × le-ℕ k (pr1 minimal-element-iterate-repeating) →
-        ¬ (Id (iterate k (map-equiv g) a) a) ×
-        ¬ (Id (iterate k (map-equiv g) a) b)
+        (iterate k (map-equiv g) a ≠ a) × (iterate k (map-equiv g) a ≠ b)
       pr1 (neq-iterate-nonzero-le-minimal-element k (pair nz ineq)) Q =
         contradiction-le-ℕ k (pr1 minimal-element-iterate-repeating) ineq
           (pr2 (pr2 minimal-element-iterate-repeating) k (pair nz Q))
@@ -2425,7 +2425,7 @@ module _
           ( λ x →
             Σ ( X)
               ( λ y →
-                Σ ( ¬ (Id x y))
+                Σ ( x ≠ y)
                   ( λ np →
                     Id
                       ( standard-2-Element-Decidable-Subtype