where it said

…nothing is yet known about the

initialityof this syntactic $(\infty,1)$-category…

I have reworded to

]]>…the

initialityof this syntactic $(\infty,1)$-category is subtle (see atinitiality conjecture)…

updated the remark (here) on existence of univalent universes

]]>Sure, done.

]]>Thanks. Could you add a quick note to this effect there?

]]>One way to see it is to identify sSet-enriched categories with particular sSet-internal categories, which preserves the notion of sSet-diagram on such a category. Then use the fact that internal diagrams on any internal category in a topos are again a topos.

]]>One needs an argument that the $sSet$-enriched functors on an $sSet$-category still form a 1-topos. Is that obvious? I didn’t really think about this before, until Ulrik Buchholtz just queried me. He says that on this point Gepner and Kock point to Thm. 6.5 in Barr-Wells, while there may be another argument using Thm. 4.46 in Johnstone’77. I don’t have time to check right now, but we should add some remark to the entry.

]]>Yes, I agree. Isn’t that still a Cisinski model category, though?

]]>In the presentation theorem, the last item 5 speaks of model structures on simplicial presheaves. But more precisely I suppose it needs to speak of the model structure on sSet-enriched presheaves over some sSet-site. No? Does that then still imply item 4?

]]>I tried to clarify the page.

]]>The initiality that you refer to is that within the category of models over a fixed theory, right? If so, that remark should maybe not appear to be as a comment to Chris’s theorem, since in Chris’ article theories never appear except in the form of their categorical models. What he shows is that given a category that deserves to be called a 1-categorical model of type theory, then its simplicial localization is a certain $\infty$-category.

Also, personally, I wouldn’t have used Peter Lumsdaine’s term “mismatch” in the same paraghraph below the statement of Chris’s theorem. This sounds as if something is at odds, while really everything is consistent, just incompletely known.

In view of the well established results about the relation between extensional type theory and 1-category theory, the due comment to me made at the bottom of that subsection seems to me to be something referring to the ultimate goal of an $(\infty,2)$-equivalence between homotopy type theories and locally Cartesian closed $\infty$-categories.

]]>I added a sentence pointing out that initiality of the syntactic $(\infty,1)$-category is also a central open question.

]]>added also pointer to the preprint corresponding to #34, available as of recently:

- Chris Kapulkin,
*Locally Cartesian Closed Quasicategories from Type Theory*(arXiv:1507.02648)

And I see that meanwhile Peter Lumsdaine had already edited in the statement itself here.

]]>Added pointer Kapulkin 14 (the video-taped talk on the result still to be made public)

]]>Yes, that’s what I meant.

]]>Oh, I see, you mean in the converse statement that I said Chris is close to showing? Right, there probably it shouldn’t be there. My fault.

]]>My first impression is also that “(locally) presentable” shouldn’t be there. There’s nothing on the type theory side that suggests (externally-indexed) filtered colimits exist.

]]>As in HTT, “presentable” is meant to mean “locally presentable”. Is that what you are concerned about?

]]>Nice! Did you really mean to say “presentable” though? That doesn’t seem like it can possibly be right.

]]>By the way, I have talked to Chris Kapukin about this, and he says that in his thesis work he is now pretty close to showing an equivalence between fibration categories of contexts of homotopy type theories and locally cartesian closed presentable $\infty$-categories.

]]>Okay, good.

I noticed now that also on nLab no entry actually said this clearly.

I have now added something more explicit here at “locally cartesian closed infinity-category” and added something like this also to

homotopy type theory (in the section on models)

All this could be expanded on a good bit even with the available knowledge. But I don’t have more leisure for this right now.

]]>Well, it might help if Peter and Michael would finish writing their paper. Not that I should throw stones since Peter and I haven’t written our HITs paper yet either.

]]>Added a pointer to your artciel to the nLab entry.

Judging from various discussions here at at the HoTT meeting at CRM, this fact is not yet widely appreciated yet at all.

]]>Okay, thanks.

]]>In 1307.6248 I wrote

]]>Most aspects of type theory aside from univalence (e.g. Σ-types, Π-types, and identity types) are now known to admit models in all (∞, 1)-toposes, and indeed in all locally presentable, locally cartesian closed (∞, 1)-categories. By the coherence theorem of [LW13], it suffices to present such an (∞, 1)-category by a “type-theoretic model category” in the sense of [Shu12], such as a right proper Cininski model category [Cis02,Cis06]. That this is always possible has been proven by Cisinski [Cis12] and by Gepner–Kock [GK12].

[Cis12] Denis-Charles Cisinski. Blog comment on post “The mysterious nature of right properness”. http://golem.ph.utexas.edu/category/2012/05/the_mysterious_nature_of_right.html#c041306, May 2012.

[GK12] David Gepner and Joachim Kock. Univalence in locally cartesian closed ∞-categories. arXiv:1208.1749, 2012.