In ordinary type theory, a proof that $a = b$ is just a certificate. In homotopy type theory, it is a path from $a$ to $b$ in a space, and two such paths need not be the same. A proof that two proofs of $a = b$ are equal is then a deformation of one path into the other. The univalence axiom says that two types with a one-to-one correspondence between them are equal, so isomorphic structures can always be swapped. This matches how mathematicians already treat isomorphic objects.

On the real line, the length of an interval does not change when the interval is shifted. A Haar measure is a way of assigning sizes to subsets of a group with the same property: moving a set by a group element keeps its size. On the circle it is arc length, on a finite group it counts points, and on the positive reals under multiplication it is $dx/x$. Indeed, the interval $[a, b]$ has measure $\log(b/a)$ for $dx/x$, and multiplying it by $c > 0$ gives $[ca, cb]$ with the same measure.

If some energy-like quantity decreases along all motions near an equilibrium, the motions stay near it. If the quantity decreases strictly, the motions must also run down to the equilibrium.

The integer points $\Z^2$ form a grid in the plane, and the grid squares tile the plane by shifts. Each tile has area $1$, so the plane "folded up" by the grid, which is a torus, has finite area. A lattice in a general group is the same idea: a discrete subgroup whose translates of one region of finite volume cover the group. The group $SL_2(\Z)$ of integer matrices with determinant $1$ sits inside $SL_2(\R)$ in this way, even though the folded-up space is not compact.

In the nineteenth century, geometers counted figures, such as lines meeting other lines or conics touching other conics, with clever but unproven rules. The rules usually gave right answers, but sometimes wrong ones, and nobody knew why. Hilbert asked for a solid foundation that explains when the rules work. The answer came through the theory of intersections and the topology of Grassmannians, developed during the twentieth century.

The Frobenius automorphism of a finite field of characteristic $p$ is the map $x \mapsto x^p$. It generates the group of all automorphisms of the field. The definition of the Frobenius automorphism gives the details.

Look at the values of a function on a small window around a point, and measure the gap between the largest and the smallest of them. Shrink the window and see what this gap tends to. That limit is the oscillation at the point. For the sign function, the values near $0$ are $-1$, $0$ and $1$, so the oscillation at $0$ is $2$.

A finite measure is a way of measuring in which the total amount is finite. Length on the interval $[0, 1]$ is a finite measure, with total $1$. Length on the whole real line is not, since the line is infinitely long. Dividing a nonzero finite measure by its total gives a probability measure.

The maximum principle says that a solution of an elliptic equation cannot have a peak inside the region: its largest value is on the boundary. For a temperature in equilibrium, the hottest point is on the edge, since a hot spot inside would spread its heat to the cooler surroundings. If the largest value is reached inside a connected region, the solution must be constant.

Inside a surface, a chain of ever smaller irreducible pieces can go surface, then a curve on it, then a point on that curve. That chain has two steps, and the surface has dimension $2$. Another way to see it is to count how many coordinates can be chosen freely. On the sphere $x^2 + y^2 + z^2 = 1$ over $\C$, two coordinates are free, and then the third has at most two possible values. So the sphere is a surface, of dimension $2$.

The Lambert W function has many branches, and it is easy to pick the wrong one. The Wright omega function packages the right branch for the input $e^z$ into one function of $z$. On the real line it is simple: $\omega(x)$ is the positive number $y$ with $y + \ln y = x$. For example, $\omega(1) = 1$ because $1 + \ln 1 = 1$.

On a convex set, a field with no swirl is the gradient of a potential. You build the potential by computing the work of the field along straight segments from one base point.

There are several ways to say that two continuous linear forms are close. The weakest asks that they agree nearly at each single vector. The strong one asks that they agree nearly, uniformly, on every bounded set of vectors. For a normed space, being close on the unit ball is the same as being close in the dual norm, so the strong dual is the usual normed dual.

The null space of a matrix is the set of vectors that the matrix sends to zero. It is the solution set of the homogeneous system with this matrix.

A directrix of a conic is a line with the following property. For each point of the conic, the distance to a focus divided by the distance to the line is the same constant. This constant is the eccentricity.

An edge on a cycle is never a bridge: if you delete it, you can still go around the other way. An edge on no cycle has no detour, so deleting it splits the graph.

A commutator $[b, T]$ measures how much the order of two operations matters: first apply $T$ and then multiply by $b$, or first multiply by $b$ and then apply $T$. For a singular integral $T$, the theorem says that this difference is a bounded operator exactly when $b$ has bounded mean oscillation. So BMO is precisely the class of multipliers that almost commute with singular integrals.

1. Let $\varphi : G \to H$ be a group homomorphism with kernel $K$. $K$ is a normal subgroup of $G$, so the quotient group $G/K$ exists.
2. Define $\psi : G/K \to \varphi(G)$ by $\psi(gK) = \varphi(g)$.
3. The map $\psi$ is well defined. If $gK = hK$, then $g^{-1}h \in K$, so $\varphi(g)^{-1}\varphi(h) = e$ and $\varphi(g) = \varphi(h)$.
4. The map $\psi$ is a homomorphism, because $\psi(gK\,hK) = \psi(ghK) = \varphi(gh) = \varphi(g)\varphi(h)$.
5. The map $\psi$ is onto the image $\varphi(G)$, because each $\varphi(g)$ is $\psi(gK)$.
6. If $\psi(gK) = e$, then $\varphi(g) = e$, so $g \in K$ and $gK = K$. Thus the kernel of $\psi$ is trivial, and $\psi$ is injective.
7. Thus $\psi$ is an isomorphism, and $G/K \cong \varphi(G)$.

A geodesic is a critical point of the energy among paths with the same ends, but it need not be a minimum. The index counts the independent ways of shortening it by a small deformation. The theorem says that this number is the number of conjugate points along the way, where nearby geodesics from the start refocus. On a sphere, a great circle arc longer than half the circle passes the antipode of its start, and it can be shortened by sliding it over the sphere.

In such a space, functions that are close in norm are also close at every single point. The value of a function at a point can be read off by taking the inner product with one special function for that point. A simple example: the vectors of $\C^n$, seen as functions on $\set{1, \dots, n}$, form such a space. The special function for the point $i$ is the unit vector $e_i$.