.. todo:: should there be a separate cubical page?
.. todo:: explain this dogma
To say that something is a constructor of a type A means that the type A was defined inductively, and that you are picking one of the options specifying its datatype. For example, \mathbf{N} has exactly two constructors: 0 and S. But since, for example, S has type \mathbf{N}\to\mathbf{N}, constructors of a type are not always elements of that type.
To say that something is an element of a type A means that it is a variable or expression whose type is A. But that means that, in some non-trivial :term:`context`, you can have an element of type \mathbf{0}: for example in the context x:\mathbf{0}, we have the element x of type \mathbf{0}.
Confusingly, even in the context x:\mathbf{0}, where we have the element x of type \mathbf{0}, we can show that \mathbf{0} does not have any elements, because the claim "A does not have any elements" is formalised as \neg A, that is, A\to\mathbf{0}, and \mathbf{0}\to\mathbf{0} is indeed inhabited (by the identity function).
Point and proof are synonyms for element.
However, when we claim that some theorem is or is not provable, then this is a meta-theoretic claim. For example, we may say that, in pure HoTT, the principle of excluded middle (which, being a logical claim, is itself encoded as some type, namely PEM=\prod_{P:\mathsf{Prop}}P+\neg P) is not provable: indeed, homotopy type theory is consistent with excluded middle, but also with its negation. However, we can't say that the type PEM has no elements, for this would be interpreted by the statement that the type PEM is empty, that is, that excluded middle is false! And in pure HoTT we can't prove that PEM is false, again, because we want to be consistent both with excluded middle and its negation.
Finally, term is a strictly syntactic notion. As a first approximation, something is a term if it is a string of characters that, when inserted in a proof assistant, would parse, and have a certain type. There are no terms of type \mathbf{0} (unless HoTT turns out to be inconsistent).
There seems to be some miscommunication regarding which statements by HoTTist are internal and which ones are metatheoretical. It may also sometimes be unclear what formal language to use to formalize informal statements. I'm not sure exactly where the confusion starts, but here are some aspects to consider.
Already in classical mathematics, some claims shouldn't be translated word-for-word into formal language. For example, the claim "we can prove theorem X" doesn't presume an internal formalisation of the notion of theorem, provability, an understanding of what "we" means, or any kind of modal logic to model the "can".
In the context of HoTT, many claims are understood to be descriptions of types. For example, "there exists a number with f(n)=0" should be interpreted by the type \exists(n:\mathbf{N}).f(n)=0. Then the understanding that this claim is true corresponds to the understanding that somebody has produced a term of that type.
However, this explanation of how to translate natural language into type theory is incomplete.
- It may not be clear what the right type-theoretical definitions are that correspond to classical mathematics. This is more apparent for type theory, as the things we used to think of as well-understood in set theory become ambiguous in a type theory where higher-dimensional structure and lack of choice axioms prevents us from unifying this or that. However, fundamentally this is not a new problem, as the question "what is the right definition for this?" is also very common in classical mathematics. At the end of the day, the correctness criterion for mathematical definitions is primarily based on the agreement of scientists. Definitions from classical mathematics don't translate one-to-one into type theory, and we don't want them to.
- Sometimes we want to talk about the semantics of a chosen type theory, irrespective of the specific foundations that those semantics are built up in. Even more confusingly, some claims are true both as internal statements, that is, when translated into type theory, and as statements about the semantics. So certain pieces of text may be understood to be formalisable entirely in a system that is not a type theory (such as papers on semantics), and others might support a fairly systematic translation of natural language to types and their elements.
.. todo:: set cover axiom. :math:`(A:Type)\to \|(B:Set)\times(f:B\to A surjection)\|` sets cover page on nlab: https://ncatlab.org/nlab/show/n-types+cover similar to in toposes: you can prove there exists something, but there might not be a global element
There are (at least) two different notions of "space" and (at least) two different "circles".
First of all, every type is thought of [1] as a space: and so the HIT S^1 freely generated by a basepoint and a path on that basepoint is thought of as a homotopical circle. The space-like behavior is given by the type theory, and can be probed using identity types.
Secondly, there is a certain subset of the real plane \mathbf{R}^2 (taking \mathbf{R} to be, for example, the dedekind reals) that represents a circle, namely the subtype of points with radius 1. The space-like behavior of such spaces internal to the theory is given by whatever notion of space we are interested in: for example, \mathbf{R}^2 is often studied as a metric space with a metric d:\mathbf{R}^2\times\mathbf{R}^2\to\mathbf{R}.
These two circles are completely unrelated, unless you add extra syntax or axioms, such as in real-cohesive HoTT :cite:`shulman:real:cohesive`.
This can be terribly confusing. For example, the fact that every map in HoTT lifts to a map on the identity types (expressing that if two inputs to a function are equal, then we can prove the outputs are equal) is explained in the HoTT book by saying that this means the function is continuous. So from the HoTT point of view, all functions are "continuous" in that sense. But in the context of constructive analysis inside HoTT, it is not provable that all functions are continuous, and in fact it need not be true, for example if one has the principle of excluded middle.
Even though the link between types and, say, topological spaces (as defined inside HoTT) is broken, the intuition of the internal theory of those spaces is still used to prove the impossibility of type-theoretical proofs. For example, it is not provable that any two points on the higher-inductive circle are equal, which is somewhat odd since in any drawing of a circle there are at least two obvious paths between any two points x and y. As a topological counter-argument, it is said that the path from x to y cannot be chosen in a "continuous" way, in the sense that if you rotate x along the circle one full rotation, you'll have to make a "jump" in your choice of path at some point. But this counter-argument is topological in nature, rather than type-theoretic (although there is a way to make it precise type-theoretically).
Indeed, proofs about types such as the higher-inductive circle look nothing like their counterparts in topology. Still, they satisfy some of the same properties: if we define the "homotopy group" of a pointed type correctly, then the higher-inductive circles seem to have the same homotopy groups as their topological counterparts in classical mathematics (in the sense that this has been shown for a handful of cases) [2]. However, some properties are fundamentally different in a seemingly unfixable way: as a theorem stated inside type theory, there do not exist any embeddings S^1\to S^3 - so higher-inductive types can't be naively used to formalise knot theory. (One further problem with such an approach is that HoTT only allows phrasing things that are invariant under homotopy, which things like "non-self-intersecting" are not.)
footnotes
| [1] | In fact, not only do we think of a type as a space, but if we take geometric semantics of univalent type theory, such as model categories, every type is interpreted by an actual space. |
| [2] | By Shulman and Lumsdaine :cite:`lumsdaine:shulman:hits`, we can construct all spheres from pushouts in any "sufficiently nice" Quillen model category. So everything we can hope to prove about the homotopy groups of spheres must be equal to the classical result. In other words, HoTT and classical mathematics cannot disagree about the homotopy groups of spheres. |
There are (at least) three notions of sets:
The objects studied by a theory such as ZFC. We can take intersections of any two such sets, even if this does not make sense from an extensional point of view: for example, we can take the intersection of \pi with the graph of x\mapsto x^2, as both objects are sets. ZFC is a material set theory, since elements may be a member of several different sets.
0-types, which behave simlar to ZFC sets in some aspects. For example, for a map f between two 0-types (but not between arbitrary types), the following are equivalent:
- f is an injection (equal outputs implies equal inputs).
- f is an embedding (equal inputs is equivalent to equal outputs).
- f is a monomorphism (with respect to all maps on all types).
The set theory of 0-types is structural, since every element is canonically a member of a fixed type.
A cumulative hierarchy of sets as in e.g. chapter 10.5 of the HoTT book, as an attempt to find a model of an axiomatic set theory like ZFC (although this will likely require choice).
In the context of HoTT, by "set" we mean 0-types, unless otherwise specified.
HoTT is not a internal language for topology. By adding modalities to HoTT, we can talk about types as topological spaces :cite:`shulman:real:cohesive`.
Within the HoTT community, "homotopy theory" refers to abstract homotopy theory in the sense of, for example, Quillen model categories, or more generally homotopy categories. The category of topological spaces and continuous maps is one such model category. However, HoTT is not an internal language for all model categories. In particular, the "homotopy" of HoTT does not (necessarily) refer to the homotopies of point-set topology.
MLTT comes with identity types \mathsf{Id}_X:X\to X\to\mathcal{U}. Now let us take "identities as paths" literally. Then, when attempting to find semantics of type theory in model categories, an obvious choice of semantics for those identity types would be the path space object. The definition of model categories ensures that these exist, and that they are :ref:`fibrations <fibrations>`.
This is a fine choice until you consider computation rules (which, semantically, are strict equalities). This obvious choice of semantics for identity types may not satisfy the required computation rules. So instead, for example in a variant of the :ref:`cubical sets <cubical_sets>` semantics, a slightly different choice of semantics is chosen for \mathsf{Id}. However, the obvious choice of path space object still exists, and this is often referred to as \mathsf{Path}.