This is a follow-up to my recent post on the structure of universes in HoTT. In this post I will outline one of the possible alternative ways of handling universes in HoTT, which I will colorfully call Super HoTT for the time being. This is not an original idea; something like that (not in the context of HoTT) can be found in Erik Palmgren’s paper On Universes in Type Theory.1 The idea comes from a comment by Andrej Bauer where he described a universe as "a structure $(\mathcal{U},\tau,\pi,\sigma,\ldots)$ where $\mathcal{U}$ is a type, $\tau$ is a type family indexed by $\mathcal{U},$ $\pi$ and $\sigma$ compute codes of dependent products and dependent sums, etc." This is a perfectly reasonable way of describing universes. By the Foundational Thesis of HoTT, this approach should be formalizable in some flavor of HoTT. This is indeed possible and the flavor (or rather flavor family) Super HoTT is one way to do that. The issue with Bauer’s description is the type family $\tau.$ Formally, a type family indexed by a type $\mathcal{U}$ is an element $\tau:\mathcal{U}\to\mathcal{V},$ where $\mathcal{V}$ is some larger universe. This type $\tau$ becomes a type family only after applying Tarski-style coercion associated to $\mathcal{V}$ that promotes elements of $\mathcal{V}$ to actual types. On the face of it, this is circular: $\tau$ is the Tarski-style coercion associated to the universe $\mathcal{U},$ which is defined in terms of that of $\mathcal{V},$ which… One way to break this circularity is [...]

In this post, I want to outline some subtle and interesting aspects and issues with respect to universes in HoTT. Some of these issues were brought up in a comment discussion with Mike Shulman some time ago and they came up again more recently in a comment discussion with Andrej Bauer and Alexander Kuklev. I will use the HoTT book as a reference though this post is not intended as a criticism of the handling of universes in the book. Indeed, to serve its purpose, the book is deliberately vague about the exact handling of universes in HoTT. In fact, this post is a good illustration why this is necessary! Also note that the issues I bring up are mostly irrelevant to conducting everyday mathematics in HoTT. While this post is largely for people interested in technical aspects of HoTT, I will nevertheless try to keep the the post at a medium level of technicality since these aspects of HoTT do come occasionally up in everyday mathematics. In section 1.3, the HoTT book introduces universes as follows: [W]e introduce a hierarchy of universes $\mathcal{U}_0 : \mathcal{U}_1 : \mathcal{U}_2 : \cdots$ where every universe $\mathcal{U}_i$ is an element of the next universe $\mathcal{U}_{i+1}$. Moreover, we assume that our universes are cumulative, that is that all the elements of the $i$th universe are also elements of the $(i+1)$st universe, i.e. if $A : \mathcal{U}_i$ then also $A : U_{i+1}.$ In the comment discussion mentioned in the [...]

It’s been a while since the last edition of HoTT Math. Fall is always very busy for me and I’ve been composing this installment one $\varepsilon$ at a time… We are finally arriving at our destination: fields! The main issue with fields is to correctly handle the implicit negation in the term nonzero. Since the natural logic of HoTT is intuitionistic rather than classical, this is much more subtle than one would expect. One issue with the basic commutative ring theory we developed last time is that there is a one-element ring. This is a feature of every equational theory since all identities are satisfied in the trivial algebra with one element. The problem is that equational logic doesn’t have negation so there is no way to state a nontriviality axiom like $\mathsf{O}\not\approx\mathsf{I}$ in this context. These issues are not new and not special to HoTT but the problem is amplified since logic in HoTT is may have more truth values than just true and false. Consequently, negation in HoTT always needs a little more care. The usual way to say $\mathsf{O}\not\approx\mathsf{I}$ is the strongest one, namely that $\mathsf{O}=_R \mathsf{I}$ is the empty type $\mathbf{0},$ or: ${\small\fbox{\phantom{b}nontrivial\phantom{q}}} :\equiv(\mathsf{O}=_R \mathsf{I}) \to \mathbf{0}.$ This is stronger than just saying that $\mathsf{O}=_R \mathsf{I}$ isn’t inhabited and it may exclude more than just the one element ring in the absence of the law of excluded middle [§3.4]. In general, we define inequality by $(x \neq_R y) :\equiv(x =_R [...] 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 Local rings and fields

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 [...]