Naming convention for algebra related code

[mortberg]

It would be nice if all the algebra would be using some more consistent naming schema. Here's a suggestion that we are more or less following:

• First letter of structure names and types should be uppercase (like Ring)
• Use appropriate abbreviation:
  • Comm = commutative
  • Assoc = associative
  • DistR/DistL = distribute right/left
• Use camelCase as much as possible, also for properties/lemmas related to operations. For example
  • +Assoc
  • ·DistR+

I'm not sure about how to name lemmas like these: https://github.com/agda/cubical/blob/master/Cubical/Structures/Ring.agda#L272

This should be implemented after https://github.com/agda/cubical/pull/401

[mchristianl]

Would it be "safe" to rename every occurrence of _*_ to _·_ in the Cubical/Algebra subdirectory?

[mortberg]

Would it be "safe" to rename every occurrence of _*_ to _·_ in the Cubical/Algebra subdirectory?

Sure! I think this should be the name for multiplication of numbers as well

[mortberg]

(just to be clear, it's \cdot not \.)

[mchristianl]

The * is currently used in

• Algebra/CommRing
• Data/BinNat (just a comment)
• Data/Fin
• Data/InfNat
• Data/Nat
• Data/NatPlusOne
• Data/Sigma
• Data/Unit
• (Data/Vec)
• HITs/AssocList
• HITs/Colimit ("lower star functor" should remain *)
• HITs/FiniteMultiset
• (HITs/Hopf)
• HITs/Ints/BiInvInt
• HITs/Ints/QuoInt
• HITs/ListedFiniteSet
• (HITs/Rationals/HITQ)
• HITs/Rationals/QuoQ
• HITs/Rationals/SigmaQ
• HITs/RPn
• HITs/S1 (debatable)
• HITs/Truncation
• HITs/Truncation/FromNegTwo
• Homotopy/Connected
• Modalities/Modality
• (Papers/Synthetic)
• Structures/Auto
• Structures/Relational/Auto
• ZCohomology/MayerVietorisUnreduced

Where I would replace it with \cdot in the fat marked parts. What about HITs/S1?

[mortberg]

I agree with all the fat marked parts. For the circle I think it's bad style that there is a definition rot which is then renamed to an operator. There should only be one of these, so please open another issue about this and leave it as it is for now.

[mchristianl]

I found that there are a lot algebraic properties that "preserve" or "reflect" a relation. The non-cubical standard library defines preservation like

_on_ : (B → B → C) → (A → B) → (A → A → C)
_*_ on f = f -⟨ _*_ ⟩- f

_=[_]⇒_ : Rel A ℓ₁ → (A → B) → Rel B ℓ₂ → Set _
P =[ f ]⇒ Q = P ⇒ (Q on f)

_Preserves_⟶_ : (A → B) → Rel A ℓ₁ → Rel B ℓ₂ → Set _
f Preserves P ⟶ Q = P =[ f ]⇒ Q

where _on_ is built up here.

In my own code, I've settled with a naming scheme like

suc-preserves-< : ∀ a b → a < b → suc a < suc b
suc-reflects-< : ∀ a b → suc a < suc b → a < b
suc-creates-< : ∀ a b → (suc a < suc b) ⇔ (a < b)

where the nomer "creates" was a hint from the agda irc channel.

Would such a naming scheme be applicable for the cubical standard library?

PS: The non-cubical standard library seems to use the nomer "mono" for such properties

pred-mono : pred Preserves _≤_ ⟶ _≤_

and uses "reflects" differently

-- The truth value of P is reflected by a boolean value.
data Reflects {p} (P : Set p) : Bool → Set p where
  ofʸ : ( p :   P) → Reflects P true
  ofⁿ : (¬p : ¬ P) → Reflects P false

[mortberg]

Leaving this open for now, but should be fixed very soon by