Induction principles and path induction

[rezk576]

In Chapter 1, a bunch of types are introduced, each with their own induction principles. In most cases, the induction principle is an object of a particular type, which comes with a defining equation. (Actually, no such defining equation is given for ind for coproduct types (1.7), though I'm sure it can be.)

The case of path induction seems very different; in 1.12.1, the path induction dependent function is merely asserted to exist, though subject to an equality when applied to refl.

Naively, it looks to me as though most of these induction maps are constructive (being given with defining equations), while path construction appears non-constructive.

Quite possibly this is not the case, and this distinction that I perceive here (between constructive and non-constructive induction principles) really doesn't exist. However, I can't find any discussion of this issue here; it seems like an important point to be addressed. Perhaps it is later on.

[mikeshulman]

There is no difference. Any difference in phrasing is probably due to the fact that they were written by different people at different times. Can you suggest a modification to the wording of section 1.12 that would make it clear that exactly the same thing is going on?

[rezk576]

I can't think of such a wording, because I don't see why there is no difference. I believe you that there isn't, but I don't understand enough to see why.

[mikeshulman]

Can you imagine what it would be like for there to be no difference? I don't see a difference, so I don't really understand what difference you are thinking there is. Is there something different about the notion of identity type -- as opposed to the way we wrote about them -- which makes you think there must be a difference?

[mikeshulman]

Does the following help? In all cases, the induction principle says that given certain data, we are allowed to introduce a new function, and that that function satisfies certain judgmental equations. In the case of coproducts, the data is two functions g: Prod(a:A) P(inl(a)) and h: Prod(b:B) P(inr(b)), the function f we introduce has type Prod(x:A+B) P(x), and its equations are f(inl(a)) == g(a) and f(inr(b)) == h(b). In the case of identity types, the data is a function d: Prod(a:A) P(a,a,refla), the function f we introduce has type Prod(x,y:A) Prod_(p:x=y) P(x,y,p), and its equation is f(a,a,refl_a) == d(a). The situations are exactly analogous.

[rezk576]

I don't know. It's probably because I'm thinking as a homotopy theorist.

Let f:P->X^I be a fibration over the path space of X. Suppose I have a section s:X->P of f over the constant paths; i.e., fs=c where c:X->X^I is the inclusion of constant paths. Then I might hope and expect to be able to say that there exists an extension s':X^I->P of s to the whole path space, such that s'c=s. However, I would not expect to say that I therefore have a construction of s', without knowing something more explicit about the situation.

This is the standard situation that comes up all the time in homotopy theory. A section exists, and in fact is unique in a strong homotopical sense (i.e., is parameterized by a contractible space of solutions), yet we do not have an explicit choice of solution which we can then feed into some other construction. I'm very curious to see how type theory gets around this issue.

[mikeshulman]

Yes, you are thinking too much like a homotopy theorist. Everything in type theory is constructive/algebraic. Perhaps it would help you to think of type families as corresponding, not to fibrations as such, but to fibrations equipped with path-lifting functions? But I don't think we want to say that to everyone, since to someone not as steeped in homotopy theory it would be an extra layer of confusion. Hmm.

[mikeshulman]

It's also really important for the reader to understand that any intuition they may have from homotopy theory or category theory is only that -- intuition -- and may or may not always supply the right answer. The rules of type theory that we are introducing must be taken literally on their own terms as describing the system we are working in, and they are the only justification for everything. Should we emphasize that more?

[rezk576]

I'm happy to imagine that the type families come with path-lifting functions. But if I do, then I'm going to start wondering how to compute such functions. Or is that not the right thing to wonder about?

[mikeshulman]

I'm not sure what you mean, but in general, you shouldn't be thinking about computation except when reading the "Open problems" section of the Introduction or the chapter Notes. Is it really so hard to take type theory as a formal system on its own terms?

[RobertHarper]

it is EXACTLY the right thing to wonder about, in my opinion at least! the computational interpretation of hott is currently lacking, which i find to be a curious, and i hope temporary situation. as i mentioned on my blog last week, the reason hott "works" is because of constructivity, particularly not affirming lem in all cases, and yet the theory currently has no computational justification. one is left wondering, absent such, why lem and not some other principle? at the moment the justification is pragmatic ("it works"), rather than foundational ("it means that all propositions are effectively decidable, which they are not").

On Jun 28, 2013, at 3:51 PM, rezk576 wrote:

I'm happy to imagine that the type families come with path-lifting functions. But if I do, then I'm going to start wondering how to compute such functions. Or is that not the right thing to wonder about?

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

[mikeshulman]

As a question for future development of the theory, yes, it is A right thing to wonder about. But it's not something that anyone should be getting hung up on preventing them from understanding the book, which makes perfect sense as mathematics, even if it is not ultimately satisfactory to a programmer.

[guillaumebrunerie]

Sections 2.5 to 2.13 more or less explain how to compute these path-lifting functions, see for instance theorems 2.6.4, 2.7.4, 2.10.5, 2.11.{2,3,4,5}. It’s not an algorithm, though, and finding the algorithm is a very important open problem (but the nature of this problem is quite different from the content of the book).

[RobertHarper]

agreed. it is in general A good thing to look at, and for me is THE good thing to look at.

On Jun 28, 2013, at 4:02 PM, Mike Shulman wrote:

As a question for future development of the theory, yes, it is A right thing to wonder about. But it's not something that anyone should be getting hung up on preventing them from understanding the book, which makes perfect sense as mathematics, even if it is not ultimately satisfactory to a programmer.

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

[mikeshulman]

So @rezk576, when you said "I'm going to start wondering" did you mean "wondering" in the sense of "gee, I wonder how one could extend the theory so that we could compute with these path-lifting functions" (in which case, excellent!) or in the sense of "huh, I wonder what is going on? This doesn't make sense if we can't compute these path-lifting functions" (in which case, we need to do some more explanation somewhere)?

[mikeshulman]

At #399 is a proposed change to clarify this issue. @rezk576, does it help at all?

[rezk576]

It seems better.