Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: inductive type

Bottom of Page

1 to 25 of 25

- CommentRowNumber1.
- CommentAuthorUrs
- CommentTimeNov 2nd 2011
- PermaLink
Author: Urs
Format: MarkdownItexI am starting stubs * [[inductive type]] * [[higher inductive type]]
I am starting stubs
- inductive type
- higher inductive type
- CommentRowNumber2.
- CommentAuthorUrs
- CommentTimeDec 8th 2011
- PermaLink
Author: Urs
Format: MarkdownItexI discovered Mike's talk _[Induction on equality](http://www.math.ucsd.edu/~mshulman/papers/induction.pdf)_, enjoyed it a lot, and added a pointer to it to the references at [[inductive type]].

I discovered Mike’s talk Induction on equality, enjoyed it a lot, and added a pointer to it to the references at inductive type.
- CommentRowNumber3.
- CommentAuthorMike Shulman
- CommentTimeDec 8th 2011
- PermaLink
Author: Mike Shulman
Format: MarkdownItexI'm glad you liked it!

I’m glad you liked it!
- CommentRowNumber4.
- CommentAuthorUrs
- CommentTimeDec 8th 2011
- PermaLink
Author: Urs
Format: MarkdownItexYes, 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?

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?
- CommentRowNumber5.
- CommentAuthorTobyBartels
- CommentTimeDec 9th 2011
- PermaLink
Author: TobyBartels
Format: MarkdownItexI'm not sure that I believe that $refl(3)$ is the only proof that $3 = 3$. Another proof would be: * Prove (by some means, which I'm sure you can think of) that $3 = (1 + 1) + 1$. * Prove that $(1 + 1) + 1 = 1 + (1 + 1)$. * Prove that $1 + (1 + 1) = 3$. * Apply transitivity twice. 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: * Prove that $3 = (1 + 1) + 1$. * Prove that addition of natural numbers is associative. * Apply the associativity of natural numbers thrice to $1$. * Prove that $1 + (1 + 1) = 3$. * Apply transitivity twice. 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.)
I’m not sure that I believe that $refl(3)$ is the only proof that $3 = 3$ . Another proof would be:
- Prove (by some means, which I’m sure you can think of) that $3 = (1 + 1) + 1$ .
- Prove that $(1 + 1) + 1 = 1 + (1 + 1)$ .
- Prove that $1 + (1 + 1) = 3$ .
- Apply transitivity twice.
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:
- Prove that $3 = (1 + 1) + 1$ .
- Prove that addition of natural numbers is associative.
- Apply the associativity of natural numbers thrice to $1$ .
- Prove that $1 + (1 + 1) = 3$ .
- Apply transitivity twice.
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.)
- CommentRowNumber6.
- CommentAuthorTobyBartels
- CommentTimeDec 9th 2011
- PermaLink
Author: TobyBartels
Format: MarkdownItexOK, 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))))$.

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))))$ .
- CommentRowNumber7.
- CommentAuthorMike Shulman
- CommentTimeDec 9th 2011
- PermaLink
Author: Mike Shulman
Format: MarkdownItexUrs: it was students at [Mathcamp](http://www.mathcamp.org). 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).

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).
- CommentRowNumber8.
- CommentAuthorDavid_Corfield
- CommentTimeDec 9th 2011
- PermaLink
Author: David_Corfield
Format: MarkdownItexWhat'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?

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?
- CommentRowNumber9.
- CommentAuthorTobyBartels
- CommentTimeDec 9th 2011
- PermaLink
Author: TobyBartels
Format: MarkdownItex@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}$.

@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}$ .
- CommentRowNumber10.
- CommentAuthorTobyBartels
- CommentTimeDec 9th 2011
- PermaLink
Author: TobyBartels
Format: MarkdownItex@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.

