Homotopy Type Theory

(This is intended to complement Mike Shulman’s nCat Cafe posting HoTT, II.)

The Propositions-as-Types conception of Martin-Löf type theory leads to a system of logic that is different from both classical and intuitionistic logic with respect to the statements that hold in the fragment of logical language that these three share, namely the quantifiers , , equality , conjunction , disjunction , implication and negation .  For example, it validates the “axiom of choice” but not the “law of excluded middle” — a combination that is impossible classically and intuitionistically.  Let us call this conception “constructive validity” following a paper by Dana Scott in which it was first introduced (Constructive Validity, Symposium on Automated Deduction, LNM 125, Springer (1970), pp. 237-275).

Constructive validity is closely tied to proof theory: as explained by Per Martin-Löf in the monograph Intuitionistic Type Theory (Bibliopolis, 1984), the constructive rules for the logical operations can be justified by associating the terms of a type with the proofs of the corresponding proposition.  To say that a proposition is constructively true or valid means just that it has a proof, and a proof of a conjunction is a pair of proofs, one for each conjunct and , and so on.  In the end, a proposition-type is true iff one has constructed a proof-term .  The rules of construction for types are seen to correspond to the usual rules of inference for propositions in a deductive calculus, and so the entire system represents a sort of “theory of proofs”, rather than the more usual logical “theory of provability”. Keyword: Curry-Howard correspondence.

The system of constructive type theory has two variants: extensional and intensional.  This is a topic for another day, but don’t confuse it with the distinct  issue of function extensionality, which can hold or fail in the intensional type theory, but is usually assumed to hold in the extensional theory.  We can model extensional constructive type theory in a now well-known way in locally cartesian closed categories.  In particular, this theory is deductively complete with respect to both topological models (i.e. sheaves on a space, see S. Awodey, Topological representation of the lambda-calculus. Math. Stru. Comp. Sci. (2000), vol. 10, pp. 81–96.) and Kripke models (i.e. presheaves on a poset, see S. Awodey and F. Rabe, Kripke Semantics for Martin-Löf’s Extensional Type Theory. TLCA 2009: 249-263).  The topological and order-theoretic interpretation of this system is a straighforward extension of the same for the simply typed -calculus, which is the basis of Dana Scott’s domain theory. The basic insight of domain theory is that logically definable maps are always continuous, and logical constructions (with their associated structure maps, like product projections) should not lead outside the category of spaces.  This leads to the development of synthetic domain theory, which like Lawvere’s synthetic differential geometry builds the continuity, respectively smooth structure, in from the start and seeks to axiomatize the logical-categorical structure of such a category of domains, respectively smooth spaces, directly (rather than modelling them as structured sets).

Still talking about the extensional system, we can compare and relate constructive to classical and intuitionistic validity by extending the system in several different ways: logic-enriched type theory of Aczel and Gambino (Collection principles in dependent type theory, in: Vol. 2277 of LNCS, Springer-Verlag, 2002, pp. 1-23.), the [bracket] types of Awodey and Bauer (Journal of Logic and Computation. Volume 14, Issue 4, August 2004, pp. 447-471), a type Prop of proof-irrelevant propositions as in Coq, and others.  In such a hybrid system, one may consider the constructive (proof-relevant) operations   as “type-theoretic” and the corresponding “predicate logical” ones as “logic”.  These new predicate logical operations are “proof irrelevant”, since they produce or apply to formulas which do not preserve all the information about proofs (e.g., from a proof of one does not always have a way to find a term and a proof of ).  Such extended systems are useful both for relating constructive and other kinds of validity, and also for reasoning about their natural models in categories like toposes that have the required structure (an lcc pretopos is more than sufficient).  However, one does not need to include such extended predicate or proof-irrelevant logical operations in a system of constructive logic, which is perfectly sensible without them. (Semantically, the proof-irrelevant operations are modeled in the fibration of subobjects or monos over the category of types, rather than in the entire codomain fibration as in the lccc semantics.)

