Discussing "An Intuitionistic Theory of Types: Predicative Part"

(Link), although I downloaded a free copy here.

Author: Per Martin-Löf (University of Stockholm)

Reference: Per Martin-Löf, An Intuitionistic Theory of Types: Predicative Part, Editor(s): H.E. Rose, J.C. Shepherdson, Studies in Logic and the Foundations of Mathematics, Elsevier, Volume 80, 1975, Pages 73-118, https://doi.org/10.1016/S0049-237X(08)71945-1.

Why this paper? Cited by Encoding Dependently-Typed Constructions into Simple Type Theory and Normalization and coherence for ∞-type theories

After covering a few advanced and recent papers on type theory recently, this week we look at the first ever fully realised paper on type theory for formalised mathematics (previous work was either incomplete or suffered from errors). It is stated from the very first sentence that the work of this paper is “intended to be a full scale system for formalizing intuitionistic mathematics”. Charmingly, the paper ends with the self-effacing remark “What is doubtful at present is not whether computerization is possible, because we already know that, but rather whether these proof-theoretical computation procedures are at all useful in practice. So far, they do not seem to have found a single significant application”. Almost 50 years on, the vision of this paper has been thoroughly vindicated by the development of sophisticated proof assistants such as Coq and Lean capable of formalising complex mathematics such as proofs of the Four-Colour Theorem and the Odd Order Theorem.

The basic idea is to exploit the Curry-Howard isomorphism, only recently worked out in detail by William Howard (see Howard’s comments on his influence on Martin-Löf here), which identifies propositions with types and (intuitionistic) proofs with programs, to develop a (at this stage, paper-only) programming language for which which proof checking is type checking. Each logical symbol, familiar from any introductory logic course, becomes associated with a type former, as well as program formers which allow programs with that type to be introduced and eliminated (used). Less familiar to logicians, a universe (type of types) is essential to formalise many mathematical arguments, but care must be taken to avoid paradoxes that would crop up if the universe is taken to be a member of itself (very similar paradoxes must be avoided in set theory); this is the predicativity of the title. Crucially (and again, perhaps not so familiar from an introductory logical course) the decidability and other good properties of algorithms related to the type theory – reduction and type checking – is proved, paving the way for type theory to jump off the page and into real implementation.

This paper is quite a readable introduction to this brand new area, as Martin-Löf does not assume familiarity with the underlying idea of performing mathematics inside type theory, as a more recent paper might, but rather must justify his approach. The paper is full of pithy quotes (some original, some adapted from other sources) to motivate the work, such as “A proposition is defined by prescribing how we are allowed to prove it” and, justifying the importance of type checking being decidable, “we recognize a proof when we see one”.

Discussing "Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom"

(Link)

Authors: Cyril Cohen (INRIA Sophia Antipolis - Méditerranée), Thierry Coquand (University of Gothenburg), Simon Huber (University of Gothenburg), and Anders Mörtberg (Institute for Advanced Study)

Reference: Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg, Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015), ed. Tarmo Uustalu, Leibniz International Proceedings in Informatics (LIPIcs), vol. 69 (2018).

Why this paper? Cited by Formalizing CCS and π-Calculus in Guarded Cubical Agda and Normalization and coherence for ∞-type theories

I’ve blogged a few times on homotopy type theory, ranging from the seminal book to various follow-ups (One Two Three). This is one of the most important follow-ups because of what it does to the univalence axiom, the cornerstone of homotopy type theory that asserts that equivalences between types correspond to identities between them. Cubical type theory is an instance of homotopy type theory for which the univalence axiom is not an axiom at all, but rather a provable theorem (inhabited type). The significance of this may not be immediately obvious to newcomers to type theory – who cares if a statement is an axiom or a consequence of some other rules? In fact with the type theories that lend themselves to applications such as interactive theorem proving we do not typically proceed by asserting axioms – unless we need to – but rather by defining rules for introducing and eliminating our basic type formers. Arranging things in this way allow us to have good computational properties, for example a constructive argument involving a natural number really will produce an appropriate natural number when run. This gives proofs in the type theory computational content, whereas the bald assertion of an axiom would provide a ‘roadblock’ in the execution of a proof.

This development proceeds by developing a type theory which has denotational semantics in the category of cubical sets. In this blog post I won’t sweat the details of these semantics – many of my comments last week about semantics in simplicial sets still apply  – although it is important to understand that working via the semantics motivates every part of this paper. However, I wish to concentrate on the details of the type theory itself as syntax.

It is fair to say that cubical type theory is a heavy duty extension to standard type theory. Some of the earlier parts of the paper are quite beautiful, however. The notion of identity as path is captured by thinking of them as (roughly) a function from a slightly abstracted version of the real interval [0,1] to a type; if we wish to express that t is equal u then we need that function to map 0 to t and 1 to u, and we’re done. This gives a startlingly simple proof of function extensionality (functions are equal if they agree on all inputs), which is a tricky property, and indeed sometimes not even true, in many type theories. Things get more involved, but still rather elegant, if we want dependence on multiple different arbitrary elements of the interval, usually called dimensions. This is where the cubes of cubical type theory come in, as zero dimensions give rise to a point in a space (which is to say, just a usual inhabitant of a type), and one dimension to a path in a space, but we can have squares, cubes, 4-dimensional hypercubes and so on as well.

