# 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.
• CommentAuthorUrs
• CommentTimeMay 15th 2012

now I have finally the time to come back to this, as announced, and so I am now starting an entry:

So far there is just some literature collected. I now plan to extract the essence of Seely’s artice into the entry in some technical detail.

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeMay 15th 2012
• (edited May 15th 2012)

it won’t come as a surprise to you that I am creating a table.

Currently it looks like this:

flavor of type theory $\;$equivalent to$\;$ flavor of category theory
first-order logic hyperdoctrine (Seely 1984a)
dependent type theory locally cartesian closed category (Seely 1984b)
intensional type theory with identity types locally cartesian closed (∞,1)-category (conjectural)
homotopy type theory with higher inductive types elementary (∞,1)-topos (conjectural)

But that made me wonder: what’s the best terminology for the entries on the left? What should be the canonical term for that part of homotopy type theory which does not assume univalence and hence is supposedly the language of locally cartesian closed $(\infty,1)$-categories?

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeMay 15th 2012

I dunno. Just “homotopy type theory” maybe?

I think there’s also an equivalence between some kind of type theory and elementary 1-toposes somewhere in the literature…

1. One could add in the entry that the morphisms in the categories in the left column of the table are what Seely calls ”derivations”.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeMay 16th 2012
• (edited May 16th 2012)

have been working on HoTT methods for homotopy theorists. Mainly added a bunch of translation tables, also reorganized a bit. Still far from what it should eventually be, but at least it is beginning to look like an entry.

A point to be amplified more, also with respect to the $n$Café-discussion, is how in the internal HoTT language statements about fibers simplify, in that the naive external statements which are generally wrong become true internally: “A morphism is $n$-truncated/$n$-connected if all fibers are so.”

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeMay 16th 2012

the morphisms in the categories in the left column of the table are what Seely calls ”derivations”.

That seems like a weird name to me; I’d be more inclined to call them something like “translations”.

2. it won’t come as a surprise to you that I am creating a table.

I like the encyclopedic flavor of your tables!

have been working on HoTT methods for homotopy theorists. Mainly added a bunch of translation tables,

In the basic dictionary table I missed that a morphism $f:X\to Y$ which is not necessarily a fibration corresponds to a typing judgement $x:X\vdash f(x):Y$. Is this omission intended?

I’d be more inclined to call them something like “translations”.

This sounds fairly descriptive. Can you explain why this is a good name?

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeMay 16th 2012

Mike writes:

I dunno. Just “homotopy type theory” maybe?

It’s just that eventually we need two terms, one for the internal language of locally cartesian closed $(\infty,1)$-catgegories in general, and one for that of elementary $(\infty,1)$-toposes.

I think there’s also an equivalence between some kind of type theory and elementary 1-toposes somewhere in the literature…

Scott and Lambek in their section II have an adjunction between toposes with NNO and type theories with product types and natural numbers. Is that maybe what you have in mind? If not, I’d be very interested in finding the reference that you do have in mind.

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeMay 16th 2012
• (edited May 16th 2012)

Concerning “derivations” and “translations”: I think you are maybe talking about different tables each?

Seely calls a term of a type a “derivation”, because it can be regarded a proof of a proposition. What should be called “translations” are the morphisms in the category of type theories, since they translate one internal language into another)

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeMay 16th 2012
• (edited May 16th 2012)

Stephan writes:

I like the encyclopedic flavor of your tables!

Thanks for letting me know. I am certainly benefitting from making such tables explicit. It helps me organize my thoughts and see clearly.

In the basic dictionary table I missed that a morphism f:X→Y which is not necessarily a fibration corresponds to a typing judgement x:X⊢f(x):Y. Is this omission intended?

It’s not really omitted, as this is a special case of the clause for a term (forth item in the table). There also the type $Y$ may depend on $x$. Your typing judgement is obtained from this by assuming that $Y$ does not in fact depend on $X$, hence by assuming that the fibration in question is the projection $Y \times X \to X$.

Maybe I should add a remark about that (as soon as the $n$Lab reacts again).

• CommentRowNumber11.
• CommentAuthorDavid_Corfield
• CommentTimeMay 16th 2012

Is the relationship between the hyperdoctrine approach and the syntactic category approach to logic known? We were talking about it here.

• CommentRowNumber12.
• CommentAuthorUrs
• CommentTimeMay 16th 2012

We were talking about it here.

Hm, interesting that slide 96 of Hirschowitz.

I guess the devil is in the details somewhere, but Seely seems to have made this kind of adjunction an equivalence

$FirstOrderTheories \simeq Hyperdoctrines$

already in 1987 (references at relation between type theory and category theory).

I haven’t looked through all the details. One thing that seems noteworthy is that in his proof Seely in fact considers hyperdoctrines whose fibers are not required to be posets. Maybe that makes the difference. But I’d say the equivalence proven justifies whatever fine-tuning on $Hyperdoctrines$ made it work.

• CommentRowNumber13.
• CommentAuthorUrs
• CommentTimeMay 16th 2012

Hm, Seely’s article contains a mistake, in that it is not dealing with the non-uniqueness of pullbacks in the category correctly.

In

there is at least a partial fix. Though I need to figure out if that fix retains the equivalence of categories $DependentTypeTheories \simeq LocallyCartesianClosedCategories$ that Seely claimed.

• CommentRowNumber14.
• CommentAuthorMike Shulman
• CommentTimeMay 16th 2012

• CommentRowNumber15.
• CommentAuthorMike Shulman
• CommentTimeMay 16th 2012

I think you are maybe talking about different tables each?

Ah, indeed we were! I misinterpreted Stephan’s remark #4. But in that case, I think the morphisms should just be called “terms”.

• CommentRowNumber16.
• CommentAuthorMike Shulman
• CommentTimeMay 16th 2012

It’s just that eventually we need two terms, one for the internal language of locally cartesian closed (∞,1)-catgegories in general, and one for that of elementary (∞,1)-toposes.

