Path induction again (sorry)

[gluttonousGrandma]

I'm really confused. I've read the first five chapters of the HoTT book and I still don't understand why path induction works.

I've come to the following conclusions about HoTT and type theory in general, please correct me if I'm wrong.

1. The general induction principles are just basic rules of type theory, something like axioms (but not exactly axioms, because axioms in HoTT are something else), you can hope to derive some induction principles from the others, but you still need to believe in at least one of them. The intuition behind induction principle is that if you can define how a function behaves on constructors of a type, then you can define a function on the whole type --- and it's a reasonable thing to believe in, because we expect that everything that a type contains has gotten there by means of the constructors of the type.
2. If there is no univalence, the identity types contain only refl's. We still have concatenation and inverses lemmas, and transport, but they are all trivial.
3. After we introduce univalence we now have nontrivial paths. And these nontrivial paths have gotten into the identity types somewhat invasively, by some sort of magic, not by means of the constructors. Some of these nontrivial paths we build directly by univalence, while the others may be build using lemmas we proved (e.g. concatenations), which in turn use induction principle which is based on the intuition that there are no other paths but the paths that are build with constructors.
4. We understand that intuition behind path induction fails, but we just go ahead and continue to use path induction anyways.

Am I terribly wrong on all of this? Should I start reading the book from the beginning?

[mikeshulman]

Well, you're not alone; your confusion is what obstructed (and continues to obstruct) a lot of type theorists from really believing in HoTT. I had hoped that we had written the book so as not to lead newcomers to this sort of misunderstanding, but maybe it is inevitable.

Try re-reading the beginning of section 5.8?

[RobertHarper]

your concerns about the nature of path induction are understandable, and are related to the absence of a computational interpretation of the theory in the hott book. here's a way to think about things that may allay your concerns.

as you point out, the structure of paths in intensional type theory is degenerate in that there are only reflexivities at each type. in particular, any two propositionally equivalent terms are in fact definitionally equivalent. as a result propositional equality in pure itt is nearly useless for mathematical purposes, lacking as it does even function extensionality, whereby two functions would be identified if they have the same graph (i/o behavior).

homotopy type theory enriches propositional equality in at least two ways, univalence and higher inductive types. to understand why these make sense it is helpful to revisit the meaning of the propositional equality as specifying an abstract type of paths between points in a space. in pure itt there meaning of propositional equality is given independently of the space, which results in the degenerate structure just mentioned. however, one can re-interpret itt in such a way that it admits generalization to hott by treating the notion of paths in a space as dependent on the space itself. so, for example, a path in a product space, A1xA2, consists of two paths, one in A1 and one in A2. similarly, a path in a function space, A1->A2, consists of a homotopy between two functions, and so forth. from this point of view reflexivity is not an atomic concept, but is rather definable at each type. for example, reflexivity at A1xA2 is a pair of reflexivities, one for A1 and one for A2, and reflexivity at A1->A2 is a homotopy consisting of reflexivities (speaking loosely here). with this in mind we can envision defining the path structure of any type we wish to introduce, for example paths in the universe are equivalences, and reflexivity is a particular equivalence, and paths in a higher inductive type are specified by the inductive definition, and reflexivity is defined trivially for the zero cells as a constructor.

now let's reconsider the meaning of identity elimination. in pure itt it says that everything respects equality. in hott this is better read as everything respects paths (homotopies) in any space. so, for example, one cannot define a map out of a higher inductive type without specifying how it respects the paths in the domain, nor can one define a map out of a universe that does not respect equivalence. given this, the elimination form allows you to take explicit advantage of this fact. in pure itt this can be stated as one axiom about reflexivity, but in hott reflexivity is a non-trivial thing, as just described. so instead the elimination form must be understood separately for each type over which we are considering paths. identity elimination for a product type works with pairs of paths, and so forth, and at a universe it applies the underlying equivalence, and at higher inductives it analyzes the particular paths generated by the definition. (a subtlety is that with higher inductives you get more paths than you explicitly specify due to higher coherences; these must be dealt with by the elimination form for identity, just as it must for the specified paths. much of the subtlety of fundamental groups stems from these implicit paths that are very hard to characterize fully in the general case.)

when seen from this perspective, one can begin to sense that there is a computational interpretation of hott that would satisfy your concerns. this is the subject of active research.

regards, bob harper

On Aug 27, 2013, at 10:34 AM, gluttonousGrandma wrote:

