Rename math symbols

[kg583]

A number of math symbols could use some adjustments to their names to improve consistency and ease-of-use. Many proposals have been discussed on Discord, though this PR represents only those with moderate consensus. This PR should remain a draft until all the proposals in the backlog have been majority approved or rejected.

• square as a variant is reserved for symbols containing squares; sq denotes variants that are just "squarer" (e.g. union.sq)
• aleph, beth, and gimmel are the new preferred names for alef, bet, and gimel
• alef, bet, and gimel remain as aliases
• emptyset is an alias for nothing
• gt.curly and lt.curly are aliases for succ and pred
• equiv replaces ident and is an alias for eq.triple
• ident.strict is eq.quad

Many name changes are implemented as aliases for the time being; whether they should remain aliases indefinitely or just until a future release should be determined on a case-by-case basis.

[kg583]

There was a lot of discussion about the "redundancy" of .stroked in variants, but .stroked is in fact the default variant for everything except arrows (for which arrow.fat was discussed as a substitute, but is probably superfluous now). The actual issue lies with the docs, which state .stroked as the canonical variant name. A direct fix to the docs generator is warranted for this, though could occur either in this PR or during the larger rewrite that needs to happen to implement function scopes.

[MDLC01]

I just realised that there is a special, left-to-right, character for the Aleph symbol used to denote transfinite cardinals: U+2135 ℵ ALEF SYMBOL.^1 Similarly, Unicode supports the following characters:

• U+2136 ℶ BET SYMBOL,
• U+2137 ℷ GIMEL SYMBOL, and
• U+2138 ℸ DALET SYMBOL.

Would it be a good idea to add x.symbol (or perhaps x.sym), where x is a letter name, as variables for the symbols mentioned above? Maybe this is too confusing to most people, since the symbols and their corresponding letters are homoglyphs.

[laurmaedje]

Do we want to merge this at some point? :)

[kg583]

Yeah, I suppose its been sitting here long enough. There's still Ryan's comment to address, but other than that we can leave future discussion for a future PR.

[laurmaedje]

I'm okay with Ryan's suggestion.

[kg583]

Each instance of eqq as a variant has been renamed to equiv, and likewise for neqq to nequiv. This conforms pretty well with how approx is used as a variant: napprox exists only as a variant name, with approx.not used for the top level. It also maintains the idea that not strikes out the entire symbol, while nequiv is only the equiv portion struck out (compare tilde.equiv.not and tilde.nequiv).

[laurmaedje]

Thank you all!