Prefer infix ＝ over Id

.vscode/tasks.json

@@ -9,7 +9,7 @@
         "kind": "test",
         "isDefault": true
       },
-      "dependsOn": ["pre-commit", "link-check", "typecheck"],
+      "dependsOn": ["link-check", "typecheck-after-pre-commit"],
       "dependsOrder": "parallel"
     },
     {
@@ -20,12 +20,26 @@
       "args": ["check"],
       "problemMatcher": [],
       "group": { "kind": "build" },
-      "dependsOn": "pre-commit",
       "presentation": {
         "panel": "dedicated",
         "clear": true
       }
     },
+    {
+      "label": "typecheck-after-pre-commit",
+      "detail": "Typecheck the library after running pre-commit",
+      "type": "shell",
+      "command": "make",
+      "args": ["check"],
+      "problemMatcher": [],
+      "group": { "kind": "build" },
+      "dependsOn": "pre-commit",
+      "presentation": {
+        "panel": "dedicated",
+        "clear": true
+      },
+      "hide": true
+    },
     {
       "label": "pre-commit",
       "detail": "Check and fix code conventions",

src/commutative-algebra/commutative-rings.lagda.md

@@ -142,7 +142,7 @@ module _
 
   commutative-add-Commutative-Ring :
     (x y : type-Commutative-Ring) →
-    Id (add-Commutative-Ring x y) (add-Commutative-Ring y x)
+    add-Commutative-Ring x y ＝ add-Commutative-Ring y x
   commutative-add-Commutative-Ring = commutative-add-Ab ab-Commutative-Ring
 
   interchange-add-add-Commutative-Ring :
@@ -335,8 +335,8 @@ module _
   mul-Commutative-Ring' = mul-Ring' ring-Commutative-Ring
 
   ap-mul-Commutative-Ring :
-    {x x' y y' : type-Commutative-Ring} (p : Id x x') (q : Id y y') →
-    Id (mul-Commutative-Ring x y) (mul-Commutative-Ring x' y')
+    {x x' y y' : type-Commutative-Ring} (p : x ＝ x') (q : y ＝ y') →
+    mul-Commutative-Ring x y ＝ mul-Commutative-Ring x' y'
   ap-mul-Commutative-Ring p q = ap-binary mul-Commutative-Ring p q
 
   associative-mul-Commutative-Ring :
@@ -353,19 +353,15 @@ module _
 
   left-distributive-mul-add-Commutative-Ring :
     (x y z : type-Commutative-Ring) →
-    ( mul-Commutative-Ring x (add-Commutative-Ring y z)) ＝
-    ( add-Commutative-Ring
-      ( mul-Commutative-Ring x y)
-      ( mul-Commutative-Ring x z))
+    mul-Commutative-Ring x (add-Commutative-Ring y z) ＝
+    add-Commutative-Ring (mul-Commutative-Ring x y) (mul-Commutative-Ring x z)
   left-distributive-mul-add-Commutative-Ring =
     left-distributive-mul-add-Ring ring-Commutative-Ring
 
   right-distributive-mul-add-Commutative-Ring :
     (x y z : type-Commutative-Ring) →
-    ( mul-Commutative-Ring (add-Commutative-Ring x y) z) ＝
-    ( add-Commutative-Ring
-      ( mul-Commutative-Ring x z)
-      ( mul-Commutative-Ring y z))
+    mul-Commutative-Ring (add-Commutative-Ring x y) z ＝
+    add-Commutative-Ring (mul-Commutative-Ring x z) (mul-Commutative-Ring y z)
   right-distributive-mul-add-Commutative-Ring =
     right-distributive-mul-add-Ring ring-Commutative-Ring
 
@@ -656,11 +652,10 @@ module _
 
   preserves-concat-add-list-Commutative-Ring :
     (l1 l2 : list type-Commutative-Ring) →
-    Id
-      ( add-list-Commutative-Ring (concat-list l1 l2))
-      ( add-Commutative-Ring
-        ( add-list-Commutative-Ring l1)
-        ( add-list-Commutative-Ring l2))
+    add-list-Commutative-Ring (concat-list l1 l2) ＝
+    add-Commutative-Ring
+      ( add-list-Commutative-Ring l1)
+      ( add-list-Commutative-Ring l2)
   preserves-concat-add-list-Commutative-Ring =
     preserves-concat-add-list-Ring ring-Commutative-Ring
 ```

src/commutative-algebra/commutative-semirings.lagda.md

@@ -200,19 +200,19 @@ module _
 
   left-distributive-mul-add-Commutative-Semiring :
     (x y z : type-Commutative-Semiring) →
-    ( mul-Commutative-Semiring x (add-Commutative-Semiring y z)) ＝
-    ( add-Commutative-Semiring
+    mul-Commutative-Semiring x (add-Commutative-Semiring y z) ＝
+    add-Commutative-Semiring
       ( mul-Commutative-Semiring x y)
-      ( mul-Commutative-Semiring x z))
+      ( mul-Commutative-Semiring x z)
   left-distributive-mul-add-Commutative-Semiring =
     left-distributive-mul-add-Semiring semiring-Commutative-Semiring
 
   right-distributive-mul-add-Commutative-Semiring :
     (x y z : type-Commutative-Semiring) →
-    ( mul-Commutative-Semiring (add-Commutative-Semiring x y) z) ＝
-    ( add-Commutative-Semiring
+    mul-Commutative-Semiring (add-Commutative-Semiring x y) z ＝
+    add-Commutative-Semiring
       ( mul-Commutative-Semiring x z)
-      ( mul-Commutative-Semiring y z))
+      ( mul-Commutative-Semiring y z)
   right-distributive-mul-add-Commutative-Semiring =
     right-distributive-mul-add-Semiring semiring-Commutative-Semiring
 

src/commutative-algebra/euclidean-domains.lagda.md

@@ -72,7 +72,7 @@ is-euclidean-valuation R v =
   ( is-nonzero-Integral-Domain R y) →
   Σ ( type-Integral-Domain R × type-Integral-Domain R)
     ( λ (q , r) →
-      ( Id x (add-Integral-Domain R (mul-Integral-Domain R q y) r)) ×
+      ( x ＝ add-Integral-Domain R (mul-Integral-Domain R q y) r) ×
         ( is-zero-Integral-Domain R r +
         ( v r <-ℕ v y)))
 ```
@@ -178,7 +178,7 @@ module _
 
   commutative-add-Euclidean-Domain :
     (x y : type-Euclidean-Domain) →
-    Id (add-Euclidean-Domain x y) (add-Euclidean-Domain y x)
+    add-Euclidean-Domain x y ＝ add-Euclidean-Domain y x
   commutative-add-Euclidean-Domain = commutative-add-Ab ab-Euclidean-Domain
 
   interchange-add-add-Euclidean-Domain :
@@ -334,8 +334,8 @@ module _
     mul-Integral-Domain' integral-domain-Euclidean-Domain
 
   ap-mul-Euclidean-Domain :
-    {x x' y y' : type-Euclidean-Domain} (p : Id x x') (q : Id y y') →
-    Id (mul-Euclidean-Domain x y) (mul-Euclidean-Domain x' y')
+    {x x' y y' : type-Euclidean-Domain} (p : x ＝ x') (q : y ＝ y') →
+    mul-Euclidean-Domain x y ＝ mul-Euclidean-Domain x' y'
   ap-mul-Euclidean-Domain p q = ap-binary mul-Euclidean-Domain p q
 
   associative-mul-Euclidean-Domain :
@@ -352,20 +352,16 @@ module _
 
   left-distributive-mul-add-Euclidean-Domain :
     (x y z : type-Euclidean-Domain) →
-    ( mul-Euclidean-Domain x (add-Euclidean-Domain y z)) ＝
-    ( add-Euclidean-Domain
-      ( mul-Euclidean-Domain x y)
-      ( mul-Euclidean-Domain x z))
+    mul-Euclidean-Domain x (add-Euclidean-Domain y z) ＝
+    add-Euclidean-Domain (mul-Euclidean-Domain x y) (mul-Euclidean-Domain x z)
   left-distributive-mul-add-Euclidean-Domain =
     left-distributive-mul-add-Integral-Domain
       integral-domain-Euclidean-Domain
 
   right-distributive-mul-add-Euclidean-Domain :
     (x y z : type-Euclidean-Domain) →
-    ( mul-Euclidean-Domain (add-Euclidean-Domain x y) z) ＝
-    ( add-Euclidean-Domain
-      ( mul-Euclidean-Domain x z)
-      ( mul-Euclidean-Domain y z))
+    mul-Euclidean-Domain (add-Euclidean-Domain x y) z ＝
+    add-Euclidean-Domain (mul-Euclidean-Domain x z) (mul-Euclidean-Domain y z)
   right-distributive-mul-add-Euclidean-Domain =
     right-distributive-mul-add-Integral-Domain
       integral-domain-Euclidean-Domain
@@ -635,11 +631,10 @@ module _
 
   preserves-concat-add-list-Euclidean-Domain :
     (l1 l2 : list type-Euclidean-Domain) →
-    Id
-      ( add-list-Euclidean-Domain (concat-list l1 l2))
-      ( add-Euclidean-Domain
-        ( add-list-Euclidean-Domain l1)
-        ( add-list-Euclidean-Domain l2))
+    add-list-Euclidean-Domain (concat-list l1 l2) ＝
+    add-Euclidean-Domain
+      ( add-list-Euclidean-Domain l1)
+      ( add-list-Euclidean-Domain l2)
   preserves-concat-add-list-Euclidean-Domain =
     preserves-concat-add-list-Integral-Domain
       integral-domain-Euclidean-Domain
@@ -677,13 +672,12 @@ module _
   equation-euclidean-division-Euclidean-Domain :
     ( x y : type-Euclidean-Domain) →
     ( p : is-nonzero-Euclidean-Domain y) →
-    ( Id
-      ( x)
-      ( add-Euclidean-Domain
-        ( mul-Euclidean-Domain
-          ( quotient-euclidean-division-Euclidean-Domain x y p)
-          ( y))
-        ( remainder-euclidean-division-Euclidean-Domain x y p)))
+    x ＝
+    add-Euclidean-Domain
+      ( mul-Euclidean-Domain
+        ( quotient-euclidean-division-Euclidean-Domain x y p)
+        ( y))
+      ( remainder-euclidean-division-Euclidean-Domain x y p)
   equation-euclidean-division-Euclidean-Domain x y p =
     pr1 (pr2 (pr2 is-euclidean-domain-Euclidean-Domain x y p))
 

src/commutative-algebra/function-commutative-semirings.lagda.md

@@ -150,7 +150,8 @@ module _
   right-distributive-mul-add-function-Commutative-Semiring :
     (f g h : type-function-Commutative-Semiring) →
     mul-function-Commutative-Semiring
-      ( add-function-Commutative-Semiring f g) h ＝
+      ( add-function-Commutative-Semiring f g)
+      ( h) ＝
     add-function-Commutative-Semiring
       ( mul-function-Commutative-Semiring f h)
       ( mul-function-Commutative-Semiring g h)

src/commutative-algebra/integral-domains.lagda.md

@@ -147,7 +147,7 @@ module _
 
   commutative-add-Integral-Domain :
     (x y : type-Integral-Domain) →
-    Id (add-Integral-Domain x y) (add-Integral-Domain y x)
+    add-Integral-Domain x y ＝ add-Integral-Domain y x
   commutative-add-Integral-Domain = commutative-add-Ab ab-Integral-Domain
 
   interchange-add-add-Integral-Domain :
@@ -303,8 +303,8 @@ module _
     mul-Commutative-Ring' commutative-ring-Integral-Domain
 
   ap-mul-Integral-Domain :
-    {x x' y y' : type-Integral-Domain} (p : Id x x') (q : Id y y') →
-    Id (mul-Integral-Domain x y) (mul-Integral-Domain x' y')
+    {x x' y y' : type-Integral-Domain} (p : x ＝ x') (q : y ＝ y') →
+    mul-Integral-Domain x y ＝ mul-Integral-Domain x' y'
   ap-mul-Integral-Domain p q = ap-binary mul-Integral-Domain p q
 
   associative-mul-Integral-Domain :
@@ -321,20 +321,16 @@ module _
 
   left-distributive-mul-add-Integral-Domain :
     (x y z : type-Integral-Domain) →
-    ( mul-Integral-Domain x (add-Integral-Domain y z)) ＝
-    ( add-Integral-Domain
-      ( mul-Integral-Domain x y)
-      ( mul-Integral-Domain x z))
+    mul-Integral-Domain x (add-Integral-Domain y z) ＝
+    add-Integral-Domain (mul-Integral-Domain x y) (mul-Integral-Domain x z)
   left-distributive-mul-add-Integral-Domain =
     left-distributive-mul-add-Commutative-Ring
       commutative-ring-Integral-Domain
 
   right-distributive-mul-add-Integral-Domain :
     (x y z : type-Integral-Domain) →
-    ( mul-Integral-Domain (add-Integral-Domain x y) z) ＝
-    ( add-Integral-Domain
-      ( mul-Integral-Domain x z)
-      ( mul-Integral-Domain y z))
+    mul-Integral-Domain (add-Integral-Domain x y) z ＝
+    add-Integral-Domain (mul-Integral-Domain x z) (mul-Integral-Domain y z)
   right-distributive-mul-add-Integral-Domain =
     right-distributive-mul-add-Commutative-Ring
       commutative-ring-Integral-Domain
@@ -604,11 +600,10 @@ module _
 
   preserves-concat-add-list-Integral-Domain :
     (l1 l2 : list type-Integral-Domain) →
-    Id
-      ( add-list-Integral-Domain (concat-list l1 l2))
-      ( add-Integral-Domain
-        ( add-list-Integral-Domain l1)
-        ( add-list-Integral-Domain l2))
+    add-list-Integral-Domain (concat-list l1 l2) ＝
+    add-Integral-Domain
+      ( add-list-Integral-Domain l1)
+      ( add-list-Integral-Domain l2)
   preserves-concat-add-list-Integral-Domain =
     preserves-concat-add-list-Commutative-Ring
       commutative-ring-Integral-Domain

src/commutative-algebra/products-commutative-rings.lagda.md

@@ -87,37 +87,34 @@ module _
 
   left-inverse-law-add-product-Commutative-Ring :
     (x : type-product-Commutative-Ring) →
-    Id
-      ( add-product-Commutative-Ring (neg-product-Commutative-Ring x) x)
-      zero-product-Commutative-Ring
+    add-product-Commutative-Ring (neg-product-Commutative-Ring x) x ＝
+    zero-product-Commutative-Ring
   left-inverse-law-add-product-Commutative-Ring =
     left-inverse-law-add-product-Ring
       ( ring-Commutative-Ring R1)
       ( ring-Commutative-Ring R2)
 
   right-inverse-law-add-product-Commutative-Ring :
     (x : type-product-Commutative-Ring) →
-    Id
-      ( add-product-Commutative-Ring x (neg-product-Commutative-Ring x))
-      ( zero-product-Commutative-Ring)
+    add-product-Commutative-Ring x (neg-product-Commutative-Ring x) ＝
+    zero-product-Commutative-Ring
   right-inverse-law-add-product-Commutative-Ring =
     right-inverse-law-add-product-Ring
       ( ring-Commutative-Ring R1)
       ( ring-Commutative-Ring R2)
 
   associative-add-product-Commutative-Ring :
     (x y z : type-product-Commutative-Ring) →
-    Id
-      ( add-product-Commutative-Ring (add-product-Commutative-Ring x y) z)
-      ( add-product-Commutative-Ring x (add-product-Commutative-Ring y z))
+    ( add-product-Commutative-Ring (add-product-Commutative-Ring x y) z) ＝
+    ( add-product-Commutative-Ring x (add-product-Commutative-Ring y z))
   associative-add-product-Commutative-Ring =
     associative-add-product-Ring
       ( ring-Commutative-Ring R1)
       ( ring-Commutative-Ring R2)
 
   commutative-add-product-Commutative-Ring :
     (x y : type-product-Commutative-Ring) →
-    Id (add-product-Commutative-Ring x y) (add-product-Commutative-Ring y x)
+    add-product-Commutative-Ring x y ＝ add-product-Commutative-Ring y x
   commutative-add-product-Commutative-Ring =
     commutative-add-product-Ring
       ( ring-Commutative-Ring R1)
@@ -140,49 +137,46 @@ module _
 
   associative-mul-product-Commutative-Ring :
     (x y z : type-product-Commutative-Ring) →
-    Id
-      ( mul-product-Commutative-Ring (mul-product-Commutative-Ring x y) z)
-      ( mul-product-Commutative-Ring x (mul-product-Commutative-Ring y z))
+    ( mul-product-Commutative-Ring (mul-product-Commutative-Ring x y) z) ＝
+    ( mul-product-Commutative-Ring x (mul-product-Commutative-Ring y z))
   associative-mul-product-Commutative-Ring =
     associative-mul-product-Ring
       ( ring-Commutative-Ring R1)
       ( ring-Commutative-Ring R2)
 
   left-unit-law-mul-product-Commutative-Ring :
     (x : type-product-Commutative-Ring) →
-    Id (mul-product-Commutative-Ring one-product-Commutative-Ring x) x
+    mul-product-Commutative-Ring one-product-Commutative-Ring x ＝ x
   left-unit-law-mul-product-Commutative-Ring =
     left-unit-law-mul-product-Ring
       ( ring-Commutative-Ring R1)
       ( ring-Commutative-Ring R2)
 
   right-unit-law-mul-product-Commutative-Ring :
     (x : type-product-Commutative-Ring) →
-    Id (mul-product-Commutative-Ring x one-product-Commutative-Ring) x
+    mul-product-Commutative-Ring x one-product-Commutative-Ring ＝ x
   right-unit-law-mul-product-Commutative-Ring =
     right-unit-law-mul-product-Ring
       ( ring-Commutative-Ring R1)
       ( ring-Commutative-Ring R2)
 
   left-distributive-mul-add-product-Commutative-Ring :
     (x y z : type-product-Commutative-Ring) →
-    Id
-      ( mul-product-Commutative-Ring x (add-product-Commutative-Ring y z))
-      ( add-product-Commutative-Ring
-        ( mul-product-Commutative-Ring x y)
-        ( mul-product-Commutative-Ring x z))
+    mul-product-Commutative-Ring x (add-product-Commutative-Ring y z) ＝
+    add-product-Commutative-Ring
+      ( mul-product-Commutative-Ring x y)
+      ( mul-product-Commutative-Ring x z)
   left-distributive-mul-add-product-Commutative-Ring =
     left-distributive-mul-add-product-Ring
       ( ring-Commutative-Ring R1)
       ( ring-Commutative-Ring R2)
 
   right-distributive-mul-add-product-Commutative-Ring :
     (x y z : type-product-Commutative-Ring) →
-    Id
-      ( mul-product-Commutative-Ring (add-product-Commutative-Ring x y) z)
-      ( add-product-Commutative-Ring
-        ( mul-product-Commutative-Ring x z)
-        ( mul-product-Commutative-Ring y z))
+    mul-product-Commutative-Ring (add-product-Commutative-Ring x y) z ＝
+    add-product-Commutative-Ring
+      ( mul-product-Commutative-Ring x z)
+      ( mul-product-Commutative-Ring y z)
   right-distributive-mul-add-product-Commutative-Ring =
     right-distributive-mul-add-product-Ring
       ( ring-Commutative-Ring R1)