I'm really confused. I've read the first five chapters of the HoTT book and I still don't understand why path induction works.

I've come to the following conclusions about HoTT and type theory in general, please correct me if I'm wrong.

The general induction principles are just basic rules of type theory, something like axioms (but not exactly axioms, because axioms in HoTT are something else), you can hope to derive some induction principles from the others, but you still need to believe in at least one of them. The intuition behind induction principle is that if you can define how a function behaves on the constructors of a type, then you can define a function on the whole type --- and it's a reasonable thing to believe in, because we expect that everything that a type contains have gotten there by means of the constructors of the type.

If there is no univalence, the identity types contain only refl's. We still have concatenation and inverses lemmas, and transport, but they are all trivial.

After we introduce univalence we now have nontrivial paths. And these nontrivial paths have gotten into the identity types somewhat invasively, by some sort of magic, not by means of the constructors. Some of these nontrivial paths we build directly by univalence, while the others are perhaps build using lemmas we proved (e.g. concatenations), which in turn use induction principle which is based on the intuition that there are no other paths but the paths that are build with constructors.

We understand that intuition behind path induction fails, but we just go ahead and continue to use path induction anyways.

Am I terribly wrong on all of these? Should I start reading the book from the beginning?

— Reply to this email directly or view it on GitHub.

[awodey]

On Aug 27, 2013, at 10:34 AM, gluttonousGrandma notifications@github.com wrote:

I'm really confused. I've read the first five chapters of the HoTT book and I still don't understand why path induction works.

I've come to the following conclusions about HoTT and type theory in general, please correct me if I'm wrong.

The general induction principles are just basic rules of type theory, something like axioms (but not exactly axioms, because axioms in HoTT are something else), you can hope to derive some induction principles from the others, but you still need to believe in at least one of them.

they are definitions, so it doesn't really make sense to "believe in them". The intuition behind induction principle is that if you can define how a function behaves on the constructors of a type, then you can define a function on the whole type --- and it's a reasonable thing to believe in, because we expect that everything that a type contains have gotten there by means of the constructors of the type.

this is only true for certain kinds of inductive types, but not for all. If there is no univalence, the identity types contain only refl's. We still have concatenation and inverses lemmas, and transport, but they are all trivial.

no, this is not true. there may be nontrivial paths without assuming UA. After we introduce univalence we now have nontrivial paths. And these nontrivial paths have gotten into the identity types somewhat invasively, by some sort of magic, not by means of the constructors.

no. 3 and 4 are not right.

Some of these nontrivial paths we build directly by univalence, while the others are perhaps build using lemmas we proved (e.g. concatenations), which in turn use induction principle which is based on the intuition that there are no other paths but the paths that are build with constructors.

We understand that intuition behind path induction fails, but we just go ahead and continue to use path induction anyways.

Am I terribly wrong on all of these? Should I start reading the book from the beginning?

— Reply to this email directly or view it on GitHub.

[mikeshulman]

As you can see, there are differences of opinion even among the authors of the book. Bob's is one way of looking at it. I maintain that one can be completely satisfied with path induction as resulting from an inductive definition of identity types, together with HITs and univalence, whether or not there is a computational interpretation of HoTT; this is what section 5.8 tries to explain.

they are definitions, so it doesn't really make sense to "believe in them".

I think it does make sense to "believe in" axioms or rules; at a formal level we just take them as given, but we have to have some reason for choosing to take particular ones over particular other ones.

The intuition behind induction principle is that if you can define how a function behaves on the constructors of a type, then you can define a function on the whole type --- and it's a reasonable thing to believe in, because we expect that everything that a type contains have gotten there by means of the constructors of the type.

this is only true for certain kinds of inductive types, but not for all.

To clarify: the first part of your statement ("if you can define how a function behaves on the constructors of a type, then you can define a function on the whole type") is true for all inductive types: it's essentially just a restatement of the induction principle. It's the second part ("it's a reasonable thing to believe in, because we expect that everything that a type contains have gotten there by means of the constructors of the type") which is not always true. What's always true is that, as explained in section 5.8, an inductive types is freely generated by its constructors. If there are no other operations around acting on those constructors, then indeed there will be nothing else in the type except them, but that may not always be the case (and indeed it is not the case for identity types).

there may be nontrivial paths without assuming UA.

More precisely, type theory without UA and HITs does not rule out nontrivial paths, but it's true that it gives us no way to construct them --- at least, no way to construct them in the empty context.

[gluttonousGrandma]

