(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.

Thanks for this nice and comprehensive explanation! I wonder, though, is it really appropriate to call “constructive validity” a “system of logic”? It makes more sense to me to think of it as a particular class of

semantics, or perhaps better, atranslationof logic into dependent type theory (whicha priorilacks a logic). In the Aczel-Gambino language, it would be a “canonical enrichment” of type theory with a logic, although of course the same type theory could admit many other enrichments.It so happens that, for instance, under this translation, the axiom of choice is always valid. I don’t think of the axiom of choice as a property of

logic, but rather as an axiom that may or may not be asserted, or which may or may not hold in a particular semantics or under a particular translation. Likewise, the fact that AC implies excluded middle is not a law oflogic, but rather a theorem under certain hypotheses, among which are power types/sets.whether constructive type theory is “logic”, and whether AC is a “law of logic” is certainly a matter of debate, and there are plenty of people on both sides of the issue. I don’t think it matters much — it’s a question of how we choose to use the term “logic”. What does matter is how we interpret the mathematical statements that we are trying to prove: as proof relevant types, or proof irrelevant “propositions”. Vladimir has set a good example by keeping track of the difference between the two, and asserting as naked propositions only those types that provably are propositions, i.e. of h-level 1 (resp. -1, depending on your numbering scheme). This seems to me like the best way to go.

Based on what you’ve been writing, Mike, it seems that HTT sometimes *does* have power types (and even more often has quotient types, which are all that you need to get EM from AC). But if HTT had EM, I think that you would have mentioned this. What’s missing here?

HoTT does sometimes have power types and quotient types. But it doesn’t (always) have AC, precisely because we interpret only the (-1)-types as propositions. The type which represents AC under the propositions-as-(all-)types translation is still provably inhabited, but that type does not represent AC when we allow only (-1)-types as propositions; to get the appropriate version of AC for HoTT we have to insert some s.

There’s nothing special about HoTT here — the same is true for the extensional dependent type theory of a lccc pretopos or a topos. The type which represents AC under propositions-as-types is always inhabited, but it doesn’t represent AC under the “internal” interpretation of logic as subobjects.

By the way, it’s evident, comparing this post to mine, that our motivations and views of “the goal” of homotopy type theory are quite different! I’m glad to have them both on the table; I didn’t realize that your point of view was so different.

I tend to feel that Voevodsky’s view is closer to mine; although he hasn’t

yetused much in his Coq development, he has at least talked about defining it (subject to a resizing axiom), and he seems inclined only to interpret as “propositions” the types that are of h-level one. So perhaps it’s misleading to say that your goal of interpreting constructive validity homotopically is “the” leading idea of homotopy type theory.I haven’t really said what my own views are — I’m just trying to lay out the basic issues here.

Actually, my view is that it would be good to include the [bracket] types construction, modelled by , in order to have a “hybrid” system that incorporates both constructive validity and more customary predicate logic — within a systematic calculus relating the two, as we did for the extensional theory. Then we can read

as, say, “there Exists an x in A such that for All y in A, x is Identical to y”,

and we can read

as “there exists an x in A such that for all y in A, there’s a path from x to y”.

That is, there are two different ways of reading these operations — constructively and non-constructively, for lack of better terms — and we don’t have good plain English renderings that do both of them justice. The logical calculus is more precise than plain English in distinguishing them — and they are moreover related to each other in a precise way that we want to formalize.

But I’m being cautious at this point, since no one has (yet) proved the soundness of such a calculus for the intensional case, with respect to the homotopy interpretation. It’s not enough to just look at simplicial sets and set Prop = 2; the general case of, say, simplicial sheaves may turn out to be more subtle — so I’m reserving judgement until I see how it works. Probably you’re ahead of me in recognizing that everything will work out fine (I hope so).

That’s great. But what I meant was different is the fact that you want to read as “there Exists an x in A such that for All y in A, x is Identical to y”. I don’t want to read it that way; I want to read it as “the type of points x in A equipped with a continuous assignation of paths from all points of A to x.”

I understand that’s what you are urging — and you certainly can do it. That’s indeed how we’ve been reading e.g. the internal topos logic. Nothing forces you to read the and as “constructive quantifiers” (which I meant by “Exists” and “for All”), rather than type-forming operations, or as Identity rather than the space of paths.

BUT: the cool thing is that one *can* do so, and it captures an *existing* notion of constructive logic — one that has been advanced by some thoughtful logicians for very good reasons — right down to the somewhat strange behavior of the intensional identity types. If you’re not interested in that reading, you can just skip that part and read ahead. ;-) Some people do care about it, for various reasons, and they are happy to know how it relates to homotopy theory.

