Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorMike Shulman
   • CommentTimeNov 30th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI wrote something at [[meaning explanation]], but I didn't add any links to it yet because I'm hoping to get some feedback from type theorists as to its correctness (or lack thereof).

   I wrote something at meaning explanation, but I didn’t add any links to it yet because I’m hoping to get some feedback from type theorists as to its correctness (or lack thereof).

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeNov 30th 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexAfter you get feedback from the experts, I hope you can sprinkle some sugar on the section on natural numbers. I have trouble understanding what the first sentence is about.

   After you get feedback from the experts, I hope you can sprinkle some sugar on the section on natural numbers. I have trouble understanding what the first sentence is about.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeNov 30th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexIt's expressing an assumption about the untyped computational objects with which we began. I'm not sure how to clarify it, can you suggest something?

   It’s expressing an assumption about the untyped computational objects with which we began. I’m not sure how to clarify it, can you suggest something?

4. • CommentRowNumber4.
   • CommentAuthorTodd_Trimble
   • CommentTimeNov 30th 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexLet me reproduce it so that I can refer to it: > Suppose that we have terms $N$, $0$, and $s(x)$, along with a recursor $rec(n,z_0,x r. z_s)$ such that $$rec(0,z_0,x r.z_s) \Rightarrow z_0$$ and $$rec(s(n),z_0,x r. z_s) \Rightarrow z_s[n/x,rec(n,z_0,x r.z_s)/r].$$ In plain English, can you explain what this recursor is supposed to mean? I don't know what $x r$ or $z_s$, or $rec$ for that matter, signify. (Sorry, I do realize it's probably a dumb question.)

   Let me reproduce it so that I can refer to it:

   Suppose that we have terms $N$, $0$, and $s(x)$, along with a recursor $rec(n,z_0,x r. z_s)$ such that

   $$rec(0,z_0,x r.z_s) \Rightarrow z_0$$

   and

   $$rec(s(n),z_0,x r. z_s) \Rightarrow z_s[n/x,rec(n,z_0,x r.z_s)/r].$$

   In plain English, can you explain what this recursor is supposed to mean? I don’t know what $x r$ or $z_s$, or $rec$ for that matter, signify. (Sorry, I do realize it’s probably a dumb question.)