Thanks everyone! It's really great to see different explanations and clarifications.

What's always true is that, as explained in section 5.8, an inductive types is freely generated by its constructors. If there are no other operations around acting on those constructors, then indeed there will be nothing else in the type except them, but that may not always be the case (and indeed it is not the case for identity types).

I feel like this is a stupid question, but is there an example of a simple type and an operation acting on it (and an induction principle for it)? I understand the free-groups example from the book, but I just can't see how it fits in type-theoretic framework. (I guess it's finally time to read a book on type theory.)

And frankly, I don't even get why, when defining a function on a group, it is enough to define it on generators of a group (so maybe there's just no hope for me).

[gluttonousGrandma]

And frankly, I don't even get why, when defining a function on a group, it is enough to define it on generators of a group (so maybe there's just no hope for me).

Oh, that was really stupid of me, sorry, I get it now ("functions" between groups are homomorphisms).

[mikeshulman]

Right. From a category-theorist's point of view, type theory is a formal syntax for describing objects and morphisms in some category. The category has to have sufficient structure to match the type constructors that one assumes in the appropriate type theory, e.g. for simply typed lambda calculus, the category has to be cartesian closed; for extensional dependent type theory, it should be locally cartesian closed; for homotopy type theory, it should be a certain sort of model category or $(\infty,1)$-category, etc. The category of groups is a perfectly good category with sufficient structure to interpret a certain type theory (no function types or dependent types, but it does have products and coproducts). Thus, one valid semantics of type theory is in the category of groups, where the coproduct type (for instance) would be interpreted by the free product of groups and hence would contain many more elements than those arising from the two constructors.

[awodey]

Another thing to keep in mind is the possibility of basic types that are not inductive, like when interpreting the system with respect to some given spaces.

Sent from my iPhone

On Aug 27, 2013, at 2:01 PM, Mike Shulman notifications@github.com wrote:

As you can see, there are differences of opinion even among the authors of the book. Bob's is one way of looking at it. I maintain that one can be completely satisfied with path induction as resulting from an inductive definition of identity types, together with HITs and univalence, whether or not there is a computational interpretation of HoTT; this is what section 5.8 tries to explain.

they are definitions, so it doesn't really make sense to "believe in them".

I think it does make sense to "believe in" axioms or rules; at a formal level we just take them as given, but we have to have some reason for choosing to take particular ones over particular other ones.

The intuition behind induction principle is that if you can define how a function behaves on the constructors of a type, then you can define a function on the whole type --- and it's a reasonable thing to believe in, because we expect that everything that a type contains have gotten there by means of the constructors of the type.

this is only true for certain kinds of inductive types, but not for all.

To clarify: the first part of your statement ("if you can define how a function behaves on the constructors of a type, then you can define a function on the whole type") is true for all inductive types: it's essentially just a restatement of the induction principle. It's the second part ("it's a reasonable thing to believe in, because we expect that everything that a type contains have gotten there by means of the constructors of the type") which is not always true. What's always true is that, as explained in section 5.8, an inductive types is freely generated by its constructors. If there are no other operations around acting on those constructors, then indeed there will be nothing else in the type except them, but that may not always be the case (and indeed it is not the case for identity types).

there may be nontrivial paths without assuming UA.

More precisely, type theory without UA and HITs does not rule out nontrivial paths, but it's true that it gives us no way to construct them --- at least, no way to construct them in the empty context.

— Reply to this email directly or view it on GitHub.

[andrejbauer]

In my experience the root of such confusion is usually the belief that "everything that an inductive type contains has gotten there by means of the constructors of the type". We base our intuitions and beliefs on our mathematical experience. A student's beliefs about real-valued functions change when you show him one that is discontnuous at rational values and differentiable at irrational values. So let me try to shatter your intuitions about inductive types by means of specific counter-examples.

Consider the inductive type of natural numbers nat. It has one constant Zero and a unary constructor Succ.

In the category of sets it is interpreted by the usual set of natural numbers. Most peopple think of the natural numbers this way.

Now we switch to the category of pointed sets, where an object (A,a) is a set A together with a chosen element a (the "point") and maps preserve points. What is the interpretation of nat now? Well, it has to have a point. But it turns out that you cannot use 0, or any other number as a point, you have to add a new one! So the natural numbers are interpreted as the set of natural numbers together with an additional point. Everything is ok, though, because all maps preserve the point.

