Use and introduction of identity types

[mikeshulman]

It's annoying that we use the identity type for some examples in chapter 1 before we actually introduce it. I still do think that we should wait until the end of the chapter to introduce it formally, but maybe something can be done to improve the situation a bit. Perhaps we can mention its existence and its intuition a bit more "officially" towards the beginning of the chapter, rather than dragging it in on an ad hoc basis as needed for the examples.

[andrejbauer]

Do we need the identity types for any purpose other than to have a non-trivial dependent type?

[mikeshulman]

If we can think of nontrivial examples that don't use the identity type, then I'd be happy to replace the existing examples with those.

[andrejbauer]

A concrete one might be vectors of size n, but that requires induction on n. If we can assume the natural numbers, then an obvious one is Fin n = {k : nat & k < n}.

[vladimirias]

This requires k < n which requires universe. As soon as you have a universe there are very simple examples. V.

On Oct 20, 2014, at 9:38 PM, Andrej Bauer notifications@github.com wrote:

A concrete one might be vectors of size n, but that requires induction on n. If we can assume the natural numbers, then an obvious one is Fin n = {k : nat & k < n}.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/730#issuecomment-59835642.

[andrejbauer]

@vladimirias, what would you suggest as an acceptable introductory example of a dependent type involving a universe?

[vladimirias]

T:U

If we had El we would have written El(T). This is the most fundamental example of a dependent type together with the identity.

V.

On Oct 21, 2014, at 2:08 PM, Andrej Bauer notifications@github.com wrote:

@vladimirias https://github.com/vladimirias, what would you suggest as an acceptable introductory example of a dependent type involving a universe?

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/730#issuecomment-59924223.

[mikeshulman]

But precisely because it's so fundamental, it's not very useful as an example to illustrate anything.

Amusingly, once we have nat and a universe, we can also define the equality on nat (i.e. the codes fibration) just as easily as the order. But perhaps that would be too confusing...

[EgbertRijke]

I personally found it nice to have identity types appear earlier than we formally introduce them. The function of that is to peak ahead and have already one toe in the water before diving in. The readers who have read the introduction have already seen the identity types being introduced, shouldn't that be sufficient?

[mikeshulman]

@EgbertRijke that's a good point, but if that's the idea, I still think it would be helpful to introduce it a little more "officially" rather than on an ad hoc basis as needed for the examples.

[martinescardo]

I explored/exploited the fact that we can define Id on nat, together with J, if we have a universe, in an Agda tutorial for our theory group a while back.

http://www.cs.bham.ac.uk/~mhe/AgdaTutorial/html/AgdaTutorial.html

I think this worked well at that time. I defined Id, refl, J and pointed out that many properties of Id (symmetry, transitivity etc) can then be proved from J without the need of induction on nat.

Moreover, I deliberately started with a weaker version of J (the recursion principle for (Id, refl)), which is enough to do many things. Then I generalized this to J (by making the weak J dependent).

What is missing from this (old) tutorial, written before the HoTT book, among other things, is that uniqueness of the homomorphism from (Id,refl) to any other "identity system" (Id',refl') is equivalent to the induction principle.

Another remark is that although one can define Id,refl,J for nat, the computation rule for the defined J can hold only judgementally. (Even though we are working in a nice system in which every closed term normalized to a canonical form).

Martin

On 21/10/14 18:46, Mike Shulman wrote:

But precisely because it's so fundamental, it's not very useful as an example to illustrate anything.

Amusingly, once we have nat and a universe, we can also define the equality on nat (i.e. the codes fibration) just as easily as the order. But perhaps that would be too confusing...

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/730#issuecomment-59967831.

Martin Escardo http://www.cs.bham.ac.uk/~mhe

[EgbertRijke]

Yes, so what we need to state is id-formation and id-introduction and we need to think about where we introduce these. The first place where we use identity types is with the booleans, but that seems not a very natural place to introduce the identity types. A better place would be in section 1.3 where we introduce families.

[mikeshulman]

Actually, we use identity types already in the uniqueness principle for products in section 1.5. I agree, mentioning them in section 1.3 makes sense. We could consider mentioning when we discuss booleans and/or natural numbers that the equality for those can be defined by recursion, as Martin mentions; I'm not sure what I think about that.

[EgbertRijke]

The risk is that it would lead us too much on a side track. The purpose of the preliminaries chapter is to introduce the type constructors and do some very basic things with them to illustrate how they work. We should stick to that, to keep it clear what we're doing in that chapter.

But it would be useful to tell in the preliminaries chapter that recursion together with the universes can also be used to define type families over inductive types. So we could use Martin's suggestion to illustrate this technique. But then I wouldn't take it much further than that. Probably it would then be best to only give a forward reference to where it is proved that this relation is equivalent to identity.