Merge pull request #775 from ecavallo/algebra-naming

Aspirational algebra naming conventions

Cubical/Algebra/NAMING.md

@@ -0,0 +1,83 @@
+NAMING
+======
+
+This file provides a guide for naming definitions in the Algebra folder.
+
+* To name a property of an operation, write the name of the operation
+  first, then the property. For example, `+Comm` or `·Assoc`.
+
+* Use the following names and abbreviations for common properties.
+  For laws that have left and right versions, use a suffix `L` or `R`.
+  Check below to see which version is `L` and which is `R`.
+  - `Assoc` = associativity
+
+    ```
+    ·Assoc : x · (y · z) ≡ (x · y) · z
+    ```
+
+  - `Comm` = commutativity
+
+    ```
+    ·Comm : x · y ≡ y · x
+    ·CommL : x · (y · z) ≡ y · (x · z)
+    ·CommR : (x · y) · z ≡ (x · z) · y
+    ```
+
+  - `Dist` = distributivity. The name should show first the operation
+    that is distributed, whether it is distributing over the left or
+    right, and then the operation that is distributed over.
+
+    ```
+    x · (y + z) ≡ (x · y) + (x · z)
+    ```
+
+  - `Id` = unit laws
+
+    ```
+    ·IdL : 1 · x ≡ x
+    -Id : (- 0) ≡ 0
+    ```
+
+  - `Inv` = inverse laws
+
+    ```
+    +InvL : (- x) + x ≡ 0
+    ```
+
+  - `Absorb` = absorption. The name should show first the outer
+    operation, whether it is absorbed on the left, then the inner
+    operation.
+
+    ```
+    ∧AbsorbL∨ : x ∧ (x ∨ y) ≡ x
+    ```
+
+  - `Invol` = involution
+
+    ```
+    -Invol : - (- x) ≡ x
+    ```
+
+  - `Cancel` = cancellation
+
+    ```
+    ·CancelL : x · a ≡ x · b → a ≡ b
+    ```
+
+  - `Annihil` = annihilation
+
+    ```
+    ·AnnihilL : 0 · x ≡ 0
+    ```
+
+  - `Idem` = idempotency
+
+    ```
+    ∧Idem : x ∧ x ≡ x
+    ```
+
+* The fact that a homomorphism preserves a specific operation
+  should be named `pres·` where `·` is the operation.
+
+* An instance of an algebraic structure should include the
+  name of the structure. For example `UnitGroup` and `ℤGroup`.

NAMING.md

@@ -4,6 +4,9 @@ NAMING
 This file provides a guide for how to name things. Note that many
 files in the library do not currently follow these guidelines.
 
+For naming conventions specific to the Algebra subfolder, see
+[Cubical/Algebra/NAMING.md](https://github.com/agda/cubical/blob/master/Cubical/Algebra/NAMING.md).
+
 * Use either descriptive names for universe levels or
   ```
   ℓ ℓ' ℓ'' ℓ''' ...
@@ -22,6 +25,9 @@ files in the library do not currently follow these guidelines.
 * Use camelCase as much as possible, also for properties/lemmas
   related to operations. For example: `+Assoc`, `·DistR+`.
 
+* Avoid referring to variable names in the names of definitions.
+  For example, prefer `+Comm` to something like `m+n≡n+m`.
+
 * Use Equiv or `≃` to refer to equivalences of types or structures.
 
 * Use Iso or `≅` to refer to isomorphisms of types or structures.
@@ -38,4 +44,3 @@ files in the library do not currently follow these guidelines.
   should appear in the order they appear in the type (like
   `isContrUnit`). For functions things can either be separated by `→`
   (like `isProp→isSet`) or `To` (like `isoToEquiv`).
-