READ THE ARGUMENT. INSPECT THE EVIDENCE.
Familiar mathematics.
Every step checked.
Explore proofs in homotopy type theory. Follow the mathematical argument, open a definition, and inspect the kernel terms behind it.
Explore the proof libraryStart with a highlight
Seven entry points into the library.
Infinitely many primes
Euclid’s argument: take a prime divisor of n! + 1 and show that it is larger than n. A short proof with definitions you can follow.
No axioms required. Read Euclid’s proof HOMOTOPY TYPE THEORYThe circle’s fundamental group
Winding number gives a group isomorphism from the circle’s loops to the additive group of integers. Its inverse turns each integer into a loop, and loop composition corresponds to addition.
Uses univalence, function extensionality, and the suspension construction of S¹. Explore loops and integers ALGEBRA & UNIVALENCEIsomorphic groups are equal
The type of group isomorphisms is equal to the type of equalities between groups. Univalence identifies the types themselves, preserving the full structures: carriers, operations, and laws.
Uses univalence and function extensionality. Explore equality of structures GALOIS THEORY & HOMOTOPYField symmetries are loops
Frobenius exchanges two roots in the four-element field. Univalence turns this symmetry into a nontrivial loop of field extensions; going around twice gives the identity.
Uses univalence and function extensionality. No excluded middle or choice. Explore the two symmetries SETS & MAPSCantor–Schröder–Bernstein
If each of two sets injects into the other, they are equivalent. Follow the construction of a bijection from the two injections.
For sets; uses excluded middle. Read the proof FINITE TYPES & COUNTINGPascal’s identity, as a bijection
Split subsets into those that contain a chosen element and those that do not. Pascal’s rule becomes an explicit bijection between finite types.
Inspect the maps and both inverse laws. Explore the bijection FINITE TYPES & COUNTINGWhy there are n! permutations
Choose the image of one element, then permute the rest. A recursive bijection counts permutations of an n-element type.
Counts permutations themselves, including their inverse data. Follow the counting argument SETS & CHOICEEvery surjection has a right inverse
Apply choice to the fibers of a surjection between sets. The conclusion records mere existence of a right inverse.
Uses the set-level axiom of choice. Inspect the role of choice