5. • CommentRowNumber5.
   • CommentAuthorTobyBartels
   • CommentTimeNov 30th 2012
   • (edited Dec 3rd 2012)
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexIn $rec(n,z_0,x r. z_s)$, $n$ is a term for a natural number, $z_0$ is a term of some type $Z$, and $z_s$ is a term of type $Z$ with a free variable $x$ for a natural number and a free variable $r$ of type $Z$ (where for some reason[^1] the presence of these free variables is indicated by writing $x r. z_s$ instead of just $z_s$). Then $rec(n,z_0,x r. z_s)$ is also a term of type $Z$. In categorial semantics, think of $n$ as a generalised element of a natural-numbers type $N$, so a map $\Gamma \to N$. Then $z_0\colon \Gamma \to Z$ and $z_s\colon \Gamma \times N \times Z \to Z$, and $rec(n,z_0,x r. z_s)\colon \Gamma \to Z$. Supposing that the term $n$ is a canonical numeral $\underline{m}$, we may express the first few $rec(n,z_0,x r. z_s)\colon \Gamma \to Z$ as follows: * $rec(\underline{0},z_0,x r. z_s)(g) \coloneqq z_0(g)$, * $rec(\underline{1},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{0},z_0)$, * $rec(\underline{2},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{1},z_s(g,\underline{0},z_0))$, * $rec(\underline{3},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{2},z_s(g,\underline{1},z_s(g,\underline{0},z_0)))$, * etc. After the first line, these follow from a general rule: * $rec(\underline{m+1},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{m},rec(\underline{m},z_0,x r. z_s)(g))$. Of course, $\underline{0}$ is what Mike is simply calling $0$, and then $\underline{m+1}$ is $s(\underline{m})$. So writing these two rules properly in type theory as beta-reductions, we have these rules of Mike's: * $rec(0,z_0,x r.z_s) \Rightarrow z_0$ and * $rec(s(n),z_0,x r. z_s) \Rightarrow z_s[n/x,rec(n,z_0,x r.z_s)/r]$ (where for some reason[^2] reduction is written as $\Rightarrow$ instead of as $\rightsquigarrow$). [^1]: I write this before reading Mike\'s article, so there might be a good reason. [^2]: I doubt that there's a good reason for this; $\Rightarrow$ is overloaded enough as it is.

   In $rec(n,z_0,x r. z_s)$, $n$ is a term for a natural number, $z_0$ is a term of some type $Z$, and $z_s$ is a term of type $Z$ with a free variable $x$ for a natural number and a free variable $r$ of type $Z$ (where for some reason¹ the presence of these free variables is indicated by writing $x r. z_s$ instead of just $z_s$). Then $rec(n,z_0,x r. z_s)$ is also a term of type $Z$.

   In categorial semantics, think of $n$ as a generalised element of a natural-numbers type $N$, so a map $\Gamma \to N$. Then $z_0\colon \Gamma \to Z$ and $z_s\colon \Gamma \times N \times Z \to Z$, and $rec(n,z_0,x r. z_s)\colon \Gamma \to Z$. Supposing that the term $n$ is a canonical numeral $\underline{m}$, we may express the first few $rec(n,z_0,x r. z_s)\colon \Gamma \to Z$ as follows:

   • $rec(\underline{0},z_0,x r. z_s)(g) \coloneqq z_0(g)$,
   • $rec(\underline{1},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{0},z_0)$,
   • $rec(\underline{2},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{1},z_s(g,\underline{0},z_0))$,
   • $rec(\underline{3},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{2},z_s(g,\underline{1},z_s(g,\underline{0},z_0)))$,
   • etc.

   After the first line, these follow from a general rule:

   • $rec(\underline{m+1},z_0,x r. z_s)(g) \coloneqq z_s(g,\underline{m},rec(\underline{m},z_0,x r. z_s)(g))$.

   Of course, $\underline{0}$ is what Mike is simply calling $0$, and then $\underline{m+1}$ is $s(\underline{m})$. So writing these two rules properly in type theory as beta-reductions, we have these rules of Mike’s:

   • $rec(0,z_0,x r.z_s) \Rightarrow z_0$ and
   • $rec(s(n),z_0,x r. z_s) \Rightarrow z_s[n/x,rec(n,z_0,x r.z_s)/r]$

   (where for some reason² reduction is written as $\Rightarrow$ instead of as $\rightsquigarrow$).

   ---

   1. I write this before reading Mike's article, so there might be a good reason. ↩

   2. I doubt that there’s a good reason for this; $\Rightarrow$ is overloaded enough as it is. ↩