“homotopy type theory” and “univalent (homotopy) type theory”?

• CommentRowNumber17.
• CommentAuthorUrs
• CommentTimeMay 16th 2012

“homotopy type theory” and “univalent (homotopy) type theory”?

But what about the higher inductive types?

Currently in the entry I have (I think) “homotopy type theory” for the language of LCC $\infty$-categories and “homotopy type theory with higher inductive types and univalence” for the language of elementary $\infty$-toposes.

• CommentRowNumber18.
• CommentAuthorUrs
• CommentTimeMay 16th 2012

Ah, great! Thanks, Mike. And what a coincidence that we posted #13 and #14 in the very same minute! :-)

• CommentRowNumber19.
• CommentAuthorTobyBartels
• CommentTimeMay 16th 2012

@Mike #15: Whether morphisms should be called ‘terms’ depends on whether objects are called ‘types’. Are the objects here types or contexts?

• CommentRowNumber20.
• CommentAuthorUrs
• CommentTimeMay 16th 2012

Toby: types.

The article under discussion is this one.

• CommentRowNumber21.
• CommentAuthorUrs
• CommentTimeMay 16th 2012
• (edited May 16th 2012)

re 18: I have worked this and related references into the entry.

When I started this quest, I had no idea that what I am after was still not settled by December last year! I thought this is ancient stuff. Interesting to see that it is not only in physics that some statements become so much folk lore that people forget that they haven’t proven them yet ;-)

• CommentRowNumber22.
• CommentAuthorMike Shulman
• CommentTimeMay 17th 2012

I think we can be flexible with terminology and not demand a concise term for every possible variation on a theme.

• CommentRowNumber23.
• CommentAuthorMike Shulman
• CommentTimeMay 24th 2012

Is it really a good idea to include the detailed constructions of the functors $Con$ and $Lan$ in the particular case of DTT vs LCCCs on the page relation between type theory and category theory? The construction of $Con$ is already described at (now) syntactic category; why duplicate it elsewhere? If we want to include the proof that $Con(T)$ is LCCC when $T$ is a DTT, it seems more natural to me to put it at syntactic category or at dependent type theory. Similarly for $Lan$.

• CommentRowNumber24.
• CommentAuthorUrs
• CommentTimeMay 24th 2012

That sounds reasonable. I didn’t finish what had planned to write there anyway.

Right now I don’t have the time to look into this. But if you have a second to do so, feel free. Otherwise I can try to look into it later.

• CommentRowNumber25.
• CommentAuthorMike Shulman
• CommentTimeMay 24th 2012

I think there is a lot of duplication and confusing organization right now. (Nobody’s fault, surely, it just happened organically.) The page internal logic discusses, for first-order theories, exactly the sort of thing that categorical semantics currently does for dependent type theories. A lot of the same thing is also at the introductory section on categorical semantics at type theory, as well as at relation between type theory and category theory.

I suppose it makes sense to keep an intuitive discussion at type theory for people who are just stumbling on that page. But maybe the rest of it can be unified and better organized. What about merging relation between type theory and category theory with categorical semantics? Maybe a descriptive pagename would be categorical semantics of type theory. Then we can try to centralize constructions of the functor $Lang$ on the page internal logic, construction of the functor $Syn$ on the page syntactic category, and discussion of the adjunction/equivalence between them at the merged page.

• CommentRowNumber26.
• CommentAuthorUrs
• CommentTimeMay 25th 2012

Yes, I feel precisely the same way. The current status of the pages is the result of several attempts to start with the same topic, each of them unfinished.

I’d certainly have no objections against merging pages.

• CommentRowNumber27.
• CommentAuthorUrs
• CommentTimeSep 17th 2013

Does anyone know if the Clairambault-Dybjer article on “The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories” has meanwhile been published in a journal?

• CommentRowNumber28.
• CommentAuthorUlrik
• CommentTimeSep 17th 2013

From MathSciNet:

@incollection {MR2830789,
AUTHOR = {Clairambault, Pierre and Dybjer, Peter},
TITLE = {The biequivalence of locally {C}artesian closed categories and
{M}artin-{L}\"of type theories},
BOOKTITLE = {Typed lambda calculi and applications},
SERIES = {Lecture Notes in Comput. Sci.},
VOLUME = {6690},
PAGES = {91--106},
PUBLISHER = {Springer},
YEAR = {2011},
MRCLASS = {03B15 (18B99)},
MRNUMBER = {2830789 (2012i:03029)},
DOI = {10.1007/978-3-642-21691-6_10},
URL = {http://dx.doi.org/10.1007/978-3-642-21691-6_10},
}

• CommentRowNumber29.
• CommentAuthorUrs
• CommentTimeSep 17th 2013

Thanks! I have added that to the entry now.

• CommentRowNumber30.
• CommentAuthorUrs
• CommentTimeDec 9th 2013

At relation between type theory and category theory I made the table entry on linear logic come out right and link to

Also highlighted this more at star-autonomous category and at linear logic.

• CommentRowNumber31.
• CommentAuthorUrs
• CommentTimeMar 27th 2014

Added a pointed to Joyal’s recent talk on categorical semantics of HoTT, and also added Mike’s notes that precede this by two years, so in total I added this to the References section at relation between type theory and category theory:

Details on this higher categorical semantics of homotopy type theory are in

with lecture notes in

• Mike Shulman, Categorical models of homotopy type theory, April 13, 2012 (pdf)

• Andre Joyal, Categorical homotopy type theory, March 17, 2014 (pdf)

• CommentRowNumber32.
• CommentAuthorZhen Lin
• CommentTimeMar 27th 2014

The Joyal link seems to point to Voevodsky’s slides.

• CommentRowNumber33.
• CommentAuthorUrs
• CommentTimeMar 27th 2014
• (edited Mar 27th 2014)

Woops.

Could somebody fix it for me, as i am just on my phone now.

(Unwise choice of file name, eh.)

• CommentRowNumber34.
• CommentAuthorZhen Lin
• CommentTimeMar 28th 2014

Fixed.

• CommentRowNumber35.
• CommentAuthorUrs
• CommentTimeMar 28th 2014

Thanks!

• CommentRowNumber36.
• CommentAuthorUrs
• CommentTimeMar 31st 2014
• (edited Mar 31st 2014)

The entry long has a placeholder section On HoTT with Univalence interpreted in infinity-Toposes.

Is there a precise version of the statement that involves mumbling “weakly Tarski universes”?

I imagine at that point in the entry it could say the following, but I don’t know what the formal status of the second half of the statement is:

Homotopy type theory with the univalence axiom added has interpretation in locally presentable and locally Cartesian closed $\infty$-categories which also satisfy the Giraud-Rezk-Lurie axioms. This is strictly so for those which have presentation by model structures of simplicial presheaves over elegant Reedy categories (Shulman), and is true generally if the univalent universes are interpreted “weakly a la Tarski”.

• CommentRowNumber37.
• CommentAuthorMike Shulman
• CommentTimeMar 31st 2014

I wrote a bit leading up to a more formal meaning of the statement in quotes at universe (homotopytypetheory).

• CommentRowNumber38.
• CommentAuthorUrs
• CommentTimeApr 1st 2014
• (edited Apr 1st 2014)

Thanks for that.

I have adapted the text that I found at that link to expand the $n$Lab entry type of types. There is now a section "Formalization" with essentially your text (enriched by some more hyperlinks), and then I have added a brief paragraph Properties – Categorical semantics with pointers to the articles that I am aware of.

I tried to vaguely indicate that the discussion in Gepner-Kock would fit under the "weakly Tarskian" umbrella. But you may feel wanting to touch the text here and there.

Then, finally, I have added a corresponding paragraph at relation between TT and CT – Univalent HoTT and Elementary infinity-toposes.

Again I pointed to the pertinent references (or tried to). The paragraph currently ends with a brief remark on how, therefore, HoTT+UV+HIT is analogous to a homotopy theoretic version of ETCS.

• CommentRowNumber39.
• CommentAuthorMike Shulman
• CommentTimeApr 1st 2014

It makes me kind of sad to copy text from one wiki to another rather than linking, since then if it gets improved in one place, the improvement won’t be visible in the other place. I also wasn’t sure that it was really reasonable to call a Tarski universe a “type of types” rather than a “type of codes for types”.

I tried to clarify some statements at “relation” that I thought were misleading or confusing.

• CommentRowNumber40.
• CommentAuthorUrs
• CommentTimeApr 1st 2014
• (edited Apr 1st 2014)

Mike,

regarding the “relations”-entry: thanks for the edits.

Regarding duplicating material: that is in the end due to your decision, not mine. I am not supposed to edit over at homotopytheory, not to link back to the nLab, and you are duplicating keywords over there which we already have on the nLab. So that makes that wiki be an external resource from the point of view of the nLab.

If I just linked to your entry over at homotopytypetheory then all the supplementary links that the nLab does offer are not abvailable, I can’t add links etc. That makes just linking to the entry less preferred than adapting its content to the nLab.

• CommentRowNumber41.
• CommentAuthorMike Shulman
• CommentTimeApr 1st 2014

I never said you weren’t supposed to edit at the HoTT wiki; just that the edits should be in its spirit, which is different from the nLab’s. Linking to the nLab is also fine from there if it’s for a topic that we probably won’t want a page on there, and otherwise one can just make a stub there which links to here, just as we sometimes do here linking to wikipedia.

I also don’t think I agree that copying content from an external resource into the nLab is always preferable to linking to it. When the external resource is static, that makes some sense (apart from the duplication of effort involved), but when the external resource is liable to change and improve itself, I think it’s better to link. By analogy, I administer a database system for a nonprofit that I volunteer for, and if you want to see only some of the information in a database table, you don’t copy that data into a smaller table, but you make a “stored view” that essentially links to the original data.

• CommentRowNumber42.
• CommentAuthorUrs
• CommentTimeMay 7th 2014
• (edited May 7th 2014)

• CommentRowNumber43.
• CommentAuthorUrs
• CommentTimeMay 7th 2014
• (edited May 7th 2014)

• CommentRowNumber44.
• CommentAuthorMike Shulman
• CommentTimeMay 7th 2014

Linking to the original source is better than not linking, but linking without copying is still better.

Actually, here’s a question: can we do [[!include]] in between webs? I.e. could we include a page from the HoTT wiki into an nLab page? I just tried it at the Sandbox and it doesn’t seem to work, but it seems like this oughtn’t to be too hard to implement even if Instiki doesn’t do it yet.

• CommentRowNumber45.
• CommentAuthorUrs
• CommentTimeMay 8th 2014

Mike, we both easily agree on what would be optimal here. But maybe we disagree on what the most practical compromise is. From my point of view currently if I send a reader from an $n$Lab page on type theory to the corresponding entry on the homotopytypetheory then I deprive him/her of a whole lot of type theoretic cross-link information that the nLab has, while homotoptypetheory does not. Readers who are already expert on the multitude of type theoretic verbiage may be happy with this, but my feeling is that the readers I care most about are not. Therefore from my point of view the best compromise is that I don’t mandatorily send readers to homotopytypetheory. Instead I copy from there the relevant information and then provide a pointer to it for those readers who wish to check for more information. This is much like we treat any other nLab-external source.

• CommentRowNumber46.
• CommentAuthorUrs
• CommentTimeMay 8th 2014

added a pointer to Lumsdaine-Warren 13

• CommentRowNumber47.
• CommentAuthorAlexisHazell
• CommentTimeMay 11th 2014
Urs, Mike,

I've only just learned of this forum, and of this discussion in particular.

As a relative beginner to HoTT, type theory, algebraic topology and category theory, I've been working on the HoTT wiki as part of my learning process: porting content from the old UF wiki, adding and fixing links, and so on.

Obviously I'm in no position to determine if and when a topic probably won't need HoTT-specific coverage, such that it's appropriate to link to an existing nLab page. However, I also find my learning flow is interrupted when a term on the HoTT wiki links to a non-existent (or minimal-content) HoTT wiki page, rather than an existing nLab page (which I then have to find via a manual search). On the gripping hand, I can certainly understand that there will sometimes be a need for a HoTT-specific perspective on certain concepts.

My suggestion, fwiw, is:

(1) default to linking to pages on the nLab wiki, where they exist and more substantial than mere stubs;

(2) only create new HoTT pages about concepts already covered on nLab in order to provide HoTT-oriented content about those concepts;

(3) ensure that the pages thus created don't duplicate existing information on nLab, but instead link to that information.
• CommentRowNumber48.
• CommentAuthorUrs
• CommentTimeMay 11th 2014
• (edited May 11th 2014)

One comment: on the nLab there easily is room for every entry to have a section providing the “HoTT-specific perpective”. Many enries already try to provide exactly that (though of course, as usual on the nLab, the current state may be found wanting). Given it’s very nature, HoTT is very much on-topic for the nLab.

My understanding is that the reason not to try to merge the content of the homotopytyetheory web into the nLab alltogether is more a sociological one, that people potentially contributing to the homotopytypetheory web may prefer the “more quiet” place that it may feel like, undisturbed by what weird ideas other people may have about editing wiki pages.

• CommentRowNumber49.
• CommentAuthorMike Shulman
• CommentTimeMay 11th 2014

Yes, the point is for the HoTT wiki to feel “owned” by the HoTT community.

Also, I would not recommend trying to learn about HoTT from the HoTT wiki! It’s nowhere near complete enough for that.

• CommentRowNumber50.
• CommentAuthorAlexisHazell
• CommentTimeMay 12th 2014
Re. the sociological issue - fair enough, point taken.

Mike: even taking the sociological issue into consideration, my first preference (call it 'A') is still to link to relevant substantive nLab pages where they exist and where not even a minimal HoTT page exists; my second preference, option 'B', would be to create minimal HoTT pages that then link to any existing substantive nLab pages; and option 'C' would be to simply leave links pointing to non-existent pages until someone wishes to make some notes about the linked-to topic. Not sure if there are other options, but which option would you prefer?

I'm certainly not trying to learn HoTT from the wiki alone! I'm continually perusing The Book also, and following the HoTT mailing list; mailing list posts regularly bring to my attention which concepts I've not necessarily got my head around yet. But:

* The Book isn't great for getting a quick reminder about the details of a particular concept. I would rather search for and access a page about 'transport' on the wiki (via my browser, which I always have open), than open up the PDF of The Book (via a PDF reader, which I don't always have open), find the page in the index which mentions 'transport', then go to the first page referenced. In this particular case, the first page referenced does have the definition of 'transport', but that's that not always true - concepts are sometimes discussed in passing before being formally defined.

* I don't want to clutter what I understand to be a research-oriented mailing list with beginner-level questions, nor waste list members time by asking them to provide answers that can be found off-list. Having said that, there are some concepts regularly referred to on the list which I've not yet found a formal definition for; 'fibrant' is a good example. What does it mean for a type to be 'fibrant'? The word isn't listed in the index of The Book, and it's only mentioned twice elsewhere, in the context of "fibrant replacement". I'm guessing it might mean "the type is a fibration, i.e. a type family", but I'm not sure.

My hope is that the wiki can address both issues, and that I can help towards that end. :-)
• CommentRowNumber51.
• CommentAuthorDavidRoberts
• CommentTimeMay 12th 2014
• (edited May 12th 2014)

