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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum 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 sheaves 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.
   • CommentAuthorDavid_Corfield
   • CommentTimeMar 11th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI see that from 15 March Dropbox is no longer going to allow a publicly accessible folder. So I was thinking of uploading some files to my personal web here, but when trying to edit the max size of file, realized I don't have the system password. Is there one for each personal web, or a master one?

   I see that from 15 March Dropbox is no longer going to allow a publicly accessible folder. So I was thinking of uploading some files to my personal web here, but when trying to edit the max size of file, realized I don’t have the system password. Is there one for each personal web, or a master one?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeMar 11th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThere's a master one. I knew it at one point, but I'm not sure whether I still do. A bit of googling suggests that maybe you can still create "public links" to individual files in dropbox folders? <https://www.dropbox.com/help/167>

   There’s a master one. I knew it at one point, but I’m not sure whether I still do.

   A bit of googling suggests that maybe you can still create “public links” to individual files in dropbox folders? https://www.dropbox.com/help/167

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeMar 11th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI see, thanks. Well if the address of the public link changes to my 'Expressing the Structure' paper, which you kindly cite in your latest paper, I'll let you know.

   I see, thanks. Well if the address of the public link changes to my ’Expressing the Structure’ paper, which you kindly cite in your latest paper, I’ll let you know.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeMar 11th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexIf you want a more stable URL for me to cite, you could make a wikipage for the paper on your personal web that contains a link to wherever the current PDF is.

   If you want a more stable URL for me to cite, you could make a wikipage for the paper on your personal web that contains a link to wherever the current PDF is.

5. • CommentRowNumber5.
   • CommentAuthorDavid_Corfield
   • CommentTimeMar 13th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexGood idea. So here is such a wikipage link: https://ncatlab.org/davidcorfield/show/Expressing+%27The+Structure+of%27+in+Homotopy+Type+Theory By the way, I posted a comment at the Cafe about your article. A couple of very minor things: >and also more novel synthetic mathematics using of nonclassical structure I'm struggling with the grammar. The reference [102] ... Cambridge, 2015, still not out yet. Hopefully this year.

   Good idea. So here is such a wikipage link: https://ncatlab.org/davidcorfield/show/Expressing+%27The+Structure+of%27+in+Homotopy+Type+Theory

   By the way, I posted a comment at the Cafe about your article.

   A couple of very minor things:

   and also more novel synthetic mathematics using of nonclassical structure I’m struggling with the grammar.

   The reference [102] … Cambridge, 2015, still not out yet. Hopefully this year.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeMar 13th 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexDavid, sorry for the slow reaction. I have increased the upload size maximum on your web. Please check if it works now.

   David,

   sorry for the slow reaction. I have increased the upload size maximum on your web. Please check if it works now.

7. • CommentRowNumber7.
   • CommentAuthorTobyBartels
   • CommentTimeMar 13th 2017
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItex<https://ncatlab.org/davidcorfield/show/Expressing+%27The+Structure+of%27+in+Homotopy+Type+Theory>

   https://ncatlab.org/davidcorfield/show/Expressing+%27The+Structure+of%27+in+Homotopy+Type+Theory

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeMar 13th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexGreat thanks, uploads are working now.

   Great thanks, uploads are working now.

9. • CommentRowNumber9.
   • CommentAuthorNikolajK
   • CommentTimeMar 13th 2017
   • (edited Mar 13th 2017)
   • PermaLink
   Author: NikolajK
   Format: MarkdownItex@David: There's a $:$ before the $\equiv$ on page 6 and later there isn't one. Is that right? In any case, if people don't know how the binding order of all those symbols go, I'd put that whole expression in brackets, $X:T \vdash (F(X)\equiv E(X)):T$ or write it in two lines $F(X)\equiv E(X)$ $X:T \vdash F(X):T$

   @David: There’s a $:$ before the $\equiv$ on page 6 and later there isn’t one. Is that right?

   In any case, if people don’t know how the binding order of all those symbols go, I’d put that whole expression in brackets,

   $X:T \vdash (F(X)\equiv E(X)):T$

   or write it in two lines

   $F(X)\equiv E(X)$

   $X:T \vdash F(X):T$

10. • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 13th 2017
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexThanks, Nikolaj. $: \equiv$ is meant to signal a definition, as in the HoTT book, but now I look I see they never seem to use the symbol to the right of a $\vdash$. Is that just for clarity?

    Thanks, Nikolaj.

    $: \equiv$ is meant to signal a definition, as in the HoTT book, but now I look I see they never seem to use the symbol to the right of a $\vdash$. Is that just for clarity?

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMar 14th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThanks for the fixes David. The HoTT book mostly doesn't use $\vdash$ at all, only in the appendix. But even when being more formal, I don't think I would normally use the "being defined to equal" symbol $:\equiv$ in that way, since it's not a *judgment*. Unless we're working in a type theory that has an internal notion of "definition" (which of course real-world systems like Coq and Agda do, but mathematical type theories don't usually), defining something to equal something else is a meta-theoretic shorthand rather than part of the formal system. I suppose one could say that it takes place in a context, though.

    Thanks for the fixes David.

    The HoTT book mostly doesn’t use $\vdash$ at all, only in the appendix. But even when being more formal, I don’t think I would normally use the “being defined to equal” symbol $:\equiv$ in that way, since it’s not a judgment. Unless we’re working in a type theory that has an internal notion of “definition” (which of course real-world systems like Coq and Agda do, but mathematical type theories don’t usually), defining something to equal something else is a meta-theoretic shorthand rather than part of the formal system. I suppose one could say that it takes place in a context, though.

12. • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 14th 2017
    • (edited Mar 14th 2017)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexThe final 'it' refers to defining something to equal something else? How then would you write such a definition if it takes place in a context? Perhaps verbally, e.g., >Relative to context $\Gamma$, we define $F(x,y,z) :\equiv ...$, where $x, y, z$ all appear as free variable in $\Gamma$.

    The final ’it’ refers to defining something to equal something else? How then would you write such a definition if it takes place in a context? Perhaps verbally, e.g.,

    Relative to context $\Gamma$, we define $F(x,y,z) :\equiv ...$,

    where $x, y, z$ all appear as free variable in $\Gamma$.

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeMar 14th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexIn ordinary mathematics, which the book strives to emulate, we don't usually feel the need to mention contexts at all. If there is something currently in the context, then when we define something, it's obviously relative to that, and we might or might not notate it depending on whether the dependence matters. Ordinary mathematics also blurs the line between hypothetical judgments $x:A \vdash f_x:B$ and functions $\cdot \vdash f:A\to B$, so any time we define something in a context we might as well be just defining a function in the empty context.

    In ordinary mathematics, which the book strives to emulate, we don’t usually feel the need to mention contexts at all. If there is something currently in the context, then when we define something, it’s obviously relative to that, and we might or might not notate it depending on whether the dependence matters. Ordinary mathematics also blurs the line between hypothetical judgments $x:A \vdash f_x:B$ and functions $\cdot \vdash f:A\to B$, so any time we define something in a context we might as well be just defining a function in the empty context.

14. • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 14th 2017
    • (edited Mar 14th 2017)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexHmm, so $\vdash the: \prod_{z: (\sum_{X: Type} isContr(X))} (\pi_1(z))$? And $the \equiv \pi_1(\pi_2)$.

    Hmm, so $\vdash the: \prod_{z: (\sum_{X: Type} isContr(X))} (\pi_1(z))$? And $the \equiv \pi_1(\pi_2)$.

15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMar 14th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI suppose.

    I suppose.