Now we switch to the category of sheaves on a space X, where nat correspond to the sheaf of continuous maps from X to the discrete space of the natural numbers N. There is the constantly 0 map, which corresponds to Zero, and in fact for each natural number n the constant map taking everything to n corresponds to the term Succ (Succ (Succ ... Zero)) where Succ is iterated n times. And these are all the elements of our sheaf, if X is a connected space. But if X is very disconnected there will be many more continuous maps from X to N. But everything is still ok. Despite there being many more elements than those obtained by Zero and Succ, our type is still initial because we get all those other elements by a process of completion (sheafification), and every morphism in the category "commutes" with completion in a suitable sense.

I will leave you with a question: are the natural numbers in the category of compact Hausdorff spaces the one-point compactification of the natural numbers, or the Stone-Čech compactification of natural numbers, or neither?

Once you stop thinking that the inductive type of natural numbers contains only natural numbers, it is much easier to think that the identity type could contains a lot of things.

[andrejbauer]

The discussion prompted me to write a blog post: http://math.andrej.com/2013/08/28/the-elements-of-an-inductive-type/

[RobertHarper]

great! i was going to write something about this, but you've done a better job than i could have.

bob

Sent from tablet

On Aug 28, 2013, at 10:19, Andrej Bauer notifications@github.com wrote:

The discussion prompted me to write a blog post: http://math.andrej.com/2013/08/28/the-elements-of-an-inductive-type/

— Reply to this email directly or view it on GitHub.

[gluttonousGrandma]

Wow, thanks for the thorough response. I must say this whole type-theory-as-syntax-for-categories perspective is just out of the blue, and it makes me wondering if I really understand anything in type theory. Is there a good place to read about this view?

(This is definitely very wrong, but the picture I have in mind so far is this: there is type theory -- a formal language, and (some) category --- a real thing. It's true that every term in identity types is refl, but terms are just labels, in reality there may be a lot of real elements. And now univalence secretly inserted real elements in some identity types, and then, because path induction doesn't look behind the scenes and knows only about labels such as refl, the inserted elements spread like infection with the help of concatenation and other lemmas.)

[mikeshulman]

It sounds to me like maybe you haven't really absorbed the argument for why path induction is correct even if not all paths are refl.

[awodey]

it is not in general true that every term of identity type is refl, and it is not the case that univalence is the only source of non-refl identity terms.

On Aug 28, 2013, at 1:49 PM, gluttonousGrandma notifications@github.com wrote:

Wow, thanks for the thorough response. I must say this whole type-theory-as-syntax-for-categories perspective is just out of the blue, and it makes me wondering if I really understand anything in type theory. Is there a good place to read about this view?

(This is definitely very wrong, but the picture I have in mind so far is this: there is type theory -- a formal language, and (some) category --- a real thing. It's true that every term in identity types is refl, but terms are just labels, in reality there may be a lot of real elements. And now univalence secretly inserted real elements in some identity types, and then, because path induction doesn't look behind the scenes and knows only about labels such as refl, the inserted elements spread like infection with the help of concatenation and other lemmas.)

— Reply to this email directly or view it on GitHub.

[andrejbauer]

Ah, another misconception. This time it is about the meaning of the eliminator. Why does the elimination principle for identity types work? Is it because the only element of the idenity type is refl, for which elimination obviously works? No! It is because all paths, whatever they are, have the "transport" property that makes elimination work. The amazing thing is that the necessary "transport" property is a well established concept in homotopy theory. If it were not, we could still cook it up, but we would probably not recognize it as important.

[gluttonousGrandma]

No! It is because all paths, whatever they are, have the "transport" property that makes elimination work.

What exactly is this property? In the book transport is defined using path induction.

[andrejbauer]

Because we are using fibrations (in the sense of homotopy theory) to model type families, and fibrations behave nicely with respect to paths in the base space, we can always transport stuff from one fiber to another along a path in the base space. And this is the reason that path induction works. (And I am mixing up "indcution" and "transport" a bit, but only a little bit, so that I can focus on transport which has a nicer geometric picture.)

[mikeshulman]

But why is it valid to use fibrations to model type families, if not because the latter inherit a property of transport from path induction? That argument seems circular to me.

[andrejbauer]

It's not a circular argument:

1. You notice that fibrations are ok to model type theory. (NB: fibrations are a concept that is older than type theory).
2. You discover that there are homotopy models in which identity types are non-trivial.
3. Everything is ok because in step 1 we noticed that fibrations are ok.

[mikeshulman]

This is not really an issue any more (if it ever was).