SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

Style guide

• Try to be informal. Use as few formulas as possible, especially for the parts about type theory and logic, to ease the entry into group theory.
• We call objects in a type elements of that type even if the type is not a set.
• An element of a proposition can be called a proof.
• An element of an identity type is called an identification, and otherwise a path. We may say that it shows how to identify two elements. We may say it establishes that two elements are equal provided the identity type is a proposition.
• The type containing the variable in a family is called the "parameter type", not the "index type", nor the "base type".
• Definitional equality is denoted with three lines and is called just that, i.e., definitional and not judgmental.
• A synonym of "function" is "map". We don't use "mapping" or "application" as synonyms.
• In the preliminary chapters (up to subgroups), the underlying set map U from groups to sets has to be applied explicitly. Thereafter, it can be a coercion.
• Composition of p: a=b and q: b=c is denoted by either p\ct q, or by q\cdot p, qp or q\circ p. The latter is preferred when p and q come from equivalences. The macro \ct currently produces a star.
• In dependent pairs, components having propositional type may be omitted.
• If x is a bound variable and c is less bound, then we prefer c = x to x = c. Typically, if c is the center of contraction.
• If k and n are number variables that can be renamed, then we prefer k < n to k > n or n < k.
• up to versus modulo regarding a group action: Up to is the stacky version, the orbit type (typically for us, a groupoid), whereas modulo refers to the set of connected components/the set of orbits. For example, given a group G, we have the groupoid of elements up to conjugation versus the set of elements modulo conjugation.
• Globally defined constants are typeset roman, while variables are italic. One exception is the B construction: The B matches whatever it operates on and joins to it without any space.
• Whenever possible, do not use a letter for a variable when the same letter is being used as an operator. E.g., try to avoid a variable B when the classifying type/map operator B is used in the same paragraph.
• Use macros with mathematical meaning, such as \conncomp, whenever possible, for uniformity of notation.
• Avoid the use of acronyms, such as LEM and LPO.
• Construct sort-order keys for glossary entries this way:
  • for unary operators, use 1 followed by something (e.g., for $-y$ use (1-);
  • for binary operators, use 2 followed by something (e.g., for $x+y$ use (2+);
  • for numbers, use 8 followed by the number (e.g., for $0$ use (80).
  • for identifiers in the Greek alphabet use 9 followed by the 2-digit ordinal number of the first letter (for proper alphabetization) and then something (e.g., for $\loops$ use (924Omega): 01 Α α, 02 Β β, 03 Γ γ, 04 Δ δ, 05 Ε ε, 06 Ζ ζ, 07 Η η, 08 Θ θ, 09 Ι ι, 10 Κ κ, 11 Λ λ, 12 Μ μ, 13 Ν ν, 14 Ξ ξ, 15 Ο ο, 16 Π π, 17 Ρ ρ, 18 Σ σ, 19 Τ τ, 20 Υ υ, 21 Φ φ, 22 Χ χ, 23 Ψ ψ, and 24 Ω ω;
  • for identifiers in the Roman alphabet use the name (e.g., for $\Ker$ use (Ker) or (ker);
• Given a: A, we refer to elements of a = a as either symmetries of a, or symmetries in A.

Current draft of the book

Go here for the current draft of the book.

An icosahedron for your viewing pleasure

Go here for an interactive icosahedron and here for a Cayley diagram of the icosahedral group.

Shield:

This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.