Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
A message to Mike:
Hi Mike,
I hear that in Swansea you ended by talking about things related to elementary -toposes. I didn’t get a chance to see anyone’s notes yets. Do you have electronic notes to share?
The links to the lectures are on the Mike’s homepage.
Yes, the link is here. (The link from my front page will probably get moved to the “Notes” section in a while.) The last slide of the last talk contains a tentative and imprecise proposal for a definition of “elementary -topos”: a locally cartesian closed -category with “sufficiently many” object classifiers and “sufficiently many” “higher initial algebras” that its internal homotopy type theory models the univalence axiom and higher inductive types.
Interestingly, I then went to the PSSL in Cambridge where Benno van den Berg proposed a definition of “predicative elementary topos” as a locally cartesian closed pretopos with W-types and satisfying internal WISC. Apparently the reason he wants WISC is to obtain closure under internal sheaf constructions and the ability to define free algebras for algebraic theories. I believe that HITs should be constructible from WISC and suffice for at least some of his applications, and I prefer the idea of including (higher) inductive definitions in the definition over a choice principle. (Note that my proposed -definition is also predicative, although one could make it impredicative.) Benno also proposed to call WISC the “axiom of multiple choice”, replacing the earlier (and somewhat stronger) axiom that has been given that name.
Ah. Thanks. I wasn’t following the webpages.
Nice notes. I have looked at 04 and 01 (gave me a good excuse for procrastinating preparing my seminar for tomorrow ;-). Spotted these typos
01, bottom of slide 14 “to to”
01, slide 21 “to to”
And a remark:
I have started a stub elementary (∞,1)-topos
now I am looking at 03, slide 47, recalling that we discussed this topic recently in another thread:
Let’s try to list as many classes of right proper lccc model categories with cofibrations the monos as we can. That should be fun
As you probably know, Denis-Charles Cisinski has a relevant result in corollary 1.5.7 of his “book”, which implies in particular (if I am not reading it wrong) that every localization of -homotopy theory type (i.e. at products with some ) of an injective model structure on simplicial presheaves is still right proper.
Thanks for the typos. I was probably going to mention these slides (and those from my UCSD seminar) on a blog at some point, probably after I get back from the UK and have time to catch my breath. (-:
Yes, for a reader, especially a reader having with some familiarity with type theory already, it would be better to make the context explicit. But I judged that for the listener who is encountering type theory for the first time and hasn’t yet internalized the word “context”, it was better to leave the context implicit and say verbally “the rules of how we interpret type theory into a category are what produce the ’Z’ here”.
Also, it’s worth noting that right properness is, I believe, more than is strictly necessary. What’s actually needed is that dependent product along a fibration between fibrant objects preserves fibrations. Right properness implies this because (together with cofibrations being the monos) it implies that all acyclic cofibrations are stable under pullback along fibrations.
Te verbal explanations at the site (gently expanding on the material on the slides) were really great! Thanks Mike for an excellent course!
Mike - are there notes from Benno’s talk? I don’t see the rationale in renaming WISC AMC, did he give any justification?
Just had a browse of the abstracts. Man, that conference looked awesome! Stuck on the other side of the world… :-(
I don’t see the rationale in renaming WISC AMC, did he give any justification?
Here is a justification for calling AMC AMC. Maybe this can be used to justify calling WISC AMC.
I have started a stub elementary (∞,1)-topos
If an (,1)-category of (,1)-presheaves is an elementary (,1)-topos is there an (,1)-diaconescu theorem?
Do we have examples of elementary but not Grothendieck -toposes? Perhaps , or some analogue of the Effective topos? Hmm, I see there’s a subject called ’recursive topology’.
I think recursive topology is a sub-subject of that of realizability toposes which is the current topic of P.T. Johnstone (see for example this seminar). The effective topos is one example of an realizability topos.
@David R.: Benno said that the original AMC implies WISC, that they are basically quite similar, and that WISC is a more natural and better axiom which suffices for most anything the original AMC was used for. Insofar as it makes sense to call anything the “axiom of multiple choice” I can see the argument for it being WISC: one wants to make choices indexed by some set , but instead we have a set of covers so that we can always pass to one of them and then make our choices.
@Stephan: Diaconescu’s theorem is just about Grothendieck toposes, but there should certainly be an -version. I can’t find it in HTT, but maybe Urs knows where it is.
@David C.: I don’t know whether there are any “realizability -toposes”; I’ve been hoping to access that question by categorifying exact completion. Finite -groupoids don’t work as well as finite sets, partly because finite colimits of finite -groupoids can yield infinite ones, and partly because the object classifier for finite -groupoids is no longer finite. You could cut off the cardinality of your -groupoids at any inaccessible cardinal smaller than the size of “the universe”, but that will only fail to be a Grothendieck -topos due to our arbitrary choice of where to draw the line between “small” and “large”. And unlike for 1-toposes, as far as I can tell it doesn’t suffice to cut off at a non-regular strong limit cardinal — the object classifiers seem to demand inaccessible bounds.
I do have a couple of ideas for nontrivial non-Grothendieck -toposes. You should be able to glue two -toposes along a lex functor, and if the functor is not accessible then the glued topos may not be Grothendieck. And you should be able to take a filterquotient of an -topos by a filter of subterminal objects. I think I know how to construct the internal homotopy type theory in both of those cases too.
Diaconescu’s theorem is just about Grothendieck toposes, but there should certainly be an (∞,1)-version. I can’t find it in HTT, but maybe Urs knows where it is.
Actually, I don’t. Have been wondering about it myself.
I am pretty sure it is not in HTT. The next place where it would naturally be expected is in Structured Spaces in the section on classifying toposes. But it’s not there either, and also there the -site is assumed to have finite limits.
@Stephan: Diaconescu’s theorem is just about Grothendieck toposes
Thanks for correcting my misconception. Since in the formulation of this theorem occurs a category of presheaves which is not a Grothendieck topos unless we choose the trivial topology I guessed that here ”topos” may mean ”elementary topos”.
Since in the formulation of this theorem occurs a category of presheaves which is not a Grothendieck topos unless we choose the trivial topology
I am not sure what you mean here. The category is a Grothendieck topos – precisely because it is for the trivial topology on .
Do you mean something different?
I am pretty sure it is not in HTT….
Time to ask MO? Or Lurie directly?
Just a minute, let me just check something, somewhere…
Okay, I have checked to see if maybe a discussion of flat -functors was hiding somewhere. But it does not seem to be the case.
van den Berg and Moerdijk have the paper today out which describes AMC/WISC and results pertaining to it in CZF: http://arxiv.org/abs/1204.4045
Mike,
I gather from the last slide of 03 that you are close to showing univalence for all (suitable presentations of) -stack -toposes. That’s great.
There is one more open problem, then, which I hear at least the computer scientists are worried about. I am not sure if I understand it well enough to even state it correctly, but it’s something about whether or not the univalence axiom is “computationally” okay, or if it can be made to be so. I suppose you will know what I mean.
When you have a spare minute, could you maybe say what your perspective on this question is?
If there were a -analogue of the effective topos, given what we know about cohomology being about Homs within -toposes, we should expect something like an ’effective cohomology’. There’s a survey of effective homology, at least.
we should expect something like an ’effective cohomology’.
True. That might be interesting.
There’s a survey of effective homology, at least.
But that’s a coincidence of terminology, unless I am missing something. This survey talks about “effective ways of computing” homology groups.
Hmm, perhaps we need to wait for Mike to crack realizability higher toposes.
I gather from the last slide of 03
Well deduced from the cryptic “check-questionmark” on that arrow. (-: Yes, I think I’m pretty close, at least in the “absolute” case (i.e. starting from simplicial sets). But there’s still a nonzero chance that some technical mistake will cause the whole thing to come crashing down, so let’s not celebrate just yet.
There is one more open problem, then
I think there’s more than one open problem! But the one you mention is indeed an important one — though it’s not the same as realizability toposes.
whether or not the univalence axiom is “computationally” okay
The issue here is that type theory is not just a foundation for mathematics and a calculus for category theory: it’s also a programming language. When you write a term like a computer can evaluate it and get . Most of the types and rules in type theory respect this computational feature, with the result that any term they produce can be algorithmically “computed” into a “value”. In particular, any term you write down of type , no matter how long and complicated, can be evaluated until it becomes a “numeral” of the form — that is, of course, unless it contains free variables. The same is true for terms belonging to other types that have a “canonical form”, like lists or trees of natural numbers, and most any “datatype” arising in everyday programming.
Univalence destroys this property by introducing terms that don’t “compute”. For instance, from univalence we can obtain a term corresponding to the automorphism of which adds one to every even number and subtracts one from every odd number. Then the term has type , but doesn’t “compute” because the computer gets “stuck” on the univalence term.
Univalence shares this problem with any other propery asserted as an “axiom”. For instance, if we assume the law of excluded middle, then we can build a term which is or according as the Goldbach conjecture is true or false, and clearly this term doesn’t “compute” either.
However, univalence is different from LEM in that its “stuck” term has a clear value that it ought to yield, namely . Moreover, we can prove inside type theory (using univalence) that is “equal” to (i.e. connected to it by a path). We just don’t have a “computation rule” which tells the computer how to evaluate it.
Voevodsky has conjectured (I think I’m getting the phrasing of this right) that any term you can write down using univalence can be proven, using univalence, to be equal to a term of canonical form. This seems plausible to me. A more ambitious project would be to find a way of implementing univalence using “computation rules” which would make terms built using univalence actually compute. Some progress has been made in the 2-dimensional case, see here.
(Going back to realizability toposes, those are a particular sort of model for type theory, in which any statement that we make inside the model has a computational interpretation. This question is rather about a meta-theoretical property of the system of type theory itself. There is probably a relationship, but right now I don’t think I can say exactly what it is.)
As for my perspective on this question, so far I have mostly left it to people who I consider better qualified than I am to address it, like Bob Harper and Dan Licata (see above link). I’m not entirely satisfied with that particular result for various reasons, some of which I mentioned in comments to it, but it’s a promising direction.
Another thing worth thinking about is that there are other statements closely related to univalence which may have an easier computational interpretation. For instance, there is the “equivalence induction” principle discussed at the end here, and the principle of “large elims” for higher inductive types (such as the universal cover used in the proof that ). HITs have a similar problem to univalence themselves, but I believe that if we can crack that one, then it might help us with univalence. In particular, there are reasons to believe that using HITs, we can construct a univalent universe, rather than having to assume it — similarly to how object classifiers in -toposes can be constructed using exactness properties and the adjoint functor theorem. Intuitively, the adjoint functor theorem for locally presentable categories is roughly a transfinite construction sort of argument, and most arguments of that form can be rephrased using (higher) inductive definitions.
Thanks, Mike. That’s helpful.
I did see that post by Dan Licata, but didn’t know what to do with it. I keep forgetting the meaning of all these technical terms, such as “canonicity”. But now I guess I’ll remember it.
I keep forgetting the meaning of all these technical terms
Yeah, and it seems like nowhere are they all written down. Plus the type theorists don’t even all use them in the same way. I had just about figured out the difference between inductive “parameters” and “indices” when I found out that Coq has things called “non-uniform parameters” which are basically indices, but are called “parameters” and written like parameters. Only not all indices can be called “non-uniform parameters”, and there’s some internal distinction that I don’t understand at all yet. Blarg.
Maybe the nLab can help record these insights when we have them: canonical form.
I am spending too much time on this, I feel like a drug addict. But here I go on again about “Science of Logic”. Please ignore.
I have been doing this: take the Lawverian dictionary and decipher the book, squarely. I kept wanting to stop, but I keep being sucked in. Because – and it’s eerie – it turns out to make sense.
Still, only tonight did I finally reach the point that I felt like seeing the whole of book 1 clearly before me. Just as Lawvere said, it’s about stratifying by sub(co-)reflections. But Lawvere had stopped translating after the first step, and the eerie thing is that it keeps going and keeps making sense. With the dictionary in hand, it’s crystal clear that we are looking at the preorder of subreflections starting from the minimal going to the maximal. Hegel says it fully explicitly (if we have the Lawverian Babelfish plugged in): Das Wesen is the maximal subcategory, hence the full ambient category itself.
Now, okay, as I said, I am spending too much time on this, and you’ve been asked to ignore this. But with this before me, tonight I for the first time switched to reading book 2.
And it’s yet more eerie. What’s the main topics of book 2, reading with the babelfish? Let me order them like this:
(1) introduction: complete Aufhebung – we are looking at an entire category, no more subcategories;
(2) section 3, especially its chapter 2: possibility and necessity – as we have exhaustively been discussing on the nForum, this is just the modal way of speaking cartesian closure;
(3) section 1, chapter 2: the reflector and the statement that this is the only way to construct proofs of identity — these are the key axioms of identity types;
(4) section 2 “Reflektion is das [Er]Scheinen des Wesens in ihm selbst” as well as section 1, chapter 1, C “Das Wesen scheint zuerst in sich selbst, oder ist Reflexion” – this now verbatim translates to: “The ambient category appears within itself, is reflected.” So what’s that? That’s an object classifier, a type universe.
Let me say this again: under our little translation rule we see that book 2 of the Objective Logic is about
(1) a category
(2) which is cartesian closed
(3) and has identity types/hom-spaces
(4) and an object classifier.
In short: Das Wesen is a locally cartesian closed infinity-category with an object classifier
This is essentially Mike’s proposal for the definition of elementary infinity-toposes in the last slide in Shulman 2012. A fun year to rediscover Hegel 1812.
As I said, please ignore.
Nice!
How does (2) work?
§1190 Actuality as itself the immediate form — unity of inner and outer is thus in the determination of immediacy over against the determination of reflection-into-self; or it is an actuality as against a possibility. Their relation to each other is the third term, the actual determined equally as a being reflected into itself, and this at the same time as a being existing immediately. This third term is necessity.
From what I said elsewhere, for a world-dependent type , at the actual world , there’s a map , sending to .
There’s also a map sending a term to .
Then there’s the adjunction .
Not sure my babelfish is up to it.
How does (2) work?
I always try to first pick out those paragraphs that make clear statements that fit into the Lawverian dictionary. So first I scan for those paragraphs that say explicitly that A and B are the moments of c, because that then is to translate to an adjunction .
Regarding possibility and necessity, the paragraph that does this is §1160 in view of §1159 this says pretty clearly that “absolute reality” is the adjunction between possibility and necessity.
I understand §1190 and other paragraphs as saying that besides this “absolute reality” there is also plain reality which more or less is possibility. If you find this stated more unambiguously, I’d be grateful for a pointer, but in any case I think a robust conclusion is now that section 3 of book two is, globally (absolutely) about the adjunction between possibility and necessity. So under the translation this is local Cartesian closure of the Wesen.
After some discussion about elementary -toposes in another thread, I have updated the proposed definition on the page.
it is arguably not a question about the definition of “elementary -topos”, or even “elementary -topos”,
Is the first supposed to be 1-topos?
Hmm, actually I don’t think the second should even be there. Thanks for catching.
I added the not-completely-trivial argument that we have universes classifying any finite family of morphisms as well, which should probably be assumed explicitly in the predicative case.
Down at the level of 1-toposes, we used the unmarked ’topos’ for elementary topos, and specify ’Grothendieck topos’ for that variety. For historical reasons we have things the other way here, and have (infinity,1)-topos deal with the Grothendieck–Rezk–Lurie variety, while ’elementary’ must be specified.
It’s no doubt too early to propose a switch, but I wanted to ask whether there are occasions on nLab pages where a construction works in the elementary case too. E.g., will we have the tangent (infinity,1)-category of an elementary (infinity,1)-topos still as an elementary (infinity,1)-topos?
A not unrelated question: how does geometric homotopy type theory differ from HoTT?
will we have the tangent (infinity,1)-category of an elementary (infinity,1)-topos still as an elementary (infinity,1)-topos?
Good question. Certainly the tangent category can be constructed elementarily (using ). It’s not immediately obvious to me how constructive is the proof that it’s again a topos, but I would hope that it would work.
how does geometric homotopy type theory differ from HoTT?
I can’t tell from our pages geometric type theory and geometric homotopy type theory what those terms are supposed to mean.
Back then I had been in need for a term of the type theories corresponding to Grothendieck toposes or Grothendieck -toposes. If any.
What does that mean? I don’t know of any such type theory.
The phrase ’geometric type theory’ occurs many times in Steve Vickers’ Locales and toposes as spaces. I can’t make out readily what he means by it.
Re the first part of #39, if it worked out, perhaps that would give a way to define spectrum objects, defined at stable homotopy type as types in .
Well, one thing he says is
In the present state of our knowledge we do not have a formal type theory along these lines
so apparently he doesn’t actually mean anything precise. His Remark 1.34 suggests that what he means is
those constructs that can be carried out in any Grothendieck topos, and are preserved by inverse image functors of geometric morphisms
I guess to start with, one could consider a dependent type theory with just those type constructors that are preserved by inverse image functors: -types, -types (extensional or intensional, according as one is interested in 1-toposes or -toposes), empty type, coproduct types, non-recursive HITs like pushouts, natural numbers, and truncations. That would capture some of what he means, but not all of it because there wouldn’t be “infinite coproducts / unions” as there are in geometric logic.
One could in theory add such things to type theory, using “rules with infinitely many premises”, but it starts to look a lot less like type theory. It occurs to me, though, that a good way around this would be to use adjoint/modal type theory. A Grothendieck topos, after all, is just an elementary topos equipped with a bounded geometric morphism to (or ), so a natural way to study it along with its “Grothendieck-ness” would be to use the “type theory of a geometric morphism” (coincidentally the main example of modal type theory that I used last week in my HoTTEST talk – the video and slides don’t seem to be posted yet). That would amount to incorporating the “meta-theory” used to describe the infinitary constructions of geometric logic into the formal syntax. I’m not quite sure how much this would buy you over the first attempt, though; given that the first attempt already has a NNO; are there infinitary constructions one wants to do for which an NNO is not sufficient?
Re: #43, we do already know how to define spectra in HoTT, hence presumably also in any elementary -topos (as long as it has an NNO).
Ah yes, I’d forgotten about that. So are you able then to develop an abstract chromatic homotopy theory in HoTT? As you have Eilenberg-MacLane spectra already, could you reach higher Morava K-theories?
By the way, the entry under discussion has its own thread here.
For some time back I had been under the clear impression that every kind of category induces its corresponding kind of type theory. In particular I had the understanding that whenever a kind of categories has an internal logic called “XYZ logic”, then just by generalizing attention from sub-objects to all objects one gets what ought to be called “XYZ type theory”. I could swear that I didn’t hallucinate this impression but learned it from discussion here. I had created that entry when I needed to speak about that typal generalization of geometric logic.
I still feel it’s true. But eventually I learned that whatever words I use to speak about type theory, somebody will complain. I feel like it’s only partially my fault. Luckily I got over it and found that I’ll better focus on something else for the next decade, and then check if meanwhile type theory has solidified enough that one can use it without apparently breaking something with every move one makes.
I’d certainly welcome some general thoughts on what counts as a type theory. Does anyone know the approach adopted in Lumsdaine’s A general definition of dependent type theories? And then there’s Mike’s talk (#44) to look forward.
I don’t believe it’s really a question of “solidification”, but of learning to translate between different languages, which is always going to be difficult. But maybe over time we can accumulate more resources to reduce the learning curve; I’m certainly trying to work in that direction myself. It’s true that type theory could use more category-theoretic abstract eyes on it – but in order to make that happen, we need category theorists willing to learn the language as it stands now.
In particular, while it certainly morally “ought” to be true that every kind of category has a corresponding kind of type theory, in the current state of things this isn’t even a precise enough statement to be a conjecture; what do we mean by a “kind of category” or a “kind of type theory”? The work I spoke about at HoTTEST is a step in this direction: for a certain class of categorical structures that can be described in a particular abstract context, we (hope to) be able to prove a general theorem that there is a corresponding type theory.
The problem of defining “a type theory” is an even harder one. It’s easy (well, maybe not that easy, but at least possible (-: ) to give general definitions that are “too general”, in that they include lots of things that may look like a type theory, but aren’t well-behaved in the appropriate type-theoretic senses. If we include definitions like this, then the one I like the best is just “an inductive-inductive type family”. The types in the family are the judgment forms; the dependency structure says which judgements occur in which others (e.g. types occur in term judgments); the constructors give the rules, and the elements of the resulting inductive-inductive family are the derivations. I don’t think I’ve encountered any type theory that couldn’t be described in this way. (Of course one then has to make precise what one means by “an inductive-inductive type family” in general, which isn’t really satisfactorily addressed in the literature yet either.)
(Caveats: here I mean what Bob Harper calls a “formal” type theory – his “computational type theories” are a different beast yet again. Moreover, even in the formal case there’s an extra aspect of “computation” that this description doesn’t address; we can incorporate “judgmental equality” as a particular judgment, but that doesn’t tell us how to “direct” the judgmental equality and turn it into a normalization procedure. And probably there are yet more caveats too.)
In this sense, there is a “tautological” type theory associated to any categorical structure: simply write the categorical structure, along with its equalities at top level if any, as a type dependency structure a la FOLDS, then express all its categorical structure as constructors for an IIT. But this doesn’t produce a well-behaved type theory, e.g. it has explicit cut/substitution, and in many cases infinitely many rules; so it’s not really what we want. What does “well-behaved” mean and how do we get there? Type theory has heuristics and guiding principles, but it’s hard to explain them except by example. My categorical logic notes were an attempt to bridge that gap; I hope one day I’ll be able to come back and polish/publish them.
So are you able then to develop an abstract chromatic homotopy theory in HoTT? As you have Eilenberg-MacLane spectra already, could you reach higher Morava K-theories?
Well, defining spectra is a ways from being able to do everything with them that one can classically. Many constructions on spectra (like defining structured ring spectra and module spectra) require infinitely many coherences, which we don’t have a general method for dealing with in Book HoTT.
Re #50, my chain of thought was sparked off by Clark Barwick’s plea. It sounded like he should be interested in what can be done synthetically in homotopy theory.
Back here you said some objections you raised were only ’nitpicky’ against a claim that
(∞,1) -category theory, homotopy theory, and homotopy type theory are all fundamentally the same subject.
But if one can’t get very far with central notions such as ring spectra, and other constructions needed for chromatic homotopy theory, that surely places severe limits on such a claim.
I see that people are turning to model theory for inspiration:
Sounds like a homotopified model theory is needed:
To extract results from our equivalences, one would like an analogous transfer principle in the ∞-categorical setting. In lieu of such an ∞-categorical transfer principle, we provide arguments that establish the transfer principle for specific problems that we are interested in.
We always seem to come back to that model theory-category theory issue, e.g., The Ax-Grothendieck Theorem According to Category Theory.
Hmm, did anything interesting happen with Tom Leinster’s category theoretic work on ultraproducts?
I was careful to specify “in Book HoTT” in #50; there are other proposals, like two-level type theory, in which one would be able to define structured ring spectra (though no one has done it yet). I don’t know whether that will eventually be the best way of doing it, but it’s certainly worth working on. Remember that homotopy type theory is a very young subject, with a fairly small group of people working on it so far; it’s not surprising that we haven’t yet figured out the best way of doing things.
We should perhaps start a page on two-level type theory, if it’s here to stay (at least for the time being). Are these the best references?
Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus, Extending Homotopy Type Theory with Strict Equality, ( arXiv:1604.03799)
Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Two-Level Type Theory and Applications, (arXiv:1705.03307)
Yes.
I see there’s a new paper out
Any comment, Mike? The author raises the question as to whether your proposed notion and his are equivalent, and leans towards ’no’.
Doesn’t Remark 3.17 say ’yes’?
Meh, somehow I missed that. :-/ Aside from my stupid question, any insights?
I see there’s a new paper out
1 to 59 of 59