15
$\begingroup$

The HoTT community is quite friendly, and produces many motivational introductions to HoTT. The blog and the HoTT book are quite helpful. However, I want to get my hands directly onto that, and am looking for a formal treatment of HoTT. Therefore this question: what's the formal definitions of the gadgets in homotopy type theory (HoTT)?

I expect an answer with absolutely no motivations and no explanations. It should define all terminologies, such as type, term, :, for all, exist, identity, equivalence.. etc. It should also clarify which words are undefined. I feel like I'm almost asking for a computer program.. so if that's your answer, I'm happy to study it.

Improve this question
$\endgroup$
2
  • 3
    $\begingroup$ There is a formal definition of homotopy type theory in the HoTT book, Appendix A. $\endgroup$
    – L. Garde
    Oct 11, 2020 at 20:54
  • $\begingroup$ A word of warning. Unless you are already familiar with the type theory formalism, it is going to be quite hard to get the point of homotopy type theory, as it deviates significantly from traditional foundations that are taught at universities. $\endgroup$
    – Andrej Bauer
    Oct 11, 2020 at 21:00

2 Answers 2

Reset to default
25
$\begingroup$

Here are some resources:

  1. The appendix of the homotopy type theory book gives two formal presentations of homotopy type theory.
  2. Martín Escardó wrote lecture notes Introduction to Univalent Foundations of Mathematics with Agda which are at the same time written as traditional mathematics and formalized in Agda (so as formal as it gets).
  3. Designed for teaching purposes is Egbert Rijke's formalization HoTT-intro which accompanies his upcoming textbook on homotopy type theory.
  4. The HoTT library is a formalization of homotopy type theory in Coq. Start reading in the order of files imported in HoTT.v.
  5. The HoTT-Agda library is quite similar to the HoTT library, except formalized in Agda.
  6. The UniMath library is another formalization of univalent mathematics in Coq.
Improve this answer
$\endgroup$
19
$\begingroup$

Andrej’s answer gives an excellent list of resources. But I think it’s also worth saying a little upfront to ward off common misunderstandings. HoTT is a foundational system — analogous to ZFC set theory — and the way in which the basic vocabulary of foundational systems is “defined” is a bit different from how most mathematical objects are defined. And for newcomers to type theory, especially experienced mathematicians, this is a frequent source of misaligned expectations.

Whenever you’re setting up some logical formal system, you are typically “defining” things in several different senses:

  1. you’re defining the formal system itself — its syntax, its rules of inference, its axioms…

  2. you’re introducing terminology to talk about the basic notions of the formal system

  3. as you work within the formal system, you’re then defining further objects within it.

With ZFC, for instance:

  1. This is the sense in which you define what “first-order logic” and “ZFC” formally are, for studying them from the outside as a logician.

  2. This is the sense in which you define set, implies, for all, and so on. You don’t define “a set is a such-and-such satisfying the so-condition”. We just introduce set as a word for the primitive objects that the ZFC axioms axiomatise. Similarly, implies is just a certain primitive symbol of our language, and first-order logic gives us rules for reasoning with it.

  3. This is the sense in which you define power sets, the rank of sets, and generally, definitions made while doing mathematics within ZFC.

So (1) and (3) are definitions in the usual mathematical sense, but happening at two different levels — external to the formal system under consideration, or internal to it. Meanwhile, (2) is a bit more different: you are “defining” things by taking them as primitive notions and axiomatising them.

I say all this because most of the things you mention in your question are “defined” in HoTT in sense (2) — so you will not find definitions of them in the sense you may expect! They are “defined” in the same way that sets are defined by ZFC. Following through the senses above, for HoTT:

  1. This is the sense in which you define what “HoTT” is, as a formal system from the outside. (HoTT and other type theories don’t have the same kind of separation between the “logical language” and the “theory in it” that you have with e.g. FOL+ZFC.)

  2. This is the sense in which you define type, term, for all, and so on: They’re the words we use for the various primitive objects and symbols of the formal system; and the formal system gives us rules for reasoning with them.

  3. This is the sense in which you define contractible, eqivalence, univalent, and so on, when developing mathematics within type theory.

Improve this answer
$\endgroup$
7
  • 1
    $\begingroup$ I like to use the word "axiomatized" to mean what you refer to as "defined in sense (2)". $\endgroup$
    – Lee Mosher
    Oct 12, 2020 at 15:58
  • 1
    $\begingroup$ @LeeMosher: that's the standard terminology, which works well if we're describing a mathematical theoryinside a chosen foundation (for instance, when we describe topological spaces inside set theory and first-order logic). But when setting up the foundation itself, we are likely introducing new concepts that are not "axioms", e.g., judgement forms or inference rules. But I don't have any suggestions about what word to use instead. $\endgroup$
    – Andrej Bauer
    Oct 12, 2020 at 16:04
  • $\begingroup$ @LeeMosher: Yes — “axiomatisation” is a standard and unambiguous way of describing it (modulo subtleties about axioms vs. rules). But there’s a significant overlap between axiomatisation and definition, in several senses, both technical and philosophical, which I wanted to point out here. On the one hand, the idea of a definition is very often formalised (e.g. in first-order logic) as simply meaning the introduction of a fresh symbol together with an axiom characterising it uniquely — so a definition (in that strict sense) is just a particularly specific kind of axiomatisation. (cont’d) $\endgroup$
    – Peter LeFanu Lumsdaine
    Oct 12, 2020 at 17:07
  • $\begingroup$ (cont’d) On the other hand, axiomatisations fulfil the same function as definitions, of introducing new concepts and telling us how to use them — as illustrated by questions like the OP’s here, which ask “how is X defined?”, and where the answer is “by being axiomatised”. $\endgroup$
    – Peter LeFanu Lumsdaine
    Oct 12, 2020 at 17:11
  • $\begingroup$ It seems like these roughly correspond to (1) “semantics” or interpretation, (2) primitive notions (function and relation symbols) and inference rules (including rules with no premises, i.e. axioms), and (3) definitions (conservative extensions). $\endgroup$
    – user76284
    Oct 12, 2020 at 18:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.