Hi Alexis,

first up, welcome to the nForum! Regarding ’fibrant’, my understanding is that it is analogous to fibrant objects in a model category. Since Homotopy Type Theory is a synthetic homotopy theory, there is likely some cross-pollination that lead to this term.

• CommentRowNumber52.
• CommentAuthorUrs
• CommentTimeMay 12th 2014

re #50, option B is the most “sustainable”, I think. This is essentially what I usually do on the nLab itself: when we need a keyword but have no content for it yet, I create a stub entry on the nLab that essentially just points to Wikipedia or some other standard source, and then link to that stub. This way the link exists right away, needs not to be remembered to be changed in the future, and the moment somebody comes and fills in actual details all is good.

• CommentRowNumber53.
• CommentAuthorAlexisHazell
• CommentTimeMay 12th 2014
David,

Unfortuntately I'm not at the point where I understand what "fibrant objects in a model category" means. I've actually spent years making repeated efforts to understand more than the basics of category theory (initially because of Haskell), but haven't had as much success as I'd hope. My experience has tended to be that, where I can often roughly understand the /technical definition/ of things (e.g. categorical 'limits'), I feel I don't 'get' them on an intuitive level. And in general, I've found many explanations of category theory to be analogous to:

- "I don't speak German at all; what does 'Flugzeug' mean?"
- "'Flugzeug' beschreibt ein Fahrzeug für Menschen fliegen durch die Luft."
- "Er ...."

:-)

One of the things I'm enjoying about learning HoTT is that I feel it's gradually helping me to start to get a handle on category theory. I feel relatively comfortable with type theory, so things like the wonderful "computational trinitarianism" table in the "relation between type theory and category theory" nLab page really help. :-)
• CommentRowNumber54.
• CommentAuthorUrs
• CommentTimeMay 12th 2014

Oh, I had missed that there was a quetion on what “fibrant type” means. Am adding a brief explanation now, just a moment…

• CommentRowNumber55.
• CommentAuthorUrs
• CommentTimeMay 12th 2014

Okay, I have written something at fibrant type and then also had to write something at Homotopy Type System.

• CommentRowNumber56.
• CommentAuthorDavidRoberts
• CommentTimeMay 12th 2014

@Alexis:

Urs is right: fibrant types seem to be a recent development centred on HTS, and are special types that in a sense can ’see’ the correct maps into or out of them (I’m not sure which, because like you I don’t follow the details of the discussions on the HoTT list very well).

