# Start a new discussion

## Not signed in

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

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeMay 24th 2012

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.

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeMay 25th 2012

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).

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeJun 9th 2012

I added a few examples of universes, and also the instructive example of simple fibrations, to categorical model of dependent types.

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeSep 29th 2012

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.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeSep 29th 2012

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.

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeSep 29th 2012

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.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeSep 29th 2012
• (edited Sep 29th 2012)

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}

###### Example

For $C$ a locally cartesian closed category $C$, it becomes a model for dependent type theory by regarding its codomain fibration $C^I \to C$ 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.

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeSep 29th 2012
• (edited Sep 29th 2012)

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 $(\infty,1)$-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 $(\infty,1)$-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.

• CommentRowNumber9.
• CommentAuthorzskoda
• CommentTimeSep 29th 2012

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.

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeSep 29th 2012

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 $\infty$-groupoid; it’s just that when we come to look at categorical semantics we only know how to model it using nonalgebraic ones.

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeSep 30th 2012

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.

• CommentRowNumber12.
• CommentAuthorDavidRoberts
• CommentTimeJul 30th 2015

The initial category with families was constructed in

inside type theory with set quotients of higher inductive types.

• CommentRowNumber13.
• CommentAuthorDavidRoberts
• CommentTimeFeb 3rd 2016

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.

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeOct 14th 2016
• (edited Oct 14th 2016)

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.

• CommentRowNumber15.
• CommentAuthorspitters
• CommentTimeJun 2nd 2018

Adding a link to the HoTT wiki. Perhaps these two pages should be integrated at some point.

• CommentRowNumber16.
• CommentAuthormaxsnew
• CommentTimeOct 19th 2018

Reformulation of Awodey’s “natural model” version of CwFs as a specific profunctor being representable.

• CommentRowNumber17.
• CommentAuthorMike Shulman
• CommentTimeOct 20th 2018

Maybe “natural model” should have its own subsection parallel to “categories with families”, “categories with attributes”, etc.

• CommentRowNumber18.
• CommentAuthormaxsnew
• CommentTimeOct 22nd 2018

Split natural models into its own subsection

• CommentRowNumber19.
• CommentAuthorMike Shulman
• CommentTimeOct 22nd 2018

Thanks! I think this reads more clearly, especially now that there’s the profunctorial reformulation in the natural models section.

• CommentRowNumber20.
• CommentAuthormaxsnew
• CommentTimeOct 22nd 2018

Fix some typos in the description of the profunctor in the natural models section

• CommentRowNumber21.
• CommentAuthorRichard Williamson
• CommentTimeOct 22nd 2018
• (edited Oct 22nd 2018)

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.

• CommentRowNumber22.
• CommentAuthormaxsnew
• CommentTimeOct 22nd 2018
• (edited Oct 22nd 2018)

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.

1. 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!

• CommentRowNumber24.
• CommentAuthorMike Shulman
• CommentTimeOct 23rd 2018

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 $\nrightarrow$.

• CommentRowNumber25.
• CommentAuthorkyod
• CommentTimeNov 12th 2018

Added a reference to Comprehensive factorisation systems that build a correspondence between comprehension categories and orthogonal factorization system.

• CommentRowNumber26.
• CommentAuthorspitters
• CommentTimeApr 23rd 2019

• CommentRowNumber27.
• CommentAuthorDavid_Corfield
• CommentTimeJul 10th 2020

I imagine this paper is worth noting here:

• Martin Bidlingmaier, An interpretation of dependent type theory in a model category of locally cartesian closed categories, (arXiv:2007.02900)

The new idea appears to be to model DTT in the whole $(2,1)$-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.

• CommentRowNumber28.
• CommentAuthorDavid_Corfield
• CommentTimeJul 10th 2020

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?

• CommentRowNumber29.
• CommentAuthorMike Shulman
• CommentTimeJul 12th 2020

I guess so. I haven’t had a chance to read this paper yet.

• CommentRowNumber30.
• CommentAuthorDavid_Corfield
• CommentTimeJul 13th 2020

Well I’ll add in the references

