Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I am starting stubs
I discovered Mike’s talk Induction on equality, enjoyed it a lot, and added a pointer to it to the references at inductive type.
I’m glad you liked it!
Yes, I liked it a lot. This mix of the very basic and the unfathomably profound. I roughly knew by now what you explain there, but it was good to see it explained in such detail.
Of course I have the advantage of knowing how the story continues. I could easily imagine that somebody who doesn’t would feel irritated by a long talk on just the natural numbers and the notion of equality! What was the audience like that you gave this talk to?
I’m not sure that I believe that $refl(3)$ is the only proof that $3 = 3$. Another proof would be:
You have to have some argument that this complicated proof reduces down to $refl(3)$. And actually, if you write down recursive definitions of addition and look at the obvious proofs of these facts in some detail, you can probably convince people of this. But now try this alternative proof:
And now if you write the obvious proofs of these facts in some detail, it is not so clear that this reduces down to $refl(3)$; there is some application of induction and $\forall$ that doesn’t easily collapse into nothing.
(I first wrote this with $1 + 2 = 2 + 1$ in place of $(1 + 1) + 1 = 1 + (1 + 1)$; but anybody who hasn’t tried this before should look at the thing in detail, and associativity is a lot simpler to prove from first principles than commutativity is. Even simpler would be to use $3 = 0 + 3$ and $0 + 3 = 3$, once as a direct calculation and once as a special case of a general theorem. However, there is an ambiguity in the definition of addition as to which variable you recurse on, and if you choose the other variable than I do, then you’ll find that this usage of a general theorem does collapse into nothing.)
OK, here are the details. I’m doing this with $0 + 3$.
First, for the record, the recursive definition of addition: $n + 0 \coloneqq n$, and $n + S(m) \coloneqq S(n + m)$.
First to see how a proof collapses, I’ll do $3 + 0$ (which will collapse). Directly, $3 = 3 + 0$ by immediate application of the definition. Since $3 + 0$ is defined to be $3$ itself, arguably there is nothing here but $refl(3)$. Now, the general proof that $n + 0 = n$ requires simply the definition again, so it is also reflexivity, essentially the infinite list $(refl(0), refl(1), refl(2), \ldots)$. So when we apply this to $3$, the proof is just $refl(3)$. And I’ll let you check for yourself (inspecting the recursive proof of transitivity that you found in the exercise on page 30) that when you apply transitivity to $refl(3)$ and $refl(3)$, you just get $refl(3)$.
But now, consider $0 + 3$. Directly, $3 = 0 + 3$ by a bit of argument: $3 = S(2) = S(S(1)) = S(S(S(0))) = S(S(S(0 + 0))) = S(S(0 + S(0))) = S(S(0 + 1)) = S(0 + S(1)) = S(0 + 2) = 0 + S(2) = 0 + 3$. But long as this is, every step comes directly from a definition, so every equality proof is reflexivity ($refl(3)$, as it happens). And transitivity collapses this string of ten copies of $refl(3)$ into a single $refl(3)$. So in the end, nothing is there. Now, the general proof that $0 + n = n$ is also more complicated and requires induction. First, $0 + 0 = 0$ (by definition, hence $refl(0)$); next, if $0 + k = k$, then $0 + S(k) = S(0 + k) = S(k)$. Every step in this last chain is by definition (hence $refl(S(k))$, or at least $refl(0 + S(k))$) except the last, which is the induction hypothesis (with substitution applied to it). Transitivity makes all of the applications of reflexivity collapse, so the induction step is essentially the function from $p\colon 0 + k = k$ to $S(p)\colon S(0 + k) = S(k)$ (an instance of substitution). Thus the entire proof that $0 + n = n$ in general is the sequence $(refl(0), S(refl(0)), S(S(refl(0))), \ldots)$. Applying this to $3$ then gives us $S(S(S(refl(0))))$. Since this is simply combined with $refl(3)$ by transitivity, the entire proof boils down to $S(S(S(refl(0))))$. So the claim is that this is the same proof as $refl(S(S(S(0))))$.
Urs: it was students at Mathcamp. I did get one comment afterwards — from one of the other instructors, not one of the kids — along the lines you mention.
Toby: I didn’t mean to claim that any proof of $3=3$ is definitionally equal to $refl(3)$, only propositionally equal to it. And that is possible to prove, because $\mathbb{N}$ is an hSet: any two parallel paths (equalities) in $\mathbb{N}$ are connected by a path (equality). And one way to prove that $\mathbb{N}$ is an hSet is to show that it has computationally decidable equality (i.e. decidable equality in the propositions-as-types sense).
What’s the technical reason for induction and recursion being “two faces of the same thing”? Is it something like in a category of algebras being initial is equivalent to having only isomorphic subobjects? The forward direction is true is any category. What about the reverse? With equalizers, I guess we could show any two arrows from the object are the same. Where does the existence come from?
@David: If we already know that the category has a strict initial object, then it’s a subobject of every object, which completes your proof. It can’t work in general, however, since $\emptyset$ is not initial in $Set^{op}$.
@Mike: Can you show me the path between the two proofs that $3 = 3$? I accept that such a path exists in HTT (although I haven’t had time to understand that yet as I’d like), but you didn’t motivate any of the special features of HTT in your talk, so I still have my intuition that they’re different. But if you can show me the path, then I’ll have better intuition for the relevant properties of HTT.
@David: In Set or a topos, the way you prove recursion from induction is to define the notion of a “partial function defined by recursion,” then prove by induction that any two such partial functions agree on their common domain, and that any element is in the domain of some such partial function; then take the union of all such to obtain an honest function. I don’t know how generally that works. All I meant to imply by the vague statement “induction and recursion are two faces of the same thing” (in a talk full of vague and vaguely misleading statements) is that they are both special cases of the same thing, namely the dependent eliminator of an inductive type.
@Toby: I’ve written out the proof that types with computationally-decidable equality are sets here. Do you also want to see the proof that $\mathbb{N}$ has computationally decidable equality?
Thanks, I’ll see if I can make that give me the path that I desire.
Returning to the original topic of this thread, I’ve added a slew of examples to higher inductive type, including two recent ones: localization (see this blog post) and spectrification.
Nice. I have added a bunch of further hyperlinks.
Can you define things like the category of braids, the free braided monoidal category on a single object, as an inductive type?
@Urs: Thanks. I am not really fond of Voevodsky’s “h-level” terminology and would just as soon not use it at all if not necessary; I prefer the usual “truncation” indexing even though it “starts” at (-2). Do you have a positive reason to want to use h-level numbers, or are you just following Voevodsky or the Coq code?
@David: if we’re working in extensional type theory, then I’m pretty sure yes. It suffices to define the braid group on $n$ strands for any $n$, since the braid category is the disjoint union of these. For that you can just use generators and relations: define the type of all words in the generators and their inverses, and quotient it by the relations. You should be able to do that in two steps with quotient types, or in one step with an HIT.
Hi Mike,
I thought this was following the established convention. I have no personal preference for “h-level” and am happy with “truncated”. I’ll stick to “truncated” in the future.
But then we should split off entries for hSet and hProp. For the moment I had made them redirect to h-level, thinking that this is terminology with the same root.
But you decide, you know how terminology should be used here. I am agnostic about it.
I had already made a section set#InHoTT to discuss hsets. But I guess having a separate page for hset and hprop would be a good idea.
Thanks to suggestions from Peter Lumsdaine, I’ve improved the HIT definition of spectrification, cutting the 9 constructors down to 7, with none of them level above 2 (i.e. only paths between paths, nothing higher).
I admit that I find it hard to follow that pseudo-Coq code. Is it possible to amplify on some of this in more traditional (?) terms?
Yeah, I’ll bet — I find it hard to follow too, and I wrote it! I tried to add some more explanation, with more traditional notation. Does that help any? I don’t really have time right now to write a lot about it, though.
Mike #23, I guess we’re both talking about higher inductive type? I looked quickly for changes and saw a few words added to spectrification, but I really want to see all the examples decoded, eventually. But, I understand you’re busy, and it may be good for my soul to see if I can do this myself and then add if I think I’ve got it. (But I really need more time than I seem to have these days.)
Ah, yes. Sorry, I assumed you were replying only to #21. We all need more time than we have…
1 to 25 of 25