• CommentRowNumber57.
• CommentAuthorUrs
• CommentTimeMay 12th 2014
• (edited May 12th 2014)

(Well, “fibrant” $\leftrightarrow$ “into”, sort of by definition.)

Yes, it’s not only a recent development, but also a somewhat ideosyncratic one, in that it is really mainly a development that Vladimir Voevosky did, when he ran into technical issues with defining semisimplicial types in “default” HoTT.

One thing has finally become clear to me after lots of discussion (personal and on the HoTT list), namely: Vladimir Voevodsky himself is not actually after “synthetic homotopy theory”. For him univalent HoTT is a way to fix intensional ML-type theory and hence make it available for formalizing mathematics. This formalization he imagines to proceed very much along the classical lines.

For instance when he says that his long-term goal is to have his work on motivic cohomology fully formalized, he is emphatically NOT thinking of using HoTT as the internal language for the $\infty$-topos over the Nisnevich site (maybe to find the “synthetic” axioms needed to be added to HoTT such that it speaks about $\infty$-toposes close enough to that over the Nisnevich site for $\mathbb{A}^1$-homotopy theory to be expressible), instead he is aiming for a formalization that faithfully follows the classical ways these things are set up via model categories of simplicial presheaves. Indeed, he is (and has been) thinking about axioms to be added to HoTT that will exclude all models other than that in plain simplicial sets.

If you are interested in “synthetic homotopy theory” proper, you need to follow the recent developements by Shulman, Lumsdaine et al. Voevodsky has been pushing much in a different direction, and HTS with its “non-fibrant types” is the latest incarnation of that.

• CommentRowNumber58.
• CommentAuthorMike Shulman
• CommentTimeMay 12th 2014

I vote for option B. I think creating stubs that link to relevant nLab pages is a great idea; then people can fill in more HoTT-specific info as they have time.

Re: the book, when a concept has multiple pages listed in the index, the page where it is defined should be in bold. If you find entries that don’t conform to this, please bring them to our attention. But it does make sense that it is easier to search a wiki than a book.

Re: fibrancy, the most important thing to understand is that this is only relevant (and meaningful) in two situations: (1) when constructing models of type theory in a model category, and (2) when working in an experimental type system such as HTS. The book never mentions it because the concept doesn’t exist in the type theory used in the book and because the book doesn’t discuss constructing models.3

Are you aware of the hott-amateurs mailing list? It was created specifically for newcomers to ask questions that would feel uncomfortable on the more research/expert-focused list.

• CommentRowNumber59.
• CommentAuthorTodd_Trimble
• CommentTimeMay 12th 2014

hott-amateurs sounds like a porn site! But I’m glad to learn of it.

• CommentRowNumber60.
• CommentAuthorDavidRoberts
• CommentTimeMay 12th 2014
• (edited May 13th 2014)

@urs I know fibrancy $\leftrightarrow$ mapping into, but the discussion has been around constructing new type by various means that took to imply mapping out of things. But now I read some recent posts, I realise that I’d misread, and people are talking about mapping out of the constructions into fibrant types.

• CommentRowNumber61.
• CommentAuthorDavidRoberts
• CommentTimeMay 12th 2014
• (edited May 13th 2014)

arg flaky connection. I’ll fix the previous anon. (Done)

• CommentRowNumber62.
• CommentAuthorMike Shulman
• CommentTimeMay 12th 2014

@Todd: Yeah, I know. I didn’t name it…

• CommentRowNumber63.
• CommentAuthorAlexisHazell
• CommentTimeMay 13th 2014
Looks like option B it is then. :-) I'll work on the wiki accordingly.

@Urs:

Thanks for your work on the 'fibrant type' entry - I've given it a quick scan, but will be sure to give it a proper read soon. :-)

@Mike:

Re. the index of The Book: okay, will do.

Re. fibrancy: okay, will keep that in mind.

Re. the Hott Amateurs list: I wasn't aware of that list, no - thanks for bringing it to my attention! I've added a link to it (and to the main HoTT list) from the HoTT wiki Home Page. :-)
• CommentRowNumber64.
• CommentAuthorUrs
• CommentTimeSep 28th 2017

Have added a pointer (here) to

• CommentRowNumber65.
• CommentAuthorUrs
• CommentTimeOct 30th 2017
• (edited Oct 30th 2017)

But I keep being suprised how this is presented as if there were no long tradition of categorical semantics of dependent type theory in fibration-like categories, as well as various recent articles with very similar approaches and results.

• CommentRowNumber66.
• CommentAuthorUrs
• CommentTimeApr 22nd 2018

Given discussion in other threads, we should revisit the entries such as relation between type theory and category theory, regarding their use of terminology.

I suppose where Seely and others used to speak of “type theories” (notably in Theorem 3.2), one should say “type 0-theories” if one were to follow Mike’s recent suggestion (slide 33 (49 of 88)).

• CommentRowNumber67.
• CommentAuthorDavid_Corfield
• CommentTimeApr 22nd 2018

Isn’t that Theorem 3.2 further up the levels? Surely the theorem itself concerns a doctrine (2-theory) and the individual ML dependent type theories are 1-theories.

• CommentRowNumber68.
• CommentAuthorUrs
• CommentTimeApr 22nd 2018
• (edited Apr 22nd 2018)

Yes, but that 2-theory is not what these authors refer to by “type theory”. They speak of the 2-category “of type theories” and their theorem shows that “a type theory”, in their sense, is the same, up to equivalence, as a category that is a model for a type 1-theory. What these authors call “type theories” are what Mike suggests to call “type 0-theories”.

• CommentRowNumber69.
• CommentAuthorMike Shulman
• CommentTimeApr 23rd 2018

I think I’m with David #67. The objects of the “2-category of type theories” are type theories generated by base types, terms and axioms, which correspond to the categories freely generated by those; according to the hierarchy on my slides those are 1-theories on both sides, and the 2-categories that are equivalent are each an incarnation of a 2-theory. A 0-theory is a functor between two such categories, a model of the domain in the codomain.