Now what about the intensional system?  Here the notion of constructive validity is even further from classical and intuitionistic validity, since the proof-relevant identity relation also behaves in a logically unfamiliar way (but one that is familiar from the standpoint of higher-dimensional categories!).  Despite its better proof-theoretic and computational character, even many type-theorists with constructive inclinations have had a hard time learning to live with this system, and prefer instead systems with additional rules that imply not only Function Extensionality, but also Uniquenes of Identity Proofs.  As a system of logic, however, intensional type theory without such additions still represents a perfectly coherent conception — just one that is very different from the intuition of (classical or intuitionistic) sets, classes, relations, functions, etc.

And now the fascinating new fact is that this conception of intensional constructive type theory does have a natural model in the world of homotopy — with the identity relation interpreted as the fibration of paths, and the quantifiers interpreted constructively as before.  This model expands the topological one of extensional type theory by replacing the diagonal relation by the fibration of paths, which aligns better with the constructive point of view, since it’s now a proof-relevant relation.  (From an order-theoretic point of view, we pass from posets to (higher-dimensional) categories, and use the (higher) groupoid of isos in place of the diagonal relation.)

This is the leading idea of Homotopy Type Theory: we still regard the operations of quantification, identity, etc. as constructively logical — and we can use the system of type theory to reason formally as before — but the interpretation is now intrinsically homotopical: the types are spaces (or homotopy types), the terms are continuous mappings, identity between terms (as expressible in the system) is homotopy, isomorphism of types is homotopy equivalence, etc.  Combining this with the constructive interpretation of the other logical operations (quantification, implication, conjunction, etc.) still makes good sense, given the topological interpretation that we already had of constructive validity — in fact, it makes even better sense than before, since now identity is handled constructively, too (as opposed to extensionally), and is modelled topologically.  The approach might also be called synthetic homotopy theory, since it has the same methodology of taking homotopy, continuity, etc., as built-in, rather than modelled in structured sets.

Finally, what happens if — as in the extensional case — we try to add a [bracket]-type constructor, or logic-enriched type theory, or a proof-irrelevant type Prop into the mix?  There does seem to be a natural “proof irrelevant logic” in the homotopical model, say in simplicial sets.  One can identify some types as “propositions” — i.e. types of H-level 1, using Voevodsky’s IsProp construction — and one can imagine using as a logical operation like the [bracket]  to “squash all the proofs together”.  In that case, one would again have a “hybrid” system in which there are both and , etc. — both “type-theoretic” and “logical” operations, as we termed them above.  This is much like (a part of) the Calculus of Constructions implemented in the current Coq system — but it is not (yet) used in homotopy type theory, nor is it used in Voevodky’s Coq development of Univalent Foundations.  That’s not to say that HoTT couldn’t profitably be extended in this way — very likely it could.  But one would first need to pick an extended type theory and then carefully investigate the homotopical interpretation of that extended system, and this has yet to be done.  Even then, however, the original constructive interpretation remains a perfectly coherent conception of constructive validity; we don’t want to be forced to always read the identity relation as a space of paths, and the quantifiers as disjoint sums and dependent products — those are constructions on structured sets rather than primitive logical operations of identity and quantification.  We want a system of logic representing constructive validity, employing the propositions-as-types paradigm — perhaps extended by some further device for erasing proof-relevance — interpreted homotopically in a way that also makes geometric sense.  Understanding both the logical and homotopical sides, and their interaction, is what this project is about.

Mike Shulman has another great posting on HoTT over at the n-Cat Cafe’. It starts out like this:

Homotopy Type Theory, II — Posted by Mike Shulman

… Last time we talked about the correspondence between the syntax of intensional type theory, and in particular of identity types, and the semantics of homotopy theory, and in particular that of a nicely-behaved weak factorization system. This time we’re going to start developing mathematics in homotopy type theory, mostly following Vladimir Voevodsky’s recent work.

via Homotopy Type Theory, II | The n-Category Café.