I certainly don’t have anything against other people reading it that way! (Even if I personally don’t quite understand yet why they want to.) I think one of the most exciting things about this subject is that it brings together such different-looking communities. I was just pointing out that the difference is, in fact, a difference. (-:

So here’s a question, which may contribute to my better understanding of this side of the project. I think I can see why the existence of homotopy semantics is interesting may be interesting to someone who cares only about intensional type theory for its own sake. For one thing, it shows the potential “nontriviality of intensionality” — i.e. there are naturally occurring non-extensional models. But is the direction of Voevodsky’s work also interesting to such a person? If so, how and why?

I am not sure if this is an answer to your question, but from the point of view

of type theory (and formalization of mathematics), an important consequence

of the univalence axiom is that it should imply that isomorphic mathematical structures are isomorphic.

This is formally checked for a simple structure (a type with a binary

operation) at the end of this file. It expresses that if two such structures are isomorphic

they are equal, and so at least in the case where the two underlying types are of

h-level 2, it represents the equality of isomorphic mathematical structures.

Thanks, that’s helpful! However, I was thinking more of Voevodsky’s aim of developing homotopy theory in type theory. What you say sounds like a good reason why a type theorist might be interested in the univalence axiom, which is something more than what I said in my first question (since the univalence axiom requires, but is not required by, a homotopy semantics). But how about the definition of exact fiber sequences, or the commutativity of ? Are those interesting to a pure intensional type theorist?

Here’s a related thought. It seems to me that perhaps what the univalence axiom does for type theorists is allow them to deal, in a familiar type-theoretic framework, with the by-now well-established fact that the “right” notion of “sameness” for sets (and sets with structure) is not equality, but isomorphism. In order to do this, we are forced to admit that the first universe is at least of h-level 3 (and any universe it belongs to is at least of h-level 4, and so on). But once our theory admits objects of h-level >2, we can’t use plain set-theoretic ideas any more, just like how when we do category theory, 2-category theory, and homotopy theory in classical mathematics we are forced to deal honestly with the nontrivial isomorphisms and homotopies that our objects can contain. In particular, concepts like fiber sequences and the commutativity of , although perhaps not yet recognized in type theory as important, will inevitably become so (just as they did in classical category theory and homotopy theory), as type theorists become accustomed to dealing with types of higher h-level in a “natural” way. Does that seem fair?

I’d like to make a terminological quibble. I regard MLTT as the current embodiment of intuitionistic mathematics, as I think do many others. It’s jarring for me to say that the denial of excluded middle and the affirmation of choice are jointly inconsistent with

intuitionisticmathematics, since this is exactly the combination that MLTT offers. I think you’re contrasting MLTT with IZF and related systems, which do not, at least in my view, accurately model intuitionistic principles, titular claims notwithstanding. I would put IZF into the category of constructive mathematics in the general sense, with MLTT being specifically the intuitionistic interpretation (it does not, for example, validate Markov’s Principle, which some would say is constructive).Fair enough!

I meant by “intuitionistic logic” something like the (possibly higher-order) intuitionistic predicate logic that’s modeled in toposes and in systems like Heyting Arithmetic. I wanted to contrast this with what I called “constructive logic”. But we can also use the term “intuisionistic logic” in the way you suggest — essentially as what I called “constructive logic”. Then one should perhaps call the other system something like “impredicative intuitionistic logic”?

Gee, I had no idea the terminology had gotten so mixed up. The set-theorists, of course, use the word “intuitionistic” for impredicative systems like IZF and reserve “constructive” for systems like CZF which are more closely related to MLTT. I wish we could at least agree on

namesfor all these systems, andthenthe people who feel like it could go off in a corner and argue about philosophy.That said, it sounds like part of your point is similar to what I said in the first comment, namely that intuitionism and AC only become inconsistent when you also add powersets into the mix, and the latter should not be implied by the word “intutionistic”?

I see the problem; perhaps I’m too doctrinaire in adhering to Martin-Loef’s predicative principles. It’s true that in MLTT there is no type Prop of all propositions, which would be the sub-object classifier. Calculus of Constructions has this, but it seems to play a smaller and smaller role these days, particularly in our current explorations of homotopy theory where the identification of propositions with types plays a central role (well-illustrated in Bauer’s recent formalization work). I wish I knew what to suggest! Steve’s proposal is a mouthful, and not standard terminology afaik.