The next feature is to define faces, which can be thought of as corresponding to faces of cubes (of various dimension), or more prosaically as restrictions on the values that our otherwise arbitrary interval elements can take. For example, we might require that both i and j are equal to one of 0 or 1, describing the outline of a square but leaving its centre unfilled. Terms and types defined with faces in their context are then only partial, e.g. only existing where the free dimensions i and j have appropriate values. Systems are terms of arbitrary type that explicitly define different constructions for different faces. Faces are also used to introduce the notion of extensibility;  a partial term t with respect to face φ is extensible if there is a term u that is not restricted to φ, for which if φ is added to its context, it is indeed equal to t. A new composition operator then comes into play that ensures that extensibility is preserved along paths. This may seem heavy, but is necessary to prove the rather mundane fact that identity is transitive. The equality judgements (intuitively, reduction rules) associated with the composition operator are fairly complex, depending on the type the composition is applied at and so needing explicit definition corresponding to each type former.

The final layer of novelty involves a new type former called glueing which connects types with partial types, and ensures that extensibility is invariant across equivalence. This is the final necessary ingredient for univalence (which is a statement about equivalences, after all) to be proved.

Discussing "The Simplicial Model of Univalent Foundations (after Voevodsky)"

(Link)

Authors: Krzysztof Kapulkin (University of Pittsburgh) and Peter LeFanu Lumsdaine (Institute for Advanced Study)

Reference: Krzysztof Kapulkin, Peter LeFanu Lumsdaine, The simplicial model of Univalent Foundations (after Voevodsky). J. Eur. Math. Soc. 23 (2021), no. 6, pp. 2071–2126. DOI 10.4171/JEMS/1050

Why this paper? Cited by Normalization and coherence for ∞-type theories, The Formal Theory of Monads, Univalently, and On the ∞-topos semantics of homotopy type theory

This paper has a rather peculiar publication history, as it started as a 2012 preprint written by the two authors along with a third, Fields medal winning mathematician Vladimir Voevodsky, who was in fact the main author. However Voevodsky grew disenchanted with the paper due to some issues with the type theory literature it was relying on, and asked for his name to be removed. Sadly, Voevodsky passed away before rectifying these holes in the literature, and so Kapulkin and Lumsdaine worked the paper into a publication. Lacking permission to re-add Voevodsky’s name to the author list, his contribution is instead recognised in the title.

One benefit of this paper having almost a decade to germinate is that it has a particularly pleasant and well written introduction to its topic, Homotopy Type Theory (HoTT). I looked at the seminal HoTT book on this blog last year; this paper picks up one of the topics that the book does not address, although it is briefly mentioned, namely denotational semantics. To recap, HoTT is an approach to mathematical foundations that aims to be both usable by humans and amenable to computer formalisation. The technical approach is to extend previous approaches to type theory with, in particular, a property called the univalence axiom (the other major innovation, higher inductive types, are not discussed here).  Univalence strengthens the usual notion of equality in type theory to, at the type level, correspond to equivalence; this means that one can move constructions and results between equivalent mathematical settings, a common feature of mathematical argument, ‘for free’. This leads one to think of types as (some sort of topological) space, with equality as paths in a space à la homotopy theory.

This paper makes this connection formal by giving homotopy type theory denotational semantics in the category of simplicial sets. Denotational semantics give a mathematical meaning for the constructions of a type theory, programming language, or logic. So long as the mathematical model chosen is not pathological, this gives us as immediate benefit a proof of consistency (one cannot prove false, or construct an element of a type that should be empty). Just as importantly, this style of semantics assures us that all syntactic constructions are not mere shuffling of symbols, but have real mathematical meaning that can be communicated to someone who is not necessarily interested in the details of the particular type theory. Put another way, the type theory is ‘about something’ other than itself.

Why is the ‘something’ that HoTT is about in this paper – i.e. simplicial sets – actually interesting, beyond mere proof of consistency? This paper does not offer an introduction to this mathematics, but looking at one of the books cited as background (link to pdf) gives some clues: “the category of simplicial sets has a homotopical structure … the resulting homotopy theory is equivalent in a strong sense to the ordinary homotopy theory of topological spaces… Insofar as simplicial sets are algebraically defined, and the corresponding closed model structure is combinatorial in nature, we obtain an algebraic, combinatorial model for standard homotopy theory”. In other words, simplicial sets are not a mere mathematical curiosity than happens to work for this type theory, but rather a strongly motivated approach to the general study of homotopy which, of course, is what motivated homotopy type theory in the first place. It should be noted that simplicial sets are not unique in having this property; there is a somewhat similar structure called cubical sets that appear to be more suited to computational implementation. But that, perhaps, is a story for another day.