• CommentRowNumber70.
• CommentAuthorUrs
• CommentTimeApr 24th 2018

But then, take the image under their equivalence of the toposes inside all locally cartesian closed categories. That gives a 2-category of type theories equivalent to that of toposes. These are the geometric type theories.

Since elsewhere you complained that the latter have not been defined, I thought you must mean it for some different notion of “type theory”.

• CommentRowNumber71.
• CommentAuthorMike Shulman
• CommentTimeApr 24th 2018

On the syntactic side, you can’t just take an arbitrary sub-2-category of the 2-category of models of some 2-theory and call it another 2-theory. You need a syntactic presentation of it.

• CommentRowNumber72.
• CommentAuthorUrs
• CommentTimeApr 24th 2018
• (edited Apr 24th 2018)

We are still talking past each other.

I am looking at that theorem 3.2, the classical statement by Seely, in its improved version.

It uses the following words:

There are 2-functors

that constitute an equivalence of 2-categories

$MLDependentTypeTheories \underoverset {\underset{Cont}{\longrightarrow}} {\overset{Lang}{\longleftarrow}} {\simeq} LocallyCartesianClosedCategories \,.$

(I may have typed that nLab version of the statement originally, but I believe this accurately reflects the language used in the corresponding articles.)

There is no mentioning of “2-theory” here. There is mentioning just of “theories”. And these are the objects in the 2-category on the left.

How do you want to call the objects in the 2-category on the left? “1-theories”? I am happy with whatever term you like best.

But since we have an equivalence between these “theories” and locally Cartesian closed cateories, we are entitled to transfer all names of special kinds of objects on the right to left left.

The sub-2-category $Toposes\hookrightarrow LocallyCartesianClosedCategories$ has an essential image

$Lang(Toposes) \hookrightarrow MLDependentTypeTheories$

which consists of some more special kind of “theories” – necessarily, since all objects in the 2-category $MLDependentTypeTheories$ are called “theories”, at least by Seely et al.

• CommentRowNumber73.
• CommentAuthorMike Shulman
• CommentTimeApr 24th 2018

Firstly, I’m not really happy with calling the objects in the 2-category on the left (the “syntax side”) “theories” of any sort, despite what various people in the literature do. To me a syntactic 1-theory is a syntactic object. I would call the objects of that 2-category on the left by the actual categorical structure that they are (“categories with families” in Clairambault-Dybjer).

It is true though that every category with families is presentable by some syntactic 1-theory. So you could, I guess, define a “geometric type 1-theory” to be a dependent type 1-theory whose corresponding lccc is a topos. However, this would not be a “dependent-type-theory refinement of geometric logic”, because “geometric logic” is not just a collection of syntactic 1-theories, but a syntactic 2-theory (written in the syntactic 3-theory of first-order logic — a 3-theory that I didn’t mention in the talk because it should be subsumed by the 3-theory of dependent type theory). Thus, geometric type theory should also be a syntactic 2-theory, this time written in the syntactic 3-theory of dependent type theory.

• CommentRowNumber74.
• CommentAuthorMike Shulman
• CommentTimeApr 24th 2018

Maybe it will help to bump it down a notch. Fix a particular 1-theory, say the 1-theory of groups (in the 2-theory of finite-product theories, in the 3-theory of simple type theory). A syntactic 0-theory is a group presentation; a semantic 0-theory is a group. The syntactic 1-theory of groups consists of the operations and axioms of a group, while the semantic 1-theory of a group is the category of groups. The rules of the syntactic 1-theory (the operations and axioms of a group) can be applied to a syntactic 0-theory (group presentation) to incarnate it as a semantic 0-theory (the group presented by a group presentation). A model of such a group presentation $\langle G | R \rangle$ in a group $H$ is an interpretation of the generators $G$ as elements of $H$ such that the relations $R$ are satisfied; the universal property of presented groups says that this is equivalent to a group homomorphism from the group presented by $\langle G|R\rangle$ into $H$.

Now suppose we are interested in some subcategory of groups, such as abelian groups, torsion-free groups, nilpotent groups, etc. In the semantic world we can just say “consider the full subcategory of X-groups”, obtaining a category that one might be tempted to call a new “semantic 1-theory”. But the corresponding sub-class of group presentations does not necessarily correspond to any syntactic 1-theory, and certainly not one in the same 2-theory. Abelian groups, yes: add the commutativity axiom, which can be expressed in the same 2-theory (finite-product theories). But torsion-free groups and nilpotent groups can’t be axiomatized as finite-product theories: I believe torsion-free groups are a geometric theory, while probably nilpotent groups require higher-order logic.

Similarly, when we go back up a level, it’s not obvious that the sub-2-category of toposes within the semantic 2-theory of lccc’s corresponds to any syntactic 2-theory in the same dependent type 3-theory.

• CommentRowNumber75.
• CommentAuthorUrs
• CommentTimeApr 24th 2018
• (edited Apr 24th 2018)

So you could, I guess, define a “geometric type 1-theory” to be a dependent type 1-theory whose corresponding lccc is a topos.

All right! That’s the resolution which I had suggested above, only that I thought you would have a “0” here instead of “1”. Whichever number it is, it is good that we have determined it now!

However, this would not be a “dependent-type-theory refinement of geometric logic”, because “geometric logic” is not just a collection of syntactic 1-theories, but a syntactic 2-theory

That’s just the same issue with new words plugged in. So it’s geometric 1-logic then. The key fact is that logic is but a fragment of type theory. If your terminology does not reflect this, I’d say it’s missing something.

I do appreciate that you are proposing more find-grained terminology. But given the common existing terminology, it is a little disingenuous to behave as if you don’t understand anymore what people say in the classical terminology.

