Constructive Validity

(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 \Pi , \Sigma , equality \mathsf{Id} , conjunction \times , disjunction + , implication \rightarrow and negation \neg .  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 A\times B is a pair of proofs, one for each conjunct A and B, and so on.  In the end, a proposition-type A is true iff one has constructed a proof-term a : A.  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 \lambda-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 \Pi, \Sigma, \mathsf{Id}, \times, + , \rightarrow, \neg  as “type-theoretic” and the corresponding “predicate logical” ones \forall, \exists, =, \wedge, \vee, \Rightarrow, \neg 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 \exists x:A. P(x) one does not always have a way to find a term a:A and a proof of P(a)).  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 \pi_{-1} 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 \Sigma and \exists, 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.

Posted in Foundations | 17 Comments

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

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

Posted in Foundations | Leave a comment

Function Extensionality from Univalence

Andrej Bauer and Peter Lumsdaine have worked out a proof of Function Extensionality from Univalence that is somewhat different from Vladimir Voevodsky’s original.  In it, they identify and employ a very useful consequence of Univalence: induction along weak-equivalences.  Andrej has written it up using CoqDoc, which produces a very readable pdf available from his GitHub repository or directly here.  Peter has a neatly organized Coq treatment in his repository here.

Here is the Introduction from Andrej’s CoqDoc:

This is a self-contained presentation of the proof that the Univalence Axiom implies Functional Extensionality. It was developed by Peter LeFanu Lumsdaine and Andrej Bauer, following a suggestion by Steve Awodey. Peter has his own Coq file with essentially the same proof.

Our proof contains a number of ideas from Voevodsky’s proof. Perhaps the most important difference is our use of the induction principle for weak equivalences, see weq induction below. We outline the proof in human language at the end of the file, just before the proof of extensionality.

This file is an adaptation of a small part of Vladimir Voevodsky’s Coq files on homotopy theory and univalent foundations, see https://github.com/vladimirias/Foundations/.

The main difference with Voevodsky’s file is rather liberal use of standard Coq tricks, such as notation, implicit arguments and tactics. Also, we are lucky enough to avoid universe inconsistencies. Coq is touchy-feely about universes and one unfortunate definition seems to be enough to cause it to encounter a universe inconsistency. In fact, an early version of this file encountered a universe inconsistency in the last line of the main proof. By removing some auxiliary definitions, we managed to make it go away.

This file also contains extensive comments about Coq. This is meant to increase its instructional value.

Posted in Univalence | 6 Comments