Skip to content
Go to file

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time


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.

An icosahedron for your viewing pleasure

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


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.



No releases published


No packages published