Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP

Loading…

Path induction again (sorry) #460

Closed
gluttonousGrandma opened this Issue · 20 comments

5 participants

@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
Owner

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
Collaborator
@awodey
Owner
@mikeshulman
Owner

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
Owner

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
Owner
@andrejbauer
Owner

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
Owner

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

@RobertHarper
Collaborator
@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
Owner

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
Owner
@andrejbauer
Owner

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
Owner

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
Owner

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
Owner

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
Owner

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.