A category with families structure is constructed on the $(2,1)$-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)
• CommentRowNumber31.
• CommentAuthormbid
• CommentTimeJul 13th 2020

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 $\mathcal{C}$ fresh choices of universal objects (finite limits, dependent products) to obtain an equivalent category $\mathcal{C}'$ with the property that every non-strict lcc functor $\mathcal{C}' \rightarrow D$ is canonically isomorphic to a strict lcc functor. By working only with categories of the form $\mathcal{C}'$, the interpretation can be made to have strict substitutions. One way to understand $\mathcal{C}'$ is as cofibrant replacement of $\mathcal{C}$, 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.

• CommentRowNumber32.
• CommentAuthorDavidRoberts
• CommentTimeJul 13th 2020

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.

• CommentRowNumber33.
• CommentAuthorDavid_Corfield
• CommentTimeJul 13th 2020

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


### Model of models

You can look at the ’Source’ of any entry to understand syntax, or ask here.

• CommentRowNumber34.
• CommentAuthorDavid_Corfield
• CommentTimeSep 17th 2020

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.

• CommentRowNumber35.
• CommentAuthorDavid_Corfield
• CommentTimeSep 17th 2020

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.

• CommentRowNumber36.
• CommentAuthorMike Shulman
• CommentTimeOct 8th 2020

This page still contained a claim from its original version in 2012 that the right adjoint splitting was better for type theory. I updated it to the modern-as-of-2014 view that the left adjoint splitting is better.

• CommentRowNumber37.
• CommentAuthorMike Shulman
• CommentTimeOct 8th 2020

Also added a note and citation that the contextual core of a CwA is a right adjoint.

• CommentRowNumber38.
• CommentAuthormbid
• CommentTimeNov 15th 2020
• (edited Nov 15th 2020)

Add example: The big model in the category of lcc categories.

This got quite long, and it overwhelms the examples section somewhat. Let me know if it should be shortened/moved somewhere else.

• CommentRowNumber39.
• CommentAuthorRichard Williamson
• CommentTimeNov 15th 2020
• (edited Nov 15th 2020)

Thanks for adding this! I’ve only glanced at it, but it looks like a very nice addition.

• CommentRowNumber40.
• CommentAuthorDavid_Corfield
• CommentTimeJul 6th 2021

2. Typo (extra “of”)

Anonymous

• CommentRowNumber42.
• CommentAuthorDavid_Corfield
• CommentTimeNov 22nd 2021

• CommentRowNumber43.
• CommentAuthorUrs
• CommentTimeJun 7th 2022

Have fixed and completed the publication data for:

and cross-linked with natural models of homotopy type theory

• CommentRowNumber44.
• CommentAuthorUrs
• CommentTimeJun 25th 2022

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?

• CommentRowNumber45.
• CommentAuthorUrs
• CommentTime4 days ago

polished up these two bibitems and deleted their duplication that was silently introduced in June 2022 (see #44 above):

• CommentRowNumber46.
• CommentAuthorUrs
• CommentTime4 days ago

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 )

• CommentRowNumber47.
• CommentAuthorUrs
• CommentTime4 days ago

polished up these two bibitems and deleted their duplication that was silently introduced in June 2022 (see #44 above)

• CommentRowNumber48.
• CommentAuthorUrs
• CommentTime4 days ago

added pointer to the following item (which was hinted at as “Bart Jacobs’ book” in the silent edit from June 2022):

• CommentRowNumber49.
• CommentAuthorUrs
• CommentTime4 days ago
• (edited 4 days ago)

Polished up this couple of reference items and deleted their duplication that was silently introduced in June 2022 (see #44 above):

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)

• CommentRowNumber50.
• CommentAuthorUrs
• CommentTime4 days ago

deleted the (ill-formed) duplicates of the following references that were silently introduced in June 2022 (see #44 above):

• CommentRowNumber51.
• CommentAuthorUrs
• CommentTime4 days ago
• (edited 4 days ago)

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” ).

• CommentRowNumber52.
• CommentAuthorUrs
• CommentTime4 days ago

• CommentRowNumber53.
• CommentAuthorUrs
• CommentTime4 days ago

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

but in the process the equivalence of categories was lost. This was finally all rectified in

and