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.
• definitional equivality is denoted with three lines and is called just that, i.e., definitional and not judgmental.
• 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.
• 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.