Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeSep 18th 2013
   • (edited Sep 18th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexAt least to the extent that we believe it or that it has been shown, homotopy type theory is the internal language of (at least some) $\infty$-toposes. Therefore in some contexts I want to label some discussion in $\infty$-topos theory as a discussion "in homotopy type theory". I want this in an attempt to reduce possible confusion (as in: look, HoTT-audience, even if you haven't read Lurie's book, then translated to your language this just says the following...) but I see a risk of increasing confusion if my audience expects that the announcement of "discussion in homotopy type theory" is followed by computer code-style formalization. So what is the curren language convention in the homotopy type theory community for standard discussion of $\infty$-toposes? Can we call that "informal homotopy type theory"? I'd maybe rather use a different word, because what is "informal" in "informal HoTT" is what is formal for the average mathematician, while the average mathematician may think that "informal" means "heuristics without mathematical proof". What's the general feeling on this issue, if any?

   At least to the extent that we believe it or that it has been shown, homotopy type theory is the internal language of (at least some) $\infty$-toposes. Therefore in some contexts I want to label some discussion in $\infty$-topos theory as a discussion “in homotopy type theory”.

   I want this in an attempt to reduce possible confusion (as in: look, HoTT-audience, even if you haven’t read Lurie’s book, then translated to your language this just says the following…) but I see a risk of increasing confusion if my audience expects that the announcement of “discussion in homotopy type theory” is followed by computer code-style formalization.

   So what is the curren language convention in the homotopy type theory community for standard discussion of $\infty$-toposes? Can we call that “informal homotopy type theory”? I’d maybe rather use a different word, because what is “informal” in “informal HoTT” is what is formal for the average mathematician, while the average mathematician may think that “informal” means “heuristics without mathematical proof”.

   What’s the general feeling on this issue, if any?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeSep 18th 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> Therefore in some contexts I want to label some discussion in ∞-topos theory as a discussion “in homotopy type theory”. I would avoid that. We don't label discussion in ordinary topos theory as discussion "in intuitionistic higher-order logic" even though the latter is the internal language of the former. They are arguably two ways of talking about the same thing, but the phrases "∞-topos theory" and "homotopy type theory" denote the ways of talking (which are different), rather than the thing being talked about (which is the same). On the other hand, if you are actually *translating* to HoTT rather than just relabeling something written in ∞-topos theory, then personally, I would just call it "homotopy type theory". If anyone expects that to mean a computer formalization, then that's their problem, which had best be corrected as soon as possible. I would have hoped that the book made clear that homotopy type theory can be done just like ordinary mathematics, without a computer.

   Therefore in some contexts I want to label some discussion in ∞-topos theory as a discussion “in homotopy type theory”.

   I would avoid that. We don’t label discussion in ordinary topos theory as discussion “in intuitionistic higher-order logic” even though the latter is the internal language of the former. They are arguably two ways of talking about the same thing, but the phrases “∞-topos theory” and “homotopy type theory” denote the ways of talking (which are different), rather than the thing being talked about (which is the same).

   On the other hand, if you are actually translating to HoTT rather than just relabeling something written in ∞-topos theory, then personally, I would just call it “homotopy type theory”. If anyone expects that to mean a computer formalization, then that’s their problem, which had best be corrected as soon as possible. I would have hoped that the book made clear that homotopy type theory can be done just like ordinary mathematics, without a computer.