Symmetry, checked by Narya

symmetry-narya is a formalization of the book Symmetry by Bezem, Buchholtz, Cagne, Dundas and Grayson, in the Narya proof assistant (default HOTT mode). It covers chapters 2 to 15 and appendix B. 888 of the 917 blocks of the book have a formal statement and a proof. 19 blocks are false as printed: for each of them, the repository proves a counterexample and a corrected statement.

Source code on GitHub (GPL-3.0-or-later) · Build and check · Book notes

book

xca:cancel-surjection (circle.tex:3104)

A surjection p : A → B gives an equivalence
(f = g) → (f ∘ p = g ∘ p), for all Y and f, g : B → Y.

Narya

module 40: a counterexample

def surjection_cancellation_counterexample
  (e : isEquiv (Id (TwoSets → TwoSets) (identity TwoSets) two_sets_constant_base)
      (Id (Unit → TwoSets) … …)
      (map_path … (precompose Unit TwoSets TwoSets two_sets_base_inclusion) …))
  : Empty

fix

the corrected statement, for a set Y

def cancel_surjection_into_set (A B Y : Type) (p : A → B)
  (hp : Surjective A B p) (hy : isSet Y) (f g : B → Y)
  : Equiv (Id (B → Y) f g) (Id (A → Y) (precompose A B Y p f) (precompose A B Y p g))

One of the 19 corrections. With A = Unit, B = Y = TwoSets (the groupoid of two-element sets) and p the inclusion of the base point, the identity and the constant map agree after p but are not equal. Module 285 proves the general form for n-connected maps.

917blocks of the book

888with a formal statement and a proof

19false as printed, with counterexamples

864of 1,140 claims of the running text formalized

812Narya modules

2 h 19full check from source, 27 GB

Chapters

Each chapter has a status page in the repository. It lists the open gaps and the corrections, and links each block of the book to its principal declarations.

chapter	blocks	mapped	refuted	partial	informal	open gaps
Chapter 2: An introduction to univalent mathematics	196	196	0	0	0	2
Chapter 3: The universal symmetry: the circle	102	101	1	0	0	10
Chapter 4: Groups, concretely	95	92	3	0	0	8
Chapter 5: Actions	112	110	1	0	1	11
Chapter 6: A categorical interlude	89	89	0	0	0	10
Chapter 7: Groups, abstractly	51	48	3	0	0	4
Chapter 8: Constructing groups	39	36	0	0	3	2
Chapter 9: Normal subgroups and quotients	71	66	5	0	0	5
Chapter 10: Finite groups	19	17	1	1	0	5
Chapter 11: Group presentations	36	29	3	3	1	10
Chapter 12: Abelian groups	19	19	0	0	0	2
Chapter 13: Rings, fields and vector spaces	44	43	0	0	1	2
Chapter 14: Geometry and groups	19	19	0	0	0	5
Chapter 15: Galois theory	7	5	2	0	0	3
Appendix B: Metamathematical remarks	18	18	0	0	0	10
Total	917	888	19	4	6	89

Blocks are the definitions, lemmas, theorems, constructions, exercises, examples and remarks of the book. Mapped: a formal statement and a proof. Refuted: false as printed; a counterexample and a corrected statement are proved. Open gaps: partial blocks, gaps of the blind check, and claims of the running text that are not formalized or only partly formalized.

Blind statement check

The main risk of a formalization is a formal statement that does not say what the book says. For chapters 4 to 15 and appendix B, a second set of statements was written from the book text only, without the formal code of the chapter. Bridge files then derive each blind statement from the main declarations.

547blind statements derived

16derived after a correction; the literal statement is refuted

5gaps, each with a note

15blocks with no mathematical claim

How the result is checked

Full check: make check typechecks all modules from source with the pinned Narya. It rejects axioms and holes in the sources and in the diagnostics of Narya, and records the hashes of the sources and of the executable. The last run took 2 h 19 min and 27 GB of memory on one core of an x86_64 Linux server.
Negative controls: Two false proofs must fail with a type mismatch, so that a broken setup cannot pass silently.
Book mapping: Each block has a note that gives every difference between the formal statement and the printed text. The mappings need mathematical review: a successful typecheck does not show that a statement agrees with the book.

Foundations

The proofs use the native Id, transport and univalence of Narya. Module 20 proves the two inverse laws of univalence.
The pinned Narya has no higher inductive types. A signature record gives each higher inductive type of the book with its induction and computation laws, for example CircleSignature.
Where the book needs a specific object, the repository constructs it. The circle is the component of the infinite cycle (Int, succ) in the type of cycles. Propositional truncation is an impredicative encoding.
Smallness predicates model the universes of the book. Resizing, replacement and classical principles are explicit hypotheses where a proof uses them.

Limits

The pinned Narya has Type : Type and no checker for termination, positivity or productivity. Thus a successful typecheck is not a consistency result. A heuristic lint scans for unrecognized recursion and non-positive datatypes, but a pass does not prove soundness.

narya-mcp, an MCP server for Narya, was measured on this formalization. Errors of Narya found during the work have reproducers in tests/narya.