Not signed in (Sign In)

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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}


    For CC a locally cartesian closed category CC, it becomes a model for dependent type theory by regarding its codomain fibration C ICC^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 (,1)(\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 (,1)(\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

    Added reference

    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.

    diff, v33, current

    • CommentRowNumber16.
    • CommentAuthormaxsnew
    • CommentTimeOct 19th 2018

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

    diff, v38, current

    • 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

    diff, v39, current

    • 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

    diff, v40, current

    • 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: . 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.

    diff, v41, current

    • CommentRowNumber26.
    • CommentAuthorspitters
    • CommentTimeApr 23rd 2019

    Adding references to Uemara, Isaev

    diff, v45, current

    • 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)(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

    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?

    • 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)(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)

    diff, v46, current

    • 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 𝒞D\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.

    diff, v48, current

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

    diff, v49, current

    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeOct 8th 2020

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

    diff, v49, current

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

    diff, v50, current

    • 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

    Added the reference

    diff, v53, current

  2. Typo (extra “of”)


    diff, v54, current

    • CommentRowNumber42.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 22nd 2021


    diff, v55, current

    • CommentRowNumber43.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2022

    Have fixed and completed the publication data for:

    and cross-linked with natural models of homotopy type theory

    diff, v56, current

    • 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?

    diff, v60, current

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)