6. • CommentRowNumber6.
   • CommentAuthorTodd_Trimble
   • CommentTimeDec 1st 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexAh, thanks Toby! That makes it very clear.

   Ah, thanks Toby! That makes it very clear.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeDec 1st 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThanks very much, Toby. The only caveat I would add is that in the context of the meaning explanation, phrases like "of some type Z" should be omitted. My understanding is that in this case, we start with some raw *untyped* notion of computation and then consider how we might *assign* types to its objects. Re: your first footnote, I think it's important to denote all variable bindings somehow. If you just write (say) $rec(0,4,r+s)$ then how do you know whether $r$ or $s$ (or neither) is the free variable denoting the recursive call? The notation $rec(0,4,x r.r+s)$ makes it clear. Re: your second footnote, I was just copying what Peter Dybjer used in his talk today. Feel free to change it to $\rightsquigarrow$ if you prefer.

   Thanks very much, Toby. The only caveat I would add is that in the context of the meaning explanation, phrases like “of some type Z” should be omitted. My understanding is that in this case, we start with some raw untyped notion of computation and then consider how we might assign types to its objects.

   Re: your first footnote, I think it’s important to denote all variable bindings somehow. If you just write (say) $rec(0,4,r+s)$ then how do you know whether $r$ or $s$ (or neither) is the free variable denoting the recursive call? The notation $rec(0,4,x r.r+s)$ makes it clear.

   Re: your second footnote, I was just copying what Peter Dybjer used in his talk today. Feel free to change it to $\rightsquigarrow$ if you prefer.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeDec 2nd 2012
   • (edited Dec 2nd 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHm, looking at the entry _[[meaning explanation]]_, I get away with the impression that all it says is that "If something computes to something that behaves like a certain type, then it is of that certain type". What is there more to it? What is non-trivial in saying this for various examples of types? Sorry, I suppose this means that I missed the main point of "meaning explanation". But maybe that point could be made more explicitly. (?)

   Hm, looking at the entry meaning explanation, I get away with the impression that all it says is that

   “If something computes to something that behaves like a certain type, then it is of that certain type”.

   What is there more to it? What is non-trivial in saying this for various examples of types?

   Sorry, I suppose this means that I missed the main point of “meaning explanation”. But maybe that point could be made more explicitly. (?)

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeDec 2nd 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOne thing that I guess is worth mentioning is that since you start from an untyped notion of computation, there are more terms assigned to a type than in the usual rules of type theory. For instance, maybe $(\lambda x. 0)\Omega$ computes to $0$, and hence has type $N$, regardless of whether $\Omega$ is even well-typed. However, you're not the only one who is confused about the point of this. I'm in the middle of a discussion with Peter Dybjer and Bob Harper about it; so far I gather that it is regarded as a "pre-mathematical" or "philosophical" explanation of why the rules of type theory are what they are. I don't really get the point either, though.

   One thing that I guess is worth mentioning is that since you start from an untyped notion of computation, there are more terms assigned to a type than in the usual rules of type theory. For instance, maybe $(\lambda x. 0)\Omega$ computes to $0$, and hence has type $N$, regardless of whether $\Omega$ is even well-typed.

   However, you’re not the only one who is confused about the point of this. I’m in the middle of a discussion with Peter Dybjer and Bob Harper about it; so far I gather that it is regarded as a “pre-mathematical” or “philosophical” explanation of why the rules of type theory are what they are. I don’t really get the point either, though.

10. • CommentRowNumber10.
    • CommentAuthorStephan A Spahn
    • CommentTimeDec 3rd 2012
    • PermaLink
    Author: Stephan A Spahn
    Format: MarkdownItexTo me it is not clear why $z_s(g,\underline{1},z_s(\underline{0},z_0))$ is not written $z_s(g,\underline{1},z_s(g,\underline{0},z_0))$.

    To me it is not clear why $z_s(g,\underline{1},z_s(\underline{0},z_0))$ is not written $z_s(g,\underline{1},z_s(g,\underline{0},z_0))$.

11. • CommentRowNumber11.
    • CommentAuthorjcmckeown
    • CommentTimeDec 3rd 2012
    • PermaLink
    Author: jcmckeown
    Format: MarkdownItex@Stephen: Probably because Toby is a real human; or else the program playing Toby has a subtle fencepost error.

    @Stephen: Probably because Toby is a real human; or else the program playing Toby has a subtle fencepost error.

12. • CommentRowNumber12.
    • CommentAuthorStephan A Spahn
    • CommentTimeDec 3rd 2012
    • PermaLink
    Author: Stephan A Spahn
    Format: MarkdownItex> subtle fencepost error Oh, I expected a subtle meaning - or rather a subtle meaning explanation.:)

    subtle fencepost error

    Oh, I expected a subtle meaning - or rather a subtle meaning explanation.:)

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeDec 3rd 2012
    • (edited Dec 3rd 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexOn [p. 25 here](http://www.cse.chalmers.se/~peterd/slides/Luminy-talk-2012-02-16.pdf#page=25) Peter Dybjer paraphrases Martin-Löf as saying > Some people feel that when I have presented my meaning explanations I have said nothing. And this is how it should be. The standard semantics should be just that: standard. It should come as no surprise. > ( Martin-Löf at the Types Summer School in Giens 2002 (as I [Peter Dybjer] recall it) )

    On p. 25 here Peter Dybjer paraphrases Martin-Löf as saying

    Some people feel that when I have presented my meaning explanations I have said nothing. And this is how it should be. The standard semantics should be just that: standard. It should come as no surprise.

    ( Martin-Löf at the Types Summer School in Giens 2002 (as I [Peter Dybjer] recall it) )

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeDec 3rd 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI added that quote, and clarified the natural numbers type. I think the conclusion of my discussions with the type theorists is that there is a mathematical component, which can be regarded as a realizability model, and then also a philosophical component, which I don't understand and probably never will.

    I added that quote, and clarified the natural numbers type. I think the conclusion of my discussions with the type theorists is that there is a mathematical component, which can be regarded as a realizability model, and then also a philosophical component, which I don’t understand and probably never will.

15. • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeDec 3rd 2012
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexOr the program implementing me (I would not say ‘playing’) has subtle errors deliberately introduced to help pass Turing tests.

    Or the program implementing me (I would not say ‘playing’) has subtle errors deliberately introduced to help pass Turing tests.

16. • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeDec 3rd 2012
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex@Mike #7 re first footnote #5: Normally I see people say things like ‹Let $z_s$ be a term (of this type) with these free variables (of these types).›; but in this raw context, I agree that (besides not specifying the types ahead of time) it's nice to put it all directly into the syntax.

    @Mike #7 re first footnote #5: Normally I see people say things like ‹Let $z_s$ be a term (of this type) with these free variables (of these types).›; but in this raw context, I agree that (besides not specifying the types ahead of time) it’s nice to put it all directly into the syntax.

17. • CommentRowNumber17.
    • CommentAuthorTobyBartels
    • CommentTimeDec 3rd 2012
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexI moved the page back to a singular name, in accordance with the naming conventions, but the text still refers to multiple meaning explanations.

    I moved the page back to a singular name, in accordance with the naming conventions, but the text still refers to multiple meaning explanations.

18. • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 3rd 2016
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI just read the email discussion linked to at [uf-ias-2012](http://uf-ias-2012.wikispaces.com/Meaning+Explanations), and find myself perfectly in agreement with Mike. A view of philosophy which would pin down one correct way of seeing things is so enormously implausible in the context of the long course of human inquiry. I'd much rather it make its contribution by providing occasional fresh insights to be fed into the mix. On the other hand, I suppose some people wouldn't be motivated to do their work if they didn't believe they were on the one true path.

    I just read the email discussion linked to at uf-ias-2012, and find myself perfectly in agreement with Mike. A view of philosophy which would pin down one correct way of seeing things is so enormously implausible in the context of the long course of human inquiry. I’d much rather it make its contribution by providing occasional fresh insights to be fed into the mix. On the other hand, I suppose some people wouldn’t be motivated to do their work if they didn’t believe they were on the one true path.

19. • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeMay 3rd 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRereading that email discussion again myself, I find myself astonished at how much energy and time I had for conversations like that three years ago. (-:

    Rereading that email discussion again myself, I find myself astonished at how much energy and time I had for conversations like that three years ago. (-:

20. • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 3rd 2016
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexJust see yourself as playing the role of Hilbert in the Hilbert-Frege (or Brouwer or Weyl) discussions. If he thought it worth the energy and time, why not you?

    Just see yourself as playing the role of Hilbert in the Hilbert-Frege (or Brouwer or Weyl) discussions. If he thought it worth the energy and time, why not you?

21. • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeMay 3rd 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhether it's worth the energy and time is a different question from whether I have that energy and time available... (-:

    Whether it’s worth the energy and time is a different question from whether I have that energy and time available… (-:

22. • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 4th 2016
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI see the search continues for a meaning explanation of higher type theory, in [arXiv:1604.08873](https://arxiv.org/abs/1604.08873), and then a constructive understanding of univalence in [Cubical Type Theory: a constructive interpretation of the univalence axiom](https://www.math.ias.edu/~amortberg/papers/cubicaltt.pdf).

    I see the search continues for a meaning explanation of higher type theory, in arXiv:1604.08873, and then a constructive understanding of univalence in Cubical Type Theory: a constructive interpretation of the univalence axiom.

23. • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 16th 2017
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI added * Jonathan Sterling, Type theory and its meaning explanations, ([pdf](http://www.jonmsterling.com/pdfs/meaning-explanations.pdf))

    I added

    • Jonathan Sterling, Type theory and its meaning explanations, (pdf)
24. • CommentRowNumber24.
    • CommentAuthorjonsterling
    • CommentTimeOct 17th 2017
    • PermaLink
    Author: jonsterling
    Format: MarkdownItexI would like to propose that we remove the link to the video of my talk, "Type theory and its meaning explanations"; the talk contains a serious error in the definition of `functionality'/sequents, which is corrected in the notes that David has just added. Are people OK with that?

    I would like to propose that we remove the link to the video of my talk, “Type theory and its meaning explanations”; the talk contains a serious error in the definition of ‘functionality’/sequents, which is corrected in the notes that David has just added.

    Are people OK with that?

25. • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeOct 17th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexIf you prefer you should remove it. But might the topic better be served if you leave it there and add a quick remark to the link regarding the error and how to fix it?

    If you prefer you should remove it. But might the topic better be served if you leave it there and add a quick remark to the link regarding the error and how to fix it?

26. • CommentRowNumber26.
    • CommentAuthorjonsterling
    • CommentTimeOct 17th 2017
    • (edited Oct 17th 2017)
    • PermaLink
    Author: jonsterling
    Format: MarkdownItexHi Urs, I have just added a note to that link saying that the explanation of functionality is incorrect, but that it is fixed in the notes that are also linked.

    Hi Urs, I have just added a note to that link saying that the explanation of functionality is incorrect, but that it is fixed in the notes that are also linked.

27. • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeOct 17th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks. I have edited the formatting slightly: [here](https://ncatlab.org/nlab/show/meaning+explanation#Sterling15)

    Thanks. I have edited the formatting slightly: here

28. • CommentRowNumber28.
    • CommentAuthorjonsterling
    • CommentTimeOct 17th 2017
    • PermaLink
    Author: jonsterling
    Format: MarkdownItexThank you, Urs!

    Thank you, Urs!

29. • CommentRowNumber29.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 17th 2017
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexI changed the YouTube link to point to just Jon's video, rather than including also the playlist information that was in the previous link.

    I changed the YouTube link to point to just Jon’s video, rather than including also the playlist information that was in the previous link.

30. • CommentRowNumber30.
    • CommentAuthoratmacen
    • CommentTimeApr 14th 2019
    • PermaLink
    Author: atmacen
    Format: TextSay, this explanation of function types isn’t right is it? It’s not enforcing that they respect equality.

    Say, this explanation of function types isn’t right is it? It’s not enforcing that they respect equality.
31. • CommentRowNumber31.
    • CommentAuthorjonsterling
    • CommentTimeApr 14th 2019
    • PermaLink
    Author: jonsterling
    Format: MarkdownItexYes, the explanation of function types seems incorrect. I'm having trouble reading it because the changes to the style changes have resulted in some bizarre effects (gigantic text mixed with small text, all very closely spaced together), but from what I can tell, the definitions in the page need a lot of corrections. If I were not stuck between a bunch of deadlines right now, I would make some corrective changes to the page.

    Yes, the explanation of function types seems incorrect. I’m having trouble reading it because the changes to the style changes have resulted in some bizarre effects (gigantic text mixed with small text, all very closely spaced together), but from what I can tell, the definitions in the page need a lot of corrections. If I were not stuck between a bunch of deadlines right now, I would make some corrective changes to the page.

32. • CommentRowNumber32.
    • CommentAuthoratmacen
    • CommentTimeApr 14th 2019
    • PermaLink
    Author: atmacen
    Format: MarkdownItexWell, I think I fixed the issue of functions respecting equality, anyway. <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/19">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/19">v19</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    Well, I think I fixed the issue of functions respecting equality, anyway.

    diff, v19, current

33. • CommentRowNumber33.
    • CommentAuthoratmacen
    • CommentTimeApr 15th 2019
    • PermaLink
    Author: atmacen
    Format: MarkdownItexChanges to wording that I think are less misleading. For example: "equal terms" -> "equal elements"; certainly they need not be syntactically equal. <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/20">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/20">v20</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    Changes to wording that I think are less misleading. For example: “equal terms” -> “equal elements”; certainly they need not be syntactically equal.

    diff, v20, current

34. • CommentRowNumber34.
    • CommentAuthoratmacen
    • CommentTimeApr 15th 2019
    • PermaLink
    Author: atmacen
    Format: MarkdownItexClarified the way the inductive judgments for Nat elements are separate from the overall induction-recursion. <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/21">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/21">v21</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    Clarified the way the inductive judgments for Nat elements are separate from the overall induction-recursion.

    diff, v21, current

35. • CommentRowNumber35.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 15th 2019
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex@Jon should the link to your meaning explanations notes (which is broken, and the pdf doesn't appear to be in your GH repo for your webpage) point to <https://arxiv.org/abs/1512.01837>?

    @Jon

    should the link to your meaning explanations notes (which is broken, and the pdf doesn’t appear to be in your GH repo for your webpage) point to https://arxiv.org/abs/1512.01837?

36. • CommentRowNumber36.
    • CommentAuthoratmacen
    • CommentTimeApr 15th 2019
    • PermaLink
    Author: atmacen
    Format: MarkdownItexClarification about what aspects of the explanation for identity types gets UIP vs equality reflection. <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/22">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/22">v22</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    Clarification about what aspects of the explanation for identity types gets UIP vs equality reflection.

    diff, v22, current

37. • CommentRowNumber37.
    • CommentAuthoratmacen
    • CommentTimeApr 15th 2019
    • PermaLink
    Author: atmacen
    Format: MarkdownItexCorrections to reduction rules. This is big-step reduction; you need premises. There should probably be a section explaining the operational setup. <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/23">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/23">v23</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    Corrections to reduction rules. This is big-step reduction; you need premises. There should probably be a section explaining the operational setup.

    diff, v23, current

38. • CommentRowNumber38.
    • CommentAuthoratmacen
    • CommentTimeApr 15th 2019
    • PermaLink
    Author: atmacen
    Format: MarkdownItexPut in some stuff about properties this meaning explanation should satisfy and why. <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/24">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/24">v24</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    Put in some stuff about properties this meaning explanation should satisfy and why.

    diff, v24, current

39. • CommentRowNumber39.
    • CommentAuthoratmacen
    • CommentTimeApr 15th 2019
    • PermaLink
    Author: atmacen
    Format: MarkdownItexUpdated/rearranged pedagogical commentary about why this is mutual inductive-recursive. <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/25">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/25">v25</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    Updated/rearranged pedagogical commentary about why this is mutual inductive-recursive.

    diff, v25, current

40. • CommentRowNumber40.
    • CommentAuthorUrs
    • CommentTimeApr 15th 2019
    • (edited Apr 15th 2019)
    • PermaLink
    Author: Urs
    Format: MarkdownItexmade more of the keywords in the first sentences be hyperlinked <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/26">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/26">v26</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    made more of the keywords in the first sentences be hyperlinked

    diff, v26, current

41. • CommentRowNumber41.
    • CommentAuthoratmacen
    • CommentTimeApr 16th 2019
    • PermaLink
    Author: atmacen
    Format: MarkdownItexPerfunctory mention of type equality and hypothetical judgements. <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/27">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/27">v27</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    Perfunctory mention of type equality and hypothetical judgements.

    diff, v27, current

42. • CommentRowNumber42.
    • CommentAuthorjonsterling
    • CommentTimeApr 16th 2019
    • PermaLink
    Author: jonsterling
    Format: MarkdownItexHi all, I wanted to remove the links to my presentation and notes from this page, but I felt I should consult the forum. I don't feel that the notes are in bad shape in a technical sense, but I no longer subscribe to the point of view which I was expressing in those notes, and feel that it might be misleading to people who reach them from this page. The technical material in the note is of course correct and fine as far as I am aware, but the ethos is a bit odious. Can we let other references, such as the works of Per, stand for themselves?

    Hi all, I wanted to remove the links to my presentation and notes from this page, but I felt I should consult the forum.

    I don’t feel that the notes are in bad shape in a technical sense, but I no longer subscribe to the point of view which I was expressing in those notes, and feel that it might be misleading to people who reach them from this page. The technical material in the note is of course correct and fine as far as I am aware, but the ethos is a bit odious. Can we let other references, such as the works of Per, stand for themselves?

43. • CommentRowNumber43.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 17th 2019
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexSure, but I think the video has some merit despite the mistake, in that I've not seen another presentation on it in that style I found it helpful.

    Sure, but I think the video has some merit despite the mistake, in that I’ve not seen another presentation on it in that style I found it helpful.

44. • CommentRowNumber44.
    • CommentAuthorjonsterling
    • CommentTimeApr 17th 2019
    • (edited Apr 17th 2019)
    • PermaLink
    Author: jonsterling
    Format: MarkdownItexHi David, thank you for your comment! By the way, I am too concerned about the error in the presentation, because it is corrected in the notes --- my main concern is that the ethos presented is naive and may lead people down an unnecessary rabbit hole. I wish I could say more at the moment, but let me be a bit mysterious and say that after spending a lot of time working on it, I am skeptical of the notion of 'meaning explanation' as a scientific discipline which can tell the difference between correct and incorrect versions of type theory. I felt I was a bit overzealous in promoting it, and perhaps made stronger claims than Per intended in his own work.

    Hi David, thank you for your comment! By the way, I am too concerned about the error in the presentation, because it is corrected in the notes — my main concern is that the ethos presented is naive and may lead people down an unnecessary rabbit hole. I wish I could say more at the moment, but let me be a bit mysterious and say that after spending a lot of time working on it, I am skeptical of the notion of ’meaning explanation’ as a scientific discipline which can tell the difference between correct and incorrect versions of type theory. I felt I was a bit overzealous in promoting it, and perhaps made stronger claims than Per intended in his own work.

45. • CommentRowNumber45.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 17th 2019
    • (edited Apr 17th 2019)
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexAh, ok. I should go have a (re)read of Martin-Löf's original treatment. Is the referenced article ("Constructive mathematics and computer programming") the only place? Also, the link to the IAS special year wiki needs updating!

    Ah, ok. I should go have a (re)read of Martin-Löf’s original treatment. Is the referenced article (“Constructive mathematics and computer programming”) the only place?

    Also, the link to the IAS special year wiki needs updating!

46. • CommentRowNumber46.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 17th 2019
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexUpdated the link to the IAS2012 wiki to point to the archived version, and added reference to Martin-Löf's _On the Meanings of the Logical Constants and the Justifications of the Logical Laws_. <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/28">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/28">v28</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    Updated the link to the IAS2012 wiki to point to the archived version, and added reference to Martin-Löf’s On the Meanings of the Logical Constants and the Justifications of the Logical Laws.

    diff, v28, current

47. • CommentRowNumber47.
    • CommentAuthorjonsterling
    • CommentTimeApr 17th 2019
    • PermaLink
    Author: jonsterling
    Format: MarkdownItexHi David, Per has also propounded the meaning explanation of his type theory in his subsequent monograph, Intuitionistic Type Theory (what some call the "Bibliopolis book"): http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf

    Hi David, Per has also propounded the meaning explanation of his type theory in his subsequent monograph, Intuitionistic Type Theory (what some call the “Bibliopolis book”): http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf

48. • CommentRowNumber48.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 18th 2019
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex@Jon, thanks, I've added it. Some words around how these different texts relate would be good, but I'm not confident in getting it right, since I know there are subtle changes over time in Martin-Löf's work.

    @Jon,

    thanks, I’ve added it. Some words around how these different texts relate would be good, but I’m not confident in getting it right, since I know there are subtle changes over time in Martin-Löf’s work.

49. • CommentRowNumber49.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 18th 2019
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexAdded the Bibliopolis book reference <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/29">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/29">v29</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    Added the Bibliopolis book reference

    diff, v29, current

50. • CommentRowNumber50.
    • CommentAuthoratmacen
    • CommentTimeApr 18th 2019
    • (edited Apr 18th 2019)
    • PermaLink
    Author: atmacen
    Format: MarkdownItexJustification for my weird reflexivity property. Discussion of how this function type differs from Martin-Löf's. Finally noticed mistake where the function type clause didn't use $C$ when it should. <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/30">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/30">v30</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    Justification for my weird reflexivity property. Discussion of how this function type differs from Martin-Löf’s. Finally noticed mistake where the function type clause didn’t use $C$ when it should.

    diff, v30, current

51. • CommentRowNumber51.
    • CommentAuthorjonsterling
    • CommentTimeApr 18th 2019
    • PermaLink
    Author: jonsterling
    Format: MarkdownItexRemoved the links to my notes & presentation, as I proposed in the n-forum thread. At some point within the next month or so, I also intend to update this page with a brief map to through the literature --- as PML's views on the topic have evolved, and without a guide, it can be hard to understand the history of these ideas. <a href="https://ncatlab.org/nlab/revision/diff/meaning+explanation/31">diff</a>, <a href="https://ncatlab.org/nlab/revision/meaning+explanation/31">v31</a>, <a href="https://ncatlab.org/nlab/show/meaning+explanation">current</a>

    Removed the links to my notes & presentation, as I proposed in the n-forum thread. At some point within the next month or so, I also intend to update this page with a brief map to through the literature — as PML’s views on the topic have evolved, and without a guide, it can be hard to understand the history of these ideas.

    diff, v31, current

52. • CommentRowNumber52.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 18th 2019
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexThanks, Jon!

    Thanks, Jon!