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.
Created categorical model of dependent types, describing the various different ways to strictify category theory to match type theory and their interrelatedness. I wasn’t sure what to name this page — or even whether it should be part of some other page — but I like having all these closely related structures described in the same place.
Thanks, Mike, that’s very useful.
I have added cross links with the entry categorical semantics, which is stubby, and where I had once started making some notes on the interpretation of dependent types (I was essentially taking diagrams from, I think, the appendix of Michael Warren’s thesis).
I added a few examples of universes, and also the instructive example of simple fibrations, to categorical model of dependent types.
Thanks to Kristina Sojakova, I have added to categorical model of dependent types a statement and reference for the equivalence between categories with families and categories with attributes.
There was a sentence
All of this could be made more precise by assembling the structures considered below categories, 2-categories, and/or strict 2-categories.
which seemed to be missing some word. I guess it is missing an “into” and should read
All of this could be made more precise by assembling the structures considered below into categories, 2-categories, and/or strict 2-categories.
I have changed it this way in the entry. But check.
I have been editing a bit, introducing more environements (whenever you say “Note that”, I made it a numbered Remark, etc.) and lots of internal cross-references to the numbered definitions and (now) numbered examples that are being referred to from elsewhere in the text. Also added more links. In theorem 1
appears but is currently an unsatisfied link. We really need that entry, I think.
What I was missing in the entry was a concluding statement that explicitly tells me what I have to do to my favorite locally cartesian closed category for it to actually be a strict model of its dependenty type theory.
So I have now added the follwing to the entry
+– {: .num_example #TypeTheoryModelFromLocallyCartesianClosedCategory}
For a locally cartesian closed category , it becomes a model for dependent type theory by regarding its codomain fibration as a comprehension category, def. \ref{ComprehensionCategory}, and then strictifying that as in example \ref{FromComprehensionToContextual}.
=–
I suppose one could embed this in a larger context of replacing categories by equivalent ones that have strict pullback, which is something that comes up independently of type-theoretic questions.
Generally, there seems to be a curious story here about how type theory is about not just category theory, but category theory with semi-strictification theorems applied.
It’s most notable of course for homotopy type theory. From one point of view the fact that “there is homotopy type theory” is equivalently the fact that there are “very good model categories” presenting any locally cartesian closed -category, which are so “good” that upon passing to the fibrant cofibrant objects all of homotopy theory is given by strict 1-category theory in them, with the only exception that path space objects have to be insderted every now and then.
Somehow it’s funny how the “intrinsically homotopy theoretic language” of homotopy type theory is therefore at the same time related to what from the point of view of -category theory is the very opposite of “intinsic homotopy theoretic”, as it comes with the choice of this very good model category, which even has to be “very-strictified” to a contextual 1-category.
A different but related thing that is “funny” in this sense is how the formal language of type theory, which feels like the “ultimate algebraization” of category theory, really talks about non-algebraic models of higher categories. And if one thinks about it, it’s in the term introduction rules: the term introduction rules only say that under some assumptions there is a term. They don’t tell us “which one”. Accordingly they are interpreted as non-unique lifts. At the same time, nevertheless the very existence of the type theory says that we may reason about such non-unique lifts purely and entirely algebraically in a sense (maybe not in another sense).
I am just stating the obvious, I guess. But every now and then I find this state of affairs curious, in view of all the discussion about geometric and algebraic models of higher category theory that we had elsewhere. In some nice sense both sides in this discussion find their reflection in homotopy type theory.
Intutionistic type theory has also old kind of models via pointless topology, but this topological model has very different topological features than the homotopy theoretic.
Thanks for the fixes. I think numbered remarks versus paragraph text is largely a stylistic choice; do you have some reason to prefer the one over the other? I actually prefer a bit more informal style except where necessary to single out a particular remark with a number, mainly so that it could be referred back to later.
Re #8, I feel like we’ve had this discussion before. (-: I agree, although I’ll repeat again that internally the type theory is a very algebraic sort of -groupoid; it’s just that when we come to look at categorical semantics we only know how to model it using nonalgebraic ones.
do you have some reason to prefer the one over the other?
Maybe it’s just my way of digesting a mathematical text. I don’t like more than one nontrivial idea expressed in a single technical paragraph, because that requires extra work on the reader to disentangle where one complex thought ends and the next one begins.
I am not the reader who wants to sit down and read a long mathematical text from beginning to end, like a crime novel. I want to be able to scan over it, jump right to the point that might be of interest to me, decide if it is, and if it is be able to easily work backwards from that point to those definitions and theorems that I need to absorb it.
That’s why I like lots of anchors in the text to facilitate this kind of reading. But I can understan if you say you find it too much.
Added reference
The initial category with families was constructed in
- Thorsten Altenkirch, Ambrus Kaposi, Type Theory in Type Theory using Quotient Inductive Types, (2015) (pdf), (formalisation in Adga). {#AltKap2015}
inside type theory with set quotients of higher inductive types.
This talk by Eric Finster looks interesting, and relevant:
Categories with families are an extremely useful reformulation of the syntax of dependent type theory in categorical terms. We show in this talk how using (a slight modification of) the Baez-Dolan definition of opetopic higher category, one can describe the notion of a “higher category with families” in completely a elementary, that is, syntactic way. The resulting structure may be regarded as a weakened version of type theory in which the conversion rule is rendered proof-relevant and is thus similar in spirit to the explicit substitution calculus of Curien, but here equipped with a direct higher categorical interpretation.
I find the following quote from Kapulkin-Lumsdaine 12 really useful, and so I have now added it to the Idea-section at categorical model of dependent types:
Rather than constructing an interpretation of the syntax directly, we may work via the intermediary notion of contextual categories, a class of algebraic objects abstracting the key structure carried by the syntax. The plain definition of a contextual category coresponds to the structural core of the syntax; further syntactic rules (logical constructors, etc.) correspond to extra algebraic structure that contextual categories may carry. Essentially, contextual categories provide a completely equivalent alternative to the syntactic presentation of type theory.
Why is this duplication of notions desirable? The trouble with the syntax is that it is mathematically tricky to handle. Any full presentation must account for (among other things) variable binding, capture-free substitution, and the possibility of multiple derivations of a judgement; and so a direct interpretation must deal with all of these, at the same time as tackling the details of the particular model in question. By passing to contextual categories, one deals with these subtleties and bureaucracy once and for all, and obtains a clear framework for subsequently constructing models. Conversely, why not work only with contextual categories, dispensing with syntax entirely?
The trouble on this side is that working with higher-order logical structure in contextual categories quickly becomes unreadable. The reader preferring to take contextual categories as primary may regard the syntax as essentially a notation for working within them: a powerful, flexible, and intuitive notation, but one whose validity requires non-trivial work to establish. (The situation is comparable to that of string diagrams, as used in monoidal and more elaborately structured categories.
Maybe “natural model” should have its own subsection parallel to “categories with families”, “categories with attributes”, etc.
Thanks! I think this reads more clearly, especially now that there’s the profunctorial reformulation in the natural models section.
Sorry to interrupt the discussion. Just wished to say that if you can let me know the LaTeX command for the symbol you are implementing as ⇸ I can add it to the renderer, as we have recently done for \llbracket, \rrbracket, and \esh. With a bit of luck, it will then magically stretch and have improved spacing.
I was using unicode, following the comments on the profunctor page here: https://ncatlab.org/nlab/show/profunctor#notation . That page also includes some LaTeX for defining a new command for a slashed arrow that it seems to me would be reasonable to add.
Ah, thanks, so it does not even exist in LaTeX! It is no problem for me to add it here so that it outputs the unicode symbol, we just need to agree on a name for it. I can use \slashedrightarrow if people wish. Mike sometimes has an opinion on this kind of thing, so I’ll wait a little to see if he pops up here and is OK with the name. Anybody else who has an opinion, please share it!
I thought about asking you to add this symbol too, but I didn’t for this very reason, that it doesn’t have a standard name in LaTeX! But we could certainly make up a name. I would incline towards something like \barredrightarrow or \rightarrowbar, since \slashedrightarrow sounds to me like it would have a diagonal slash like \nrightarrow .
I imagine this paper is worth noting here:
The new idea appears to be to model DTT in the whole -category of locally cartesian closed categories, which since locally presentable may be treated via model categories, rather than rely on a single lccc and slices.
Where would it be added?
we construct cwf structure on the category of all lcc categories instead of cwf structure on some specific lcc category.
So in the Examples section?
I guess so. I haven’t had a chance to read this paper yet.
Well I’ll add in the references
A category with families structure is constructed on the -category of all locally cartesian closed categories, which since locally presentable may be treated via model categories, in:
- Martin Bidlingmaier, An interpretation of dependent type theory in a model category of locally cartesian closed categories, (arXiv:2007.02900)
Hi, I’m the author of this article. The article doesn’t define an new notion of model, it just constructs one particular model, so it’s an instance of a model, not a new notion of model. The model is somewhat special in that it contains every sufficiently small democratic cwf/lccc as a submodel via slicing, so you could say that it’s a “model of models”.
I’d be happy to write a few paragraphs about this on the nlab unless it’s considered bad style to write about your own work here. The idea of the model is that one interprets the contexts of type theory as separate lcc categories instead of as objects of one particular lcc category. I think this would fit next to where Seely’s interpretation in lcc categories is explained, which appears to be here.
The other thing in the paper is a coherence construction which can be phrased in terms of (combinatorial) model category theory. I don’t know of an abstract way to state it for arbitrary type constructors, but the idea for lcc categories is that one can freely adjoin to an lcc category fresh choices of universal objects (finite limits, dependent products) to obtain an equivalent category with the property that every non-strict lcc functor is canonically isomorphic to a strict lcc functor. By working only with categories of the form , the interpretation can be made to have strict substitutions. One way to understand is as cofibrant replacement of , and it’s precisely what you might be familiar with from Lack’s model structure on strict algebras of a 2-monad and their strict morphisms, hence the relation to model category theory.
It’s not at all bad style! Please go ahead, bearing in mind this is a wiki, and it may be touched up. The only aspect that would be considered bad style is using the nLab to bypass normal academic communication channels to promote one’s own super, super niche theory out of all proportion, or a topic bordering on crankery. Adding details about published or arXived work is highly welcome, especially if additional exposition/insight is imparted in the process that might have been unsuitable for the paper.
As the other David says, go right ahead. Maybe the best place is the ’Examples’ section, where you could add a few paragraphs in a new subsection, such as
### Model of models
You can look at the ’Source’ of any entry to understand syntax, or ask here.
Added a reference for comprehension categories
Our main purpose and achievement in this paper is to exhibit the 2-categorical structures secretly at work in the 1-categorical approach to comprehension structures traditionally found in categorical logic.
Not that that article in #34 is explicitly about dependent types, but this page is a redirect for ’comprehension category’, and is the only place as yet to add it.
At some point it would be good to get back to whatever it is that connects Paul-André et al.’s work on refinement (glimpsed at times in the article) with Mike et al.’s work on modality.
Thanks for adding this! I’ve only glanced at it, but it looks like a very nice addition.
Added the reference
Added
Have fixed and completed the publication data for:
and cross-linked with natural models of homotopy type theory
Just a heads-up that in rev 57 on June 9 a user signing as “Anonymous” had dropped code with no less than 9 sub-section headers into the References-section, the top line of the new material announcing it as “Another overview”.
I guess this block of source code was blindly copy-and-pasted from the HoTT wiki. It’s not as long as the 9 subsection headers suggest, since many of them consist of nothing but one or two bib-items.
Maybe somebody who cares about this entry might find the energy to remove this “Another overview”-subsection hierarchy and instead merge the bibitems into the previously existing list?
polished up these two bibitems and deleted their duplication that was silently introduced in June 2022 (see #44 above):
John Cartmell, Generalised algebraic theories and contextual categories, Annals of Pure and Applied Logic Volume 32, 1986, Pages 209-243 (doi:10.1016/0168-0072(86)90053-9)
Thomas Streicher, Semantics of type theory – Correctness, completeness and independence results, Progress in Theoretical Computer Science, Birkhäuser (1991) [ISBN:0-8176-3594-7, doi:10.1007/978-1-4612-0433-6, MR1134134 ]
On Cartmell’s article: I deleted pointer to
https://github.com/peterlefanulumsdaine/cartmell-thesis
since I can’t spot a human-readable file hosted on that page.
If anyone has a pointer to the intended pdf, let’s add it.
(But notice that I have added the doi, using which the original article may be viewed directly here )
polished up these two bibitems and deleted their duplication that was silently introduced in June 2022 (see #44 above)
Eugenio Moggi, A category-theoretic account of program modules, Math. Structures Comput. Sci. 1 1 (1991) 103-139 [MR1108806 , doi:10.1017/S0960129500000074]
Andrew M. Pitts, Categorical logic, in Handbook of Logic in Computer Science 5 Oxford Univ. Press (2000) 39-128 [doi:10.1093/oso/9780198537816.003.0002, pdf, MR1859470]
added pointer to the following item (which was hinted at as “Bart Jacobs’ book” in the silent edit from June 2022):
Polished up this couple of reference items and deleted their duplication that was silently introduced in June 2022 (see #44 above):
Peter Dybjer, Internal type theory, Types for proofs and programs (Torino, 1995), Lecture Notes in Comput. Sci. 1158 Springer (1996) 120-134 [doi:10.1007/3-540-61780-9_66, pdf, MR1474535]
Bart Jacobs, Comprehension categories and the semantics of type dependency, Theoret. Comput. Sci. 107 2 (1993) 169-207 [MR1201808, doi:10.1016/0304-3975(93)90169-T]
Deleted the following pointers also introduced in that June edit, all of which are dead (if anyone has working links, let’s add them in):
http://uf-ias-2012.wikispaces.com/file/view/cwf1.pdf/373011668/cwf1.pdf
http://uf-ias-2012.wikispaces.com/file/view/notesTT.pdf/370624132/notesTT.pdf
http://uf-ias-2012.wikispaces.com/file/view/substitution.pdf/418826938/substitution.pdf
http://uf-ias-2012.wikispaces.com/file/view/CGH-Glynn-anniv-2013.pdf/418828064/CGH-Glynn-anniv-2013.pdf
(all of these look like ill-formed URLs, but even applying the evident fixes does not make them work)
deleted the (ill-formed) duplicates of the following references that were silently introduced in June 2022 (see #44 above):
André Joyal, Notes on Clans and Tribes [arXiv:1710.10238]
Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer Science, 28 2 (2016) 241-286 [arXiv:1406.3219, doi:10.1017/S0960129516000268]
Deleted the sub-section header “References – Another overview” that was silently introduced in June 2022 (see #44 above), having now dealt with all its items.
The only reference in that June edit which was not a duplicate or a broken link was to Jacobs’ textbook (and that was literally given just as “Jacobs’ textbook” ).
added pointer to:
added the following chunk of references, copied over from relation between category theory and type thory:
The model of dependent type theory with dependent product types/dependent function types in locally cartesian closed categories was first made explicit in
The problem with strict substitution compared to weak pullback in this argument was discussed and fixed in
{#Curien} Pierre-Louis Curien, Substitution up to isomorphism, Fundamenta Informaticae, 19 1-2 (1993) 51-86 [doi:10.5555/175469.175471] and: Diagrammes 23 (1990) 43-66 [numdam:DIA_1990__23__43_0]
{#Hofmann} Martin Hofmann, On the interpretation of type theory in locally cartesian closed categories, in Computer Science Logic. CSL 1994, Lecture Notes in Computer Science 933 (1994) 427–441 [doi:10.1007/BFb0022273]
but in the process the equivalence of categories was lost. This was finally all rectified in
and
added pointer to
1 to 57 of 57