@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.
- CommentRowNumber11.
- CommentAuthorMike Shulman
- CommentTimeDec 9th 2011
- PermaLink
Author: Mike Shulman
Format: MarkdownItex@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.

@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.
- CommentRowNumber12.
- CommentAuthorMike Shulman
- CommentTimeDec 9th 2011
- PermaLink
Author: Mike Shulman
Format: MarkdownItex@Toby: I've written out the proof that types with computationally-decidable equality are sets [here](http://nlab.mathforge.org/nlab/show/set#InHoTT). Do you also want to see the proof that $\mathbb{N}$ has computationally decidable equality?

@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?
- CommentRowNumber13.
- CommentAuthorTobyBartels
- CommentTimeDec 9th 2011
- PermaLink
Author: TobyBartels
Format: MarkdownItexThanks, I'll see if I can make that give me the path that I desire.

Thanks, I’ll see if I can make that give me the path that I desire.
- CommentRowNumber14.
- CommentAuthorMike Shulman
- CommentTimeDec 13th 2011
- PermaLink
Author: Mike Shulman
Format: MarkdownItexReturning 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](http://homotopytypetheory.org/2011/12/06/inductive-localization/)) and spectrification.

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.
- CommentRowNumber15.
- CommentAuthorUrs
- CommentTimeDec 14th 2011
- PermaLink
Author: Urs
Format: MarkdownItexNice. I have added a bunch of further hyperlinks.

Nice. I have added a bunch of further hyperlinks.
- CommentRowNumber16.
- CommentAuthorDavid_Corfield
- CommentTimeDec 14th 2011
- PermaLink
Author: David_Corfield
Format: MarkdownItexCan you define things like the category of braids, the free braided monoidal category on a single object, as an inductive type?

Can you define things like the category of braids, the free braided monoidal category on a single object, as an inductive type?
- CommentRowNumber17.
- CommentAuthorMike Shulman
- CommentTimeDec 14th 2011
- PermaLink
Author: Mike Shulman
Format: MarkdownItex@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?

@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?
- CommentRowNumber18.
- CommentAuthorMike Shulman
- CommentTimeDec 14th 2011
- PermaLink
Author: Mike Shulman
Format: MarkdownItex@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.

@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.
- CommentRowNumber19.
- CommentAuthorUrs
- CommentTimeDec 14th 2011
- (edited Dec 14th 2011)
- PermaLink
Author: Urs
Format: MarkdownItexHi 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.

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.
- CommentRowNumber20.
- CommentAuthorMike Shulman
- CommentTimeDec 15th 2011
- PermaLink
Author: Mike Shulman
Format: MarkdownItexI 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.

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.
- CommentRowNumber21.
- CommentAuthorMike Shulman
- CommentTimeDec 16th 2011
- PermaLink
Author: Mike Shulman
Format: MarkdownItexThanks 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).

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).
- CommentRowNumber22.
- CommentAuthorTodd_Trimble
- CommentTimeDec 16th 2011
- PermaLink
Author: Todd_Trimble
Format: MarkdownItexI 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?

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?
- CommentRowNumber23.
- CommentAuthorMike Shulman
- CommentTimeDec 16th 2011
- PermaLink
Author: Mike Shulman
Format: MarkdownItexYeah, 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.

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.
- CommentRowNumber24.
- CommentAuthorTodd_Trimble
- CommentTimeDec 16th 2011
- PermaLink
Author: Todd_Trimble
Format: MarkdownItexMike #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.)

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.)
- CommentRowNumber25.
- CommentAuthorMike Shulman
- CommentTimeDec 16th 2011
- PermaLink
Author: Mike Shulman
Format: MarkdownItexAh, yes. Sorry, I assumed you were replying only to #21. We all need more time than we have...

Ah, yes. Sorry, I assumed you were replying only to #21. We all need more time than we have…

1 to 25 of 25

nForum

Discussion Feed

Not signed in

Site Tag Cloud

nLab > Latest Changes: inductive type