In this installment of HoTT Math, we are taking one more step toward elementary field theory by exploring the unit group of a ring. A commutative (unital) ring is a set $R$ with two constants $\mathsf{O},\mathsf{I}:1\to R$, one unary operation ${-\square}:R \to R$, two binary operations ${\square+\square},{\square\cdot\square}:R \times R \to R$ along with the usual axioms: ${\small\fbox{\phantom{b}group\phantom{q}}}(\mathsf{O},-\square,\square+\square)$, ${\small\fbox{\phantom{b}monoid\phantom{q}}}(\mathsf{I},{\square\cdot\square})$, ${\small\fbox{\phantom{b}distributivity\phantom{q}}}({\square+\square},{\square\cdot\square}) : \prod_{x,y,z:R} ((x+y)\cdot z =_R x \cdot z + y \cdot z) \times \prod_{x,y,z:R} (x\cdot(y+z) =_R x \cdot y+x \cdot z),$ and ${\small\fbox{\phantom{b}commutativity\phantom{q}}}({\square\cdot\square}) : \prod_{x,y:R} (x \cdot y =_R y \cdot x).$ Commutativity of addition can be derived as usual using the fact that $x+(x+y)+y =_R (x+y)\cdot(\mathsf{I}+\mathsf{I}) =_R x + (y + x) + y.$ If you want to test your path manipulation skills, you can try to write down the resulting term for ${\small\fbox{\phantom{b}commutativity\phantom{q}}}({\square+\square}) : \prod_{x,y:R} (x + y =_R y+x).$ However, as we discussed last time, this is not necessary since the proof is ultimately not relevant when the carrier of an algebra is a set. Reading off the usual definition of unit, we obtain the type $\operatorname{\mathsf{unit}}(x) :\equiv\sum_{y:R} (x\cdot y =_R \mathsf{I}).$ Elements of type $\operatorname{\mathsf{unit}}(x)$ are pairs $(y,p)$, where $y:R$ and $p: x \cdot y =_R \mathsf{I}$. Because $R$ is a set and inverses are unique, there is always at most one such $(y,p)$, which means that $\operatorname{\mathsf{unit}}(x)$ is a proposition. Therefore, we can comprehend the set of units: $R^\times :\equiv\{x:R \mid \operatorname{\mathsf{unit}}(x)\} :\equiv\sum_{x:R} \operatorname{\mathsf{unit}}(x).$ (Subset comprehension is discussed in §3.5 [...]

Last time, I promised we would look at fields. I have to delay this by one or two installments of HoTT Math since there is so much to say and I am struggling to keep these short. This edition of HoTT Math is a continuation of the first. The main lesson of HoTT Math 1 was that equational logic still works, provided you’re careful enough. As I was working through some algebra, I realized that I should have been more precise and nuanced. To make things more precise, I will briefly recall some basic universal algebra and then I will talk a little about Birkhoff’s soundness and completeness theorem for equational logic. A signature is a sequence $\sigma$ of sets indexed by natural numbers. The elements of the set $\sigma_n$ are intended to be symbols for $n$-ary operations ($0$-ary operations are simply constants). For example, the signature for rings can be thought as $(\{0,1\},\{-\},\{+,\cdot\},\varnothing,\varnothing,\dots).$ It is generally assumed that the sets $\sigma_n$ are mutually disjoint so that each symbol has a definite arity. In the end, only the cardinality of the sets $\sigma_n$ matters since the particular symbols used for the operations is mostly a matter of taste. The logic of universal algebra is equational logic. The symbols from the signature $\sigma$ can be strung together to form terms. In addition to the symbols from $\sigma$, we need an infinite set $\{x_0,x_1,x_2,\dots\}$ of variable symbols. Formally, terms are defined inductively using the two rules: [...]

This is the first in a series of posts on doing mathematics in Homotopy Type Theory (HoTT). Various conventions and notations are explained in the preamble; there are no additional prerequisites for this post. A group is a set $G$ equipped with a constant $e:1 \to G$, a unary operation $\square^{-1}:G \to G$ and a binary operation ${\square\cdot\square}:G \times G \to G$ that satisfy the usual axioms. In HoTT the group axioms must be motivated, so the group $G$ comes with three more components: \begin{aligned} {\small\fbox{\phantom{Q}associativity\phantom{Q}}} &: \prod_{x,y,z:G} (x\cdot(y\cdot z) =_G (x\cdot y)\cdot z) \\ {\small\fbox{\phantom{Q}identity\phantom{Q}}} &: \prod_{x:G} (x \cdot e =_G x) \times \prod_{x:G}(e \cdot x = x)\\ {\small\fbox{\phantom{Q}inverse\phantom{Q}}} &: \prod_{x:G} (e = x^{-1} \cdot x) \times \prod_{x:G} (e =_G x \cdot x^{-1}) \\ \end{aligned} The axioms are concrete objects in proof-relevant mathematics! The last two axioms are actually the conjunction of two axioms since conjunction in HoTT correspond to products. It’s conceptually convenient to package them together and use ${\small\fbox{\phantom{Q}identity\phantom{Q}}}_1$ and ${\small\fbox{\phantom{Q}identity\phantom{Q}}}_2$ for the two conjuncts obtained by applying the projections. In fact, it makes sense to pack all of these into one ${\small\fbox{\phantom{Q}group\phantom{Q}}} :\equiv{\small\fbox{\phantom{Q}associativity\phantom{Q}}}\times{\small\fbox{\phantom{Q}identity\phantom{Q}}}\times{\small\fbox{\phantom{Q}inverse\phantom{Q}}}$ (but, for the sake of clarity, it is best to refrain from using things like ${\small\fbox{\phantom{Q}group\phantom{Q}}}_1$ for ${\small\fbox{\phantom{Q}associativity\phantom{Q}}}$). The axioms types above are parametrized by $G:\mathsf{Set}$ and the three components $e$, $\square^{-1}$, $\square\cdot\square$, so one can form the type of all groups: $\mathsf{Grp}:\equiv\sum_{\substack{G:Set\\e:1\to G\\\square^{-1}:G\to G\\\square\cdot\square:G\times G \to G}} {\small\fbox{\phantom{Q}group\phantom{Q}}}(G,e,\square^{-1},\square\cdot\square).$ This level of formalism is cumbersome and since [...]

I am planning to do a series of posts where I attempt to do math in Homotopy Type Theory (HoTT). The plan is to do some relatively simple proof-relevant mathematics at an informal level. The topics will all be undergraduate level so the mathematics won’t be hard to follow. I’m hoping to keep the series brief so each post will only be an appetizer and not a full course dinner. Enjoy! This preamble will serve to accumulate a table of contents and various conventions and notations that come up along the way. The only prerequisites (or rather corequisites) are the first two chapters of the (free) Homotopy Type Theory book. Further prerequisites and reverences to later topics in the book will always be indicated where they occur. Elementary group theory More on equational logic Unit group of a ring

After a productive year at the Institute for Advanced Study, the Univalent Foundations Program has written a book on Homotopy Type Theory (HoTT). The foreword gives a succinct description of the purpose of this book: We did not set out to write a book. The present work has its origins in our collective attempts to develop a new style of "informal type theory" that can be read and understood by a human being, as a complement to a formal proof that can be checked by a machine. Univalent foundations is closely tied to the idea of a foundation of mathematics that can be implemented in a computer proof assistant. Although such a formalization is not part of this book, much of the material presented here was actually done first in the fully formalized setting inside a proof assistant, and only later "unformalized" to arrive at the presentation you find before you — a remarkable inversion of the usual state of affairs in formalized mathematics. The danger in writing such a book is to fall into the minefields of logic wars. The authors successfully avoided much of these traps, so logicians from other perspectives can read the book without too much cringing. To avoid unnecessary confusion, I recommend mentally substituting most instances of "set theory" by the more apropos "classical mathematics." Readers from strongly opposing points of view should be prepared for a certain amount of propaganda, which is to be expected in a book [...]

I just made my first contribution to the Selected Papers Network. It was fun and easy and I strongly recommend you use it too! It’s too early for serious commentary on the experience but there are a few things I noted right away: The front page selectedpapers.net does not yet support MathJax. (Neither does Google+ but that’s another problem.) Hopefully that will be fixed soon. Meanwhile, you can use the MathJax bookmarklet. The hashtag syntax is fairly simple and intuitive but there is room for improvement. The main improvement would be to relax the ID rules to allow full urls which are easier to cut and paste. For example, http://arxiv.org/abs/1234.6789 for arXiv:1234.6789, http://dx.doi.org/10.1234/0987654321 for doi:10.1234/0987654321. Comments do not seem to generate arXiv trackbacks. (Or they have not yet made it through the arXiv editorial process.) I wish topic (hash)tags were allowed to have natural syntax. I can’t think of a good reason why this has to follow the Twitter standard. Should it be #cstarAlgebras or #CstarAlgebras or #CStarAlgebras… why not C*-algebras? It’s better to allow natural syntax and implement a tag synonym system. You can track these and other issues here.

This is a very difficult question that I find myself pondering every so often. I once heard a story that Jim Baumgartner was asked this question at a major logic meeting where all areas — recursion theory, model theory, proof theory, etc. — were well represented and he responded that it was the only area of logic not represented there. Indeed, the best way to describe infinitary combinatorics is to describe what it isn’t, as in the introductory paragraph of Jim’s review of William’s book on the subject: Combinatorial set theory is frequently distinguished from axiomatic set theory, although the distinction is becoming less and less clear all the time. If there is a difference, it is more one of method than substance. Axiomatic set theory uses the tools of mathematical logic, such as the method of ultrapowers and the theory of forcing and generic sets, while the methods of combinatorial set theory are purely “combinatorial” in nature. In practice, an argument of result is “combinatorial” if it is not overtly model-theoretic, topological, or measure-theoretic.1 I stumbled across the above review while seeking to find a reference for the anecdote about Jim at the meeting. I don’t remember where I got this story from, I may have read it somewhere or I may have heard it from somebody or Jim himself. I didn’t find a reference for the anecdote. However, I did find that Jim wrote some fantastic book reviews. One of the best [...]

In [2], Joel David Hamkins proposed a set of axioms for the set-theoretic multiverse. Several of these axioms reflect the typical world many set theorists live in, namely that generic extensions, inner models and the like are all legitimate universes. Some set theorists prefer the universe perspective where one such universe is singled out as more legitimate than others and other set theorists prefer to think that any universe is as legitimate as any other. Hamkins is of the latter view and, in many ways, his view is even radically opposed to the universe perspective. Indeed, some of Hamkins’s axioms take the form of “mirages” that gradually eliminate the possibility of singling out a preferred universe. These can be formulated as follows.1 Uncountability Mirage Every universe is countable from the perspective of a larger universe. Undefinability Mirage Every universe is constructible from the perspective of a larger universe. Wellfoundedness Mirage Every universe is not wellfounded from the perspective of a larger universe. Finiteness Mirage Every universe has a nonstandard $\omega$ from the perspective of a larger universe. The Undefinability Mirage is a fascinating axiom that I hope to talk about in the near future but it does not directly contradict the universe perspective. The Uncountability Mirage is startling but it isn’t earth-shattering on its own. However, the last two mirages are fundamentally incompatible with the universe perspective. The Finiteness Mirage — which actually implies the Wellfoundedness Mirage — is especially striking since it asserts [...]


Set Theory has a fantastic and legendary history. At the end, it left us with ZFC, which is currently recognized as the foundation of mathematics. This state of affairs is arguably one of the best possible outcomes for the foundational crisis that plagued mathematics in the early 20th century. However, the choice to adopt ZFC was by no means unanimous, dissent has always been present, often with good reason. Whether propelled by inertia or by sheer power, for better or for worse, ZFC is now approaching 100 years of reign as the foundation of mathematics. The most vocal opposition to ZFC has been from Category Theory (and its relatives). Indeed, the basic tenets of ZFC are very foreign to Category Theory and the various hoops that one has to go through to formalize Category Theory in ZFC quickly turn into major annoyances. The same issues arise elsewhere but Category Theory distinguishes itself from other areas by the fact that it regularly runs into genuine foundational issues, so the frictions that other areas feel become irritations for Category Theory. As expected, this irritation has led to a lot of heated debates and frustrations, but the more important outcome for a logician like me is a variety of interesting alternatives to ZFC. Tom Leinster recently wrote a nice account [4] of one of these alternatives, Lawvere’s Elementary Theory of the Category of Sets (ETCS) [2,3]. The paper is intended for a general mathematical audience; the goal [...]