Better than exclaiming “I don’t know what an X-theory is!!” (implying, since you are the expert, that your discussion partner is not making any sense) would be to say “I know what you mean, but just saying ’X-theory’ is, while established practice, a little ambiguous. What you mean is what I suggest to call an ’X-1-theory’, in the terminology that I proposed, to be frank, just the other day.”

• CommentRowNumber76.
• CommentAuthorDavid_Corfield
• CommentTimeApr 24th 2018
• (edited Apr 24th 2018)

Is there still some of the subtlety to capture from that discussion on What is a Theory?

So it seems like a theory (in any given doctrine) can be considered at various different levels of “completedness” or “embodiment.” From least to greatest, we have:

1. An axiomatization in terms of types, operations, and axioms.
2. The seemingly more traditional notion, with generating types and operations fixed, but the “axioms” are closed under implication.
3. Something like a (generalized) operad/multicategory, where the generating types are fixed, but the operations are closed under composition and satisfaction of the axioms.
4. A fully embodied walking model, in which all the type-constructing rules are also fully applied.

and at the end

Perhaps the conclusion to draw is that there is no one “traditional” notion of morphism of theories; we have (at least) four possible categories of theories (per doctrine) and they are all potentially interesting. All the more reason to have good systematic names for them.

Now we have 3-theories, they’ll be more levels to worry about. Is the property-structure-stuff framework worth reviving, as suggested there?

• CommentRowNumber77.
• CommentAuthorDavid_Corfield
• CommentTimeApr 24th 2018

Could a fuller picture than slide 33 of Mike’s talk look something like a pyramid with level $n$ corresponding to $n$-theory in the $n+1$-theory of the level above, and there being a horizontal sequence from the most syntactic to the most semantic, where the passage to the right is driven by closure under entries on a higher level.

Then passage to the right may not be straightforward in that it may be hard to determine identities there (such as in the word problem for groups). And the passage back to the left may be difficult (such as in deriving presentations). Sometimes there are reconstruction theorems which allow passage to the left, but maybe just up to some equivalence of presentation.

Then the task of left passage having formed a sub-n-category at some point in the pyramid may also be problematic, since it may be impossible to reconstruct a presentation within the framework of the pyramid (as with Mike’s nilpotent group example).

• CommentRowNumber78.
• CommentAuthorMike Shulman
• CommentTimeApr 24th 2018

That’s just the same issue with new words plugged in.

No, it’s not! That’s the point I’m making, which is not just a terminological one: not every collection of geometric 1-theories is a 2-theory. In the case of geometric 1-logic, the collection of “geometric 1-theories” does coincide with a particular 2-theory, but in the case of “geometric type theory” the collection of “geometric type 1-theories” does not correspond to any yet-known 2-theory. I think this is what Vickers would have meant. The standard terminology is ambiguous, but the people who use it generally know when they are using “theory” to mean what I would call a 1-theory and when what I would call a 2-theory, and it seems clear to me from Vickers’ usage that “geometric type theory” in this sense should be (but is not yet defined as) what I am calling a 2-theory.

• CommentRowNumber79.
• CommentAuthorMike Shulman
• CommentTimeApr 24th 2018

Urs, check out #74. Do you see how the category of abelian groups corresponds to the syntactic axiom $\forall x \forall y. (x y = y x)$, and how there is no corresponding first-order axiom corresponding to the category of nilpotent groups?

• CommentRowNumber80.
• CommentAuthorDavid_Corfield
• CommentTimeApr 24th 2018

Where does one stop with the hierarchy? If unary, simple and dependent are three kinds of type 3-theories, do they take their place in a 4-theory?

I guess for each $n$ there’s the vacuous $n$-theory. In the doctrine case, this was described as the doctrine of no structure at all.

But perhaps first I’d need to know what a syntactic formulation of a type 3-theory looks like.

• CommentRowNumber81.
• CommentAuthorMike Shulman
• CommentTimeApr 24th 2018

@David #78: Yes, this should generalize somewhat. However, when you get to things like dependent type theory, the distinction between “types” and “terms” and “axioms” is no longer straightforward. And even if we ignore that problem, I think the length of the stuff-structure-property stratification at any fixed level of $n$-theories would probably depend on the category level (or dependency structure) of the theory in question, rather than on $n$, so that you wouldn’t get a pyramid.

@David #80: One would hope, yes, but I have no idea yet what such a “4-theory” would mean.

• CommentRowNumber82.
• CommentAuthorDavid_Corfield
• CommentTimeApr 25th 2018

@Mike#81

I think the length of the stuff-structure-property stratification at any fixed level of $n$-theories would probably depend on the category level (or dependency structure) of the theory in question, rather than on $n$

I thought the $n$ of $n$-theory is supposed to be related to the category level. You have on the semantic side (slide 33):

A 2-theory is a structured 2-category freely generated by something…

and

A 3-theory is a 3-category like “2-categories”,“cartesian monoidal 2-categories”…

• CommentRowNumber83.
• CommentAuthorDavid_Corfield
• CommentTimeApr 25th 2018

I knew bells were ringing. The idea of an iterated dependency was what John Baez and I were discussing in Minneapolis. About the only glimpse of this is in a comment here. Curiously we thought two levels of dependency had a modal flavour.

We didn’t begin to achieve the intricacy of your modal dependent type 2-theory, but those metatypes are pointing somewhere in the direction of your modes.

• CommentRowNumber84.
• CommentAuthorMike Shulman
• CommentTimeApr 25th 2018

