Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Excellent; thank you Urs. The articles on homotopy type theory are coming along nicely.
Thanks for the feedback, Todd!
I still have a bunch of gaps in my understanding, but I feel I am finally picking up some speed here.
One dumb question: when we say “type theory is the internal language of locally cartesian closed categories”, should we not more precisely be adding some clause about existence/non-existence of inductive types/colimits? I mean, a general locally cartesian closed category won’t have colimits, so much of type theory that we are talking about does not actually have a model in it.
What’s the language convention here?
I don’t know, Urs, because my gaps are even greater. I have been putting off until only very recently learning about dependent type theory, and I have some questions, too.
In the article Martin-Löf dependent type theory, I see a bunch of rules for judgments of type formations, corresponding roughly to what one might call (unfortunately but traditionally) “logical rules”, and one question I have is: where are the corresponding structural rules? For example, one might expect to see a “weakening” rule
which would be interpreted in a locally cartesian closed category by pulling back along a projection . I do see partial instances of this rule, as for example in the statement, “For any context , if is an atomic type, ,” and which could be derived by applying weakening:
Similarly, what about contraction and exchange rules?
@Urs: we should not say “type theory is the internal language of locally cartesian closed categories”. There are many different kinds of type theory, containing many different constructions and rules. One particular one of those type theories (at least) may be called the internal language of locally cartesian closed categories, but all sorts of other categories with more or less structure also have internal logics that are different type theories, and there are also type theories that aren’t so closely related to categories at all.
@Todd: I believe that in the presentation at that page, the weakening, contraction, and exchange rules are theorems. The special case of weakening for atomic types is the base case of an inductive proof of weakening for all judgments, which goes through because all the rules allow an arbitrary context to be present.
Mike,
okay, that’s what I was thinking (well, I meant to say dependent type theory. ). But then I see people say “dependent type theory is the internal language of locally cartesian closed categories”.
For instance Joyal does essentially that on p. 19 of the OW report.
When I look around I seem to see lots of authors use language this way. Martin Hofman has an article titled “On the Interpretation of Type Theory in Locally Cartesian Closed Categories”. and the first sentence of the abstract right away states
We show how to construct a model of dependent type theory (category with attributes) from a locally cartesian closed category.
Ok, I see what you’re saying. While I’ve learned a fair amount of type theory, I still don’t fully “speak type-theorist”. I agree that we should be more precise, even if type theorists can say such things and know what they mean. I think probably the best way to do that is by explicitly listing the type constructors we have, e.g. “dependent type theory with dependent sums and dependent products – perhaps also with extensional identity types – is the internal logic of a lccc”.
Definitely we’ll want extensional identity types in the type theory corresponding precisely to the internal logic of a plain lccc, no?; otherwise (if we don’t intend to have to have extensional identity types), we’ll need to distinguish between arbitrary slices and those particular slices representing dependent types, which means we’ll need more structure than just an lccc (we’ll need a specified pullback stable, etc., class of “display maps”). The nice thing about having the combination of extensional identity types and dependent sums is that we no longer need any extra information on top of our category of closed types in order to describe dependent types; all the extra structure becomes redundant in their presence.
I’m still trying to understand what’s going on, so let me throw out a naive question. If we have a dependent type theory with extensional identity types, then is it reasonable to say that the “term model” it freely generates can be described as a hyperdoctrine
where is a suitable category of contexts, the functor takes each object to a category of “display maps” over , and each is assumed to have left and right adjoints obeying some Beck-Chevalley conditions? Or what would be the right thing to say?
@Sridhar: It’s not obvious to me that there is a unique internal logic for a given kind of category. Certainly, extensional identity types make the internal logic of a lccc more convenient, and match the category theory more closely. But just because DTT without identity types also admits models more general than lcccs, that doesn’t mean we can’t still think of it as an internal logic for lcccs.
@Todd: That’s the right track, but I think there’s a bit more structure that people usually include: the hyperdoctrine of display maps comes with a map to the codomain fibration, so that each display map “is” actually a map in the category as well. (Hmm, maybe this can be constructed out of left adjoints to ?) There are various different structures called things like “category with attributes” and “contextual category” depending on things like whether this map is fully faithful or not. Unfortunately this is one part of type theory that I haven’t fully understood yet either; I usually only think about the models in plain categories and the term models of that sort.
@Mike: Well, sure, DTT without identity types describes valid reasoning inside lcccs. But that’s just because DTT without identity types is a part of DTT with identity types. I wouldn’t want to say DTT without identity types is the internal logic of lcccs; I’d want to say DTT without identity types is part of the internal logic of lcccs.
That is, the sense in which I was thinking of the term “internal logic” is that quite often there is a correspondence (morally an equivalence) where any theory in the framework of such-and-such a logic is represented by a corresponding algebraic/categorical structure of such-and-such a sort, and vice versa, such that the definition of either (the system of logic or the flavor of categorical structure) makes clear* a definition of the other, and the study of the categorical structures is precisely the same as the “presentation-free” study of the logic’s theories. E.g., my advisor first defined “topos” to me as “a category whose objects and morphisms are the predicates and functional relations of a theory in intuitionistic higher-order logic”. Knowing what the logic was told me precisely what the categorical structure was (though of course it took time to appreciate that the same structure could be defined much more compactly in terms of a few universal properties, with less direct accounting for the logical interest).
[*Well, there’s usually a little room for decisions about what ought be implicitly taken as ignorable “presentation” and what must be preserved, but brushing over that for now…]
In some sense, the study of cartesian closed categories and the study of equational theories in the typed lambda calculus (with tupling) are exactly the same thing. In some sense, the study of categories with products and the study of algebraic theories are the exact same thing. And so on. That “exact same thing”-ness is my model for how to think of the “internal logic” associated to a category; of course, one can use lambda calculus to reason about topoi, or propositional intuitionistic logic to reason about Boolean algebras, or such things, but this is simply because topoi are among other things cartesian closed categories and Boolean algebras are among other things Heyting algebras, and so on. It seems useful to me, though, to be able to note the more precise correspondences between logics and their algebraizations, and then describe such relationships as “Lambda calculus is the internal logic of cccs, IHOL is the internal logic of topoi, and lambda calculus is part of IHOL/topoi are special cccs”. So… that’s how I think about it.
Fair enough. My #10 was a bad example. I think what I originally had in mind is that there may not be a unique “maximally good” internal logic for a given kind of category (or, conversely, a maximally good kind of category for interpreting a given type theory in). The internal logic of a topos, for instance, can be presented in many different ways; it could be a dependent type theory with a type of propositions, or the Mitchell-Benabou language, or a two-level non-dependent type theory with types and propositions as separate entities. The internal language of an lccc could also be two-level, putting equalities into the logic rather than building them into the DTT as identity types.
Sure, although I think I’d want to ultimately say all those ostensibly different logics are really the same logic, just presented differently (just as, for most purposes, Boolean logic axiomatized with the Sheffer stroke would be considered the same as Boolean logic axiomatized with OR and NOT, or such things). [Though this amounts to a tautology, since my criterion for “Do I want to consider these to be alternative presentations of the same logic?” ends up being something like “Do I want to consider these to be modelled by the same algebraic structure?”]. Anyway, we’re on the same page now.
we’re on the same page now.
Maybe some reflection of elements of this exchange could be turned into some paragraphs to be included in the relevant Lab etries?
I’ve added stuff to locally cartesian closed (infinity,1)-category and Cisinski model category and right proper model category from the blog discussion. I should link them with locally cartesian closed model category too, but I have to run.
Okay, now linked a bit.
Certainly the projective and injective model structures on simplicial presheaves are Quillen equivalent. There is discussion of this at model structure on functors and at model structure on simplicial presheaves.
I’d suggest to replace the query box in the entry with a numered remark saying something like “Notice that the projective and injective model structures are Quillen equivalent”, if it is felt that this is a piece of information that should be recalled here.
How detailed/precise has anyone made the -version of the theorem that there is an equivalence of 2-categories between locally Cartesian closed categories and ML dependent type theories?
I am aware, as we discussed, that every locally cartesian closed -category has a model category presentation such that the internal type theory of the model category is homotopy type theory without, possibly, univalence. Has anyone gone further than this?
Such as to state an equivalence of -categories between locally cartesian closed -categories and HoTTs without univalence? Probably not, or I would have heard of it, I suppose. But anything roughly in this direction?
I think this is a major open problem in HoTT.
Okay, thanks for the information.
A related question: what might be a good way to cite the insight on the nLab page which involves that discussion with Denis-Charles Cisinski? Do you later state this in one of your articles?
(I mean specifically the insight that gave rise to the original nLab note which involved Denis-Charles’s comment, not the later independent discussions of this point.)
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.
Okay, thanks.
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.
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.
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.
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 -categories.
Nice! Did you really mean to say “presentable” though? That doesn’t seem like it can possibly be right.
As in HTT, “presentable” is meant to mean “locally presentable”. Is that what you are concerned about?
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.
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.
Yes, that’s what I meant.
Added pointer Kapulkin 14 (the video-taped talk on the result still to be made public)
added also pointer to the preprint corresponding to #34, available as of recently:
And I see that meanwhile Peter Lumsdaine had already edited in the statement itself here.
I added a sentence pointing out that initiality of the syntactic -category is also a central open question.
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 -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 -equivalence between homotopy type theories and locally Cartesian closed -categories.
I tried to clarify the page.
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?
Yes, I agree. Isn’t that still a Cisinski model category, though?
One needs an argument that the -enriched functors on an -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.
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.
Thanks. Could you add a quick note to this effect there?
Sure, done.
where it said
…nothing is yet known about the initiality of this syntactic -category…
I have reworded to
…the initiality of this syntactic -category is subtle (see at initiality conjecture)…
1 to 46 of 46