I think the $n$ is related to a different category level. (-:O I’m not sure how best to explain this, but maybe it helps to just point out that HoTT is a theory of $(\infty,1)$-categories, but it is still just a 2-theory?

• CommentRowNumber85.
• CommentAuthorDavid_Corfield
• CommentTimeApr 25th 2018

Isn’t that just down to the second number? So the 2-theory HoTT has the $(\infty, \mathbf{2})$-category of $(\infty, 1)$-toposes as semantics.

We’re going wrong in that work in #83 by running the dependency levels together with $n$-groupoid levels. But iterated dependency is a good idea.

• CommentRowNumber86.
• CommentAuthorMike Shulman
• CommentTimeApr 25th 2018

In that case, yes. I’m not sure whether I believe that that’s always the case. But even that is enough to break the pyramid picture, since an $(\infty,2)$-category still has $\infty$ many levels of stuff-structure-property.

• CommentRowNumber87.
• CommentAuthorDavid_Corfield
• CommentTimeApr 26th 2018

So is it right then that as we ascend the ladder of whatever is doing the indexing, the categorical dimension increases: a category of types, a 2-category of modes? Perhaps were one to want to relate different 2-categories of modes, this would require higher indexing. This process tops out somewhere with the trivial $n$-category of higher modes. So a non-modal unary type theory could be seen as a modal unary type theory indexed by a trivial $\mathcal{M}$. (Cf. that “untyped is uni-typed” idea.)

And presumably at all levels of indexing there is something like the spectrum of presentations of the first quote in #76. So in the case of slide 29, I could present that cartesian monoidal 2-category of modes via the generators or, at the other extreme, as the walking model with all rules of the 3-theory applied.

Stuff-structure-property isn’t applying to the groupoidal level but across a given indexing level.

• CommentRowNumber88.
• CommentAuthorMike Shulman
• CommentTimeApr 26th 2018

I’m now writing a Cafe blog post about $n$-theories, and as I do so, I’m coming to the conclusion that I was wrong back in #81, and you right in #82. An $n$-theory does have an $n$-category of models, which means that its models are structured $(n-1)$-categories. I was misled by the fact that HoTT appears to be a theory of $(\infty,1)$-categories, but actually it is a theory of certain 1-categorical presentations of $(\infty,1)$-categories (“tribes”). In particular, it doesn’t have a judgment for higher cells, only for objects and morphisms; the higher cells are represented implicitly as morphisms into a path-type. As such, it is simply a 2-theory (a doctrine), and any particular 1-theory in that doctrine is a structured 1-category. Similarly, Riehl-Shulman directed type theory is implicitly (sort of) about an $(\infty,2)$-category, but explicitly it is only about another particular kind of 1-categorical presentation, so it is again simply a 2-theory.

The spectrum/pyramid of presentations quoted in #76, though, I still believe fails when we get to dependent type theory, where we can’t distinguish any more between types, terms, and axioms, or at least we can’t distinguish them in the sense of giving all the types, then giving all the terms, then giving all the axioms. Peter Lumsdaine explained this to me very well in terms of a ladder of complexity for syntactic presentations and their corresponding universal properties.

• In the simplest case, you can give the entire presentation first and only then start generating things freely from it. For instance, free categories are generated by directed graphs, and you can specify a directed graph without mentioning any part of the structure of a category; only afterwards do you take strings of composable arrows to be the morphisms in your free category. In this case the universal property is a simple adjunction $F : Pres \leftrightarrows Alg : U$ between presentations and algebras.
• In the next simplest case, you have a sequence of “layers of dependency” in which when specifying the generators at layer $n+1$ you have to refer to the free structure generated from the generators in level $n$. For instance, free 2-categories are generated by 2-computads, and in order to specify the 2-cells in a computad you have to already have taken strings of the generating 1-cells as in the free category that they generate, to be the domain and codomain of the 2-cells. In this case the universal property is a sequence of adjunctions $F_n : n Pres \leftrightarrows : Alg : U_n$ defined inductively, with the definition of the category $n Pres$ (and the adjunction $F_n\dashv U_n$) involving the previously defined adjunction $F_{n-1} \dashv U_{n-1}$, as for instance described for globular operads at computad.
• In the final case, such as dependent type theory, there is not even any division into layers. Every generator has a type which can refer arbitrarily to the previous generators and all the structure generated from them freely. In this case one natural way to express the universal property of a “presented object” is as a cell complex, in which each generator is added on by a pushout that glues it to whatever structure was generated freely by the previous generators. A “category of presentations” can only be defined inductive-recursively together with its “free functor”, or perhaps after the fact as the category of coalgebras for an awfs.

In the first two cases, I believe there is a “spectrum of realization” for theories that realizes at some layer and above but not below it. But in the third case I don’t see how to do this.

• CommentRowNumber89.
• CommentAuthorDavid_Corfield
• CommentTimeApr 27th 2018

Interesting times. I wonder if there’s some greater power of expression building in dependency intrinsically in some future dependent type $n$-theory that we haven’t seen before. Looking back I remember Urs being highly impressed by opetopic type theory, in this discussion. But dependent types hadn’t been given definitive expression at that time (#3).

By the way, any further news on the directed HoTT of Denis-Charles (#15)?

• CommentRowNumber90.
• CommentAuthorMike Shulman
• CommentTimeApr 27th 2018

any further news on the directed HoTT of Denis-Charles (#15)?

He’s communicated privately with me about it. I wasn’t convinced by what he had to say at the time, but I look forward to reading more if and when he ever writes it down.

• CommentRowNumber91.
• CommentAuthorMike Shulman
• CommentTimeApr 30th 2018

Another problem with this:

take the image under their equivalence of the toposes inside all locally cartesian closed categories. That gives a 2-category of type theories equivalent to that of toposes. These are the geometric type theories.

that just occurred to me is that in this 2-category the morphisms will correspond to locally cartesian closed functors (between toposes). Surely in the 2-category of geometric type theories the morphisms should be (inverse image functors of) geometric morphisms.

• CommentRowNumber92.
• CommentAuthorUrs
• CommentTimeJun 8th 2018
• (edited Jun 8th 2018)

added pointer to Isaev 18. This seems to be pretty useful.

Peter Lumsdaine pointed to this today as a parallel/alternative to the approach he was presenting here (and Bas Spitters kindly unraveled what the pointer was pointing to)

• CommentRowNumber93.
• CommentAuthorUrs
• CommentTimeJun 8th 2018

or rather, maybe, Isaev 16

• CommentRowNumber94.
• CommentAuthorUrs
• CommentTimeOct 10th 2021