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.
added pointer to
to initial algebra over an endofunctor, higher inductive type and W-type
It seems to me that something’s missing on this page higher inductive type. We have an Idea, and Examples, but is it not possible to say something general, such as
A type theory is said to have/possess higher inductive types if it admits the following type formation schema…
Then what would such a schema look like? That a type, possibly dependent on other types, be formed by any specification of elements and further specification of elements in any types derived by type formation from the previous specification.
I’m sure there’s a better way of putting it, but surely something exists along these lines.
The other Wiki doesn’t help much:
A higher inductive type (HIT) is an inductive type whose constructors can output not just elements of the type itself, but elements of its path space?s and higher path spaces.
Our inductive type isn’t in a great state either.
Defining what a HIT is “in general” is an open research problem. One mostly-precise proposal is in these slides. A more syntactic description of a class of HITs was written by Guillaume here.
Thanks. I’ve added your remarks.
Presumably if HITs are part of HoTT, the internal language of -toposes, then it’s the nature of the latter which determine what HITs ought to be. Is it then largely an issue of finding a good presentation, or is there still something conceptual missing as to what HITs ought to be?
I would say rather that it’s the nature of HITs that will determine the notion of elementary -topos. Grothendieck -toposes, which are the only ones we have an accepted definition of, have many properties that aren’t reflected in type theory due to the finitary nature of type theory; the question is to find appropriate “finitary shadows” of them. For instance, one can construct initial algebras for endofunctors using a transfinite induction argument; thus in type theory we postulate the existence of inductive types. So the question is: what class of “infinitary constructions” that are available in Grothendieck -toposes can be described finitarily by something that deserves the name “higher inductive type”? The slides I linked to give one possible answer.
Thanks! I’ve added those comments to elementary (∞,1)-topos, which I see ends with a link to Hegel’s ’The doctrine of essence’.
Given how concise the definition of an elementary topos can be made, what prospects in the (∞,1)-case? Is the prospect on the final slide of Inductive and higher inductive types likely to pan out?
I still believe in that proposed definition, once a suitable general definition of HIT is found. The definition of elementary 1-topos is arguably “simpler than it has a right to be” because you get a lot for free from the impredicativity of a classifier for all (-1)-types, and that’s especially true when all types are 0-types. By comparison, in a predicative topos we have to assert the existence of finite colimits separately, as well as the existence of all W-types; in an impredicative 1-topos we can construct all finite colimits, and also construct all W-types once we have an NNO. An elementary (∞,1)-topos is more like a predicative 1-topos than an impredicative one, even if we make the subobject classifier impredicative, since mere subobjects don’t tell us nearly as much about -types for , and asking for an impredicative classifier of all objects is inconsistent.
Moreover, one can make an argument that the definition of “elementary topos” — or, more precisely, “elementary W-topos”, i.e. elementary topos with NNO — is not quite right, because although an NNO in a 1-topos suffices to construct all W-types (i.e. inductive types), it does not suffice to construct all higher inductive types (which, of course, also make perfect sense in a 1-category). For instance, in an elementary 1-topos with NNO not all algebraic theories necessarily have free algebras (although finitary ones do). So in that case the “accepted” definition is not just “simpler than it has a right to be” but “simpler than it should be”.
It occurs to me now that the unresolvedness of a general notion of HIT really only applies to the W-topos case, or rather to the strengthening of it that includes HITs as well. That is, we should already be able to give a fine definition of an “elementary (∞,1)-topos”. Until recently I would have resisted that too, feeling that some of the constructions of HoTT that require HITs — notably, the -truncation modalities — ought to exist in any “elementary (∞,1)-topos” worthy of the name. But now that it’s been shown that -truncation can be constructed out of non-recursive HITs (i.e. finite colimits) and an NNO, it might be reasonable to define an elementary (∞,1)-topos to be just a locally cartesian closed (∞,1)-category with finite limits and colimits and sufficiently many object classifiers. I’ve added such a definition to elementary (∞,1)-topos; what do folks think?
it’s been shown that -truncation can be constructed out of non-recursive HITs (i.e. finite colimits) and an NNO
Could you provide a reference or explain how this works?
I put the citation on the page: https://arxiv.org/abs/1701.07538.
Sorry for the following minor point, but anywayy: In the entry it has
…by repeating categorically…
Could we change this, for clarity, to “by repeating category theoretically” or even to “by repeating in terms of constructions of category theory”?
Thanks for the link, Mike. Let me try to reinterpret the construction in a more familiar (at least to me) setting to see if I understand it right.
If is a (connected for simplicity) space and we are trying to construct , then we are picking a particular component of . Since I assumed that is connected, these components are of the form so we just need to identify the right . If we pick a point we can set so that .
This looks quite funky, is this correct? If so, was this already known to topologists in some guise? Topologists tend not to think of things like as spaces, but so much was written about classifying spaces that something like this may be hidden somewhere in the literature.
Urs: of course, feel free to fix it.
It is not quite as simple, as we can see if we plug in the infinite real projective space for . This is a pointed connected 1-type, but the type has (at least) two connected components (of the identity function, and the constant map) so it is not equivalent to (the 1-truncation of) . However, following Karol’s idea, we can still see that is the connected component of the identity function .
It is still the case that if is pointed connected, then following the construction of the paper is a connected component of the space . Using again that is pointed connected, we see that any connected component of is also a connected component of . As we have seen above, it is not necessarily the case that this space is connected. However, we can identify which connected component is the -truncation of : namely that of the pointed map that is induced by the unit .
Unfortunately I’m not familiar enough with the wide literature about classifying types. I would also like to know whether this construction is hidden somewhere in the literature.
(edits: some clarifications, typo)
I just thought that maybe the place to look for something similar is in the literature of reflective sub--categories, because the construction of the (n+1)-truncation can be generalized to the construction of separated objects for a higher modality.
This may or may not be obvious, but this characterization of the truncation seems less “funky” to me when I see it as really just a version of the Yoneda lemma. For any type , the curried identity type is an embedding. Hence, if is pointed and connected, it exhibits as equivalent to a connected component of , namely the connected component of . And if , then , while its connected component in is an -type so that maps into it from are the same as maps into it from . Egbert’s observation is that if we don’t already have then we can use this as a definition of it, with the “small image” construction ensuring that it lives in the same universe.
There is not much literature on reflective sub--categories that I am aware of (except for the left-exact case).
I feel like there should be a connection to k-invariants, but I don’t quite see it yet.
Thank you for the clarification, Egbert. I got distracted by the fact that classifying spaces are connected and forgot that the mapping space between two connected spaces is still typically disconnected.
That’s a very nice paper by the way. The idea of constructing the -truncation by applying -truncation “on path spaces” is a very natural one. This occurred to me before, but I didn’t quite see how to put it together. In the end, I’m quite surprised that the colimits involved are so simple. I was going for geometric realizations myself and I was quite convinced that they would be necessary.
I believe that Egbert was inspired also by the internal construction of the separated-reflection and sheafification functors corresponding to a Lawvere-Tierney topology, which involve taking the image of a suitably reflected singleton embedding into a power object. I’m also surprised at how much one can do with only sequential colimits!
Here’s a thought related to Karol’s idea of which I don’t quite manage to get the details worked out, and it connects to the idea of using geometric realization (and possibly the bar construction), so maybe someone can help me with this:
If you take the Cech nerve of a morphism in an oo-category, that gives you a certain simplicial object of which the colimit is the image (I suppose). Now you can consider the n-skeleton of this simplicial set. Taking the colimits of these are approximations the colimit of the entire simplicial object. In the 1-skeleton case, the colimit is just the join of the map with itself (or rather the domain thereof), because reflexive coequalizers are just pushouts. I would expect that in the general case, the colimit of the n-skeleton might be the (domain of) the n-fold join of f with itself. If this is the case then the join construction would just be another version of the bar construction (and the n-fold joins indeed appear in Milnor’s original work on the construction of a universal bundle of a topological group).
Of course, in HoTT we don’t have such things as simplicial objects, so we can’t go that route. But it would be nice to see whether in simplicial sets there’s a connection.
The join construction itself was motivated by the construction of the real and complex projective spaces in HoTT. And then the idea to get the n-truncations in this particular way was indeed inspired by the construction of separated objects as Mike mentioned.
Why are reflexive coequalizers pushouts homotopically? It’s easy to see in a 1-category but I don’t think I realized that it carried over to the -case.
(The colimit of the 1-skeleton of the Cech nerve, by the way, appears in section 8.7.2 of the HoTT Book, along with a remark 8.7.10 about colimits of higher skeleta.)
Why are reflexive coequalizers pushouts homotopically?
Oh, I think I see: given with and , we have
so the homotopy pushout of the underlying span of a reflexive parallel pair is equivalent to a “homotopy reflexive coequalizer”, which is one way to 1-truncate a geometric realization (but not the one in 8.7.2, which ignores the section).
This, together with Milnor’s version of a bar construction with iterated joins, makes it seem quite plausible to me that the join sequence really does coincide with the skeleta of the Cech nerve. Looking at makes it seem even more plausible: expanding out the definition of a triple join and using the fact that products preserve pushouts, it becomes a colimit over a barycentrically subdivided triangle, which seems likely to correspond to a “2-truncated geometric realization” in a similar way to the above.
Exactly. So one observation you can make with this is that the reflexive coequalizer of the indiscrete reflexive pair of an object is the join of that object with itself. Borrowing the notation from cohesive toposes (because reflexive graphs are cohesive over the universe), we get . As we show in the paper, the mere propositions are precisely the fixed points of .
One can do this in an arbitrary cohesive 1-topos: the composite of the outer adjoints is even a well-pointed endofunctor so that we can directly apply Kelly’s “unified treatment of practically everything and so on” to get a factorization system on any cohesive 1-topos. And apparently, taking a leap of which I don’t claim to be able to fill in all the details, in an -cohesive topos we get the (n-connected,n-truncated)-factorization system.
This seems to be related to, or possibly equivalent to, Mike’s proposed definition of an elementary -topos: we have finite colimits precisely when the reflexive pairs form a cohesive topos over the base topos. I like Mike’s proposal, because it corresponds to the setting in which I like to work.
I have some questions about Mike’s definition:
Good questions, Egbert.
The object classifiers are, in general, unrelated to each other. Moreover, they are merely assumed to exist, not to be given by an operation, so you can’t talk about “the” object classifier associated to a given map. If is a pullback of , then any object classifier that classifies of course also classifies ; but there will also be other object classifiers containing that it doesn’t contain. However, any object classifier that classifies can be embedded in an object classifier that also classifies . In fact, more generally given any object classifier and any map , we can embed in an object classifier that also classifies , simply by finding some object classifier that classifies and using extensivity. In particular, we get a sort of cumulativity for universe extensions: for any object classifier , there is an object classifier in which embeds and which also classifies itself.
I suppose. Van den Berg’s definition of predicative topos even includes all W-types. But that choice has the unfortunate consequence that an impredicative topos is not necessarily a predicative topos – unless you add a NNO or W-types to the definition of impredicative topos too, whereas the extremely standard definition of “elementary topos” doesn’t include them (though frequently topos theorists do need to assume them). In fact, in the -case it seems that there is much less you can do without an NNO even in the impredicative case, due partly to the nature of and partly to the fact that (-1)-truncated impredicativity is less useful when not all types are 0-truncated. So maybe an NNO should be included even in the definition of impredicative elementary -topos? I could be convinced.
Yes, having an NNO is a weaker property than having W-types. In the impredicative 1-topos case it’s actually equivalent; I expect that in the predicative or -case it is strictly weaker. I suppose one might argue for the inclusion of all W-types in an elementary -topos, predicative or not…
I don’t believe it follows. It’s certainly a reasonable condition, but I would not include it in this definition, because I want to stick as closely as possible to something that’s transparently an -ization of elementary 1-toposes, and as far as I know it is not possible to localize those at arbitrary families either. I’m proposing to distinguish between “elementary -toposes”, which transparently categorify elementary 1-toposes and model HoTT without recursive HITs (but, perhaps, with some recursive ordinary inductive types), and some stronger yet-to-be-defined notion that is still “elementary” but also models recursive HITs (with localization as a special case).
That’s an excellent question. I don’t know. I don’t immediately see any way to extract a universal property relative to endomorphisms from a universal property relative to automorphisms; do you have any ideas? (If we could show that, I think it would follow that it is a 0-type, for the same reasons that the usual NNO is a 0-type.)
Let’s try to solve 5, because it would be interesting to see whether any predicative elementary -topos automatically has a natural numbers object.
The first challenge is to identify the type that we hope to be the natural numbers object. We cannot simply say that it is the type of elements of the form , because that would use a natural numbers object. However, maybe we can take the type given by
In other words: is the intersection of all decidable subsets of that contain and are closed under composition by (i.e. they are inductive), writing as an abbreviation for . The proposal for the natural numbers object would then be the total space of . Note that by ranging only over the decidable subset, we ensure that is small, and this ought to be sufficient.
It is clear from the definition of that contains and that is closed under successors. Now we need to find a way to prove that it is initial.
About constructions of -truncations. I seem to recall that Charles Rezk told me about something similar, but I think it was supposed to involve coskeleta of Čech nerves rather than skeleta. I can’t quite recall the details.
Let me also ask a question about Mike’s proposed definition, a simple one compared to those that you are discussing. Many arguments that we would like to carry out in an -topos involve steps like “it is enough to check this condition on fibers”. (For example, the “dual Blakers–Massey” can be verified by saying “check it on fibers where it boils down to connectivity of joins”.) How does this work in an -topos as you defined it? I mean, certainly taking literal fibers as in “pullbacks to the terminal object” is not going to be sufficient. We really need suitable “internal fibers”, right?
Karol: correct. That’s also true in a Grothendieck -topos, of course. From a category-theoretic perspective, “taking internal fibers” means working in a slice category. So the crucial result is the so-called “fundamental theorem of topos theory” that a slice category of a topos is again a topos. I think this is straightforward to prove for the definition I gave: it’s only nontrivial in 1-topos theory if we don’t include dependent exponentials in the definition of 1-topos.
Egbert: I had essentially the same idea, although I was thinking of using all subsets of in the impredicative case. I’m a little doubtful that using only decidable subsets will work, because we also want to be able to prove non-decidable properties by induction. But it would already be interesting (and seems more likely to me on a priori grounds) that we can construct an NNO in the impredicative case. For instance, if we use arbitrary subsets then we can prove “by induction” that is closed under path-concatenation in , and that satisfies all of Peano’s postulates except possibly . To show this last postulate it would suffice to exhibit, for each , a type and an automorphism such that ; this seems “obviously” true since we have arbitrarily large finite types, but I haven’t been able to make it work yet. If we can show all of Peano’s postulates, then I think it follows that is a NNO for hsets at least.
So can we glimpse elementary but not Grothendieck -toposes? We were on the trail of realizability -toposes once.
Okay, lets focus on the impredicative case. Here’s a sketch of a proof that for all .
If has the property that , then we can show that for all , we have . Indeed we have , basically by our assumption, and if , then we certainly have . We get the implication from the fact that is the least inductive subset containing . Thus, we see that is closed under as well as . Now we see that is an automorphism on , and hence that is all of .
We use this automorphism to construct an automorphism on , taking to and to . We can use this automorphism to show that , because is an automorphism on that splits as the sum . However, there exists an automorphism of order three, so this leads to a contradiction.
Hmm… Actually I don’t see how to make the last step work :(
So we have that if for some , then . It is somehow hard to come up with a predicate on that contains , is inductive, but doesn’t contain everything, if we don’t already have a natural numbers object, or to see that leads to an inconsistency. I’ve tried some things but I don’t see how to do it.
I had the same sort of idea to construct an automorphism on , but I also wasn’t able to get it to work. (-:
Good question David. Closely related to what I’m talking about with Egbert, it’s worth noting that the non-Grothendieck elementary 1-topos has no apparent -analogue. Of course object classifiers are a problem, but even worse than that, the category of finite groupoids lacks finite colimits (the coequalizer of is the infinite groupoid ) while the category of finitely presented groupoids lacks finite limits ( is infinite).
I suspect that a fairly easy non-Grothendieck elementary -topos to construct would be a filterquotient.
(I don’t think , which is , is finitely presented because it can be written as the sequential colimit of the , but this is probably a typo and you meant instead of .)
In the setting of a predicative elementary -topos, possibly with an impredicative subobject classifier but without an assumed NNO or W-types, how do you detect that is infinite or not finitely presented?
Regarding possible generalization of the elementary topos to -topos theory:
Not sure if it helps here, but just to recall that there is (at least) one other concept of what “finiteness” of an -groupoid means, namely homotopy type with finite homotopy groups.
At the very least the collection of these has a natural -topos theoretic characterization: they are the coherent objects in the coherent -topos of all -groupoids (here).
Yes, of course I meant . I have no idea how the “B” snuck in there. As for how to detect its infiniteness internally, that’s the whole question! I was just saying that externally, there’s no obvious way to construct an elementary -topos lacking a NNO.
The homotopy types with finite homotopy groups are also not closed under colimits, e.g. does not have finite homotopy groups.
What about simply taking finite colimits of ? This would agree with in the -truncated case, of course.
Regarding the discussion about constructing a natural numbers object, you are basically trying to construct the set from the set , as far as I see. Can’t you simply take the equaliser of and from to ? I am assuming of course that can be constructed, but it is certainly possible if we think of as a quotient of the inductive type defined by , , , and I would certainly believe that can be identified with such a .
I don’t think there is an obvious way to construct absolute value on ; essentially we know about it is that it’s the initial type equipped with a point and an automorphism. Impredicatively, we could construct the smallest sub-type of the universe containing and closed under coproducts with , but this wouldn’t be a NNO since it wouldn’t be a set.
Here is an argument that doesn’t seem to quite work. (-:O First note that with an impredicative , we can define the propositional truncation as . Now with defined as the smallest sub-type of containing (i.e. ) and closed under concatenation with (i.e. ), we can prove propositions about by induction (but no more).
Consider the property “there (merely) exists a set and an automorphism of such that ”. For , this is true; take and the swapping automorphism. Now suppose it to be true for , witnessed by and , and let and define by
Then we can similarly define by
making an automorphism of . Intuitively, however, to show , we need to know not just that but that for all , i.e. we need “strong induction”.
We can try to define by saying that is the smallest sub-type of containing and closed under , and strengthen the inductive hypothesis . But then we have a problem with the base case, since showing that is tantamount to what we’re trying to prove in the first place. Bah.
A really wacky possibility is to consider the sub-type of the universe consisting of all types (merely) equal to for some . If we do have a NNO, then we can prove that these types are all rigid so that this is a set, and hence isomorphic to . However, it’s far from clear to me whether we could show anything of the kind in the absence of an assumed NNO.
In case it was not clear, my #39 was intended as a suggestion for an analogue of in an -setting, not as a construction of a natural numbers object.
Regarding #41: what you describe is a universal property. Surely one can prove that with the obvious point and automorphism has the same universal property, and hence identify with ? Surely this is (predicatively as well) a set?
The point is that we don’t have a definition of “” other than . In particular, we’re not assuming that any recursive inductive types exist, which rules out in particular the one you suggested in #40.
Indeed. In the first instance, looking to construct an integer type rather than a natural numbers type might be more natural (and then one could construct a natural numbers type in the way I suggested), because everything is invertible.
There are ways in which one might try to construct the map for , e.g. in the case of it exhibits as the co-equaliser of and change of signs (i.e. multiplication by ), but that also does not seem very useful here. Possibly one can use the automorphism and its inverse in some clever way, together with the universal property of as a homotopy limit, to construct , but I could not see it after a quick attempt.
Of course, it might also be that something other than is easier to work with.
I think maybe I will ask this question on the HoTT mailing list; it’s been a while since there was an interesting discussion there.
Just a thought, that using an impredicative subobject classifier we can also construct the n-truncation (taking n as an external parameter), as follows:
Now we can take the smallest subuniverse containing and closed under coproduct with , as Mike suggests in #41, and set-truncate it. Not sure how to show that it is the initial object with a point and an endomap, but maybe now we’re getting closer to constructing an NNO.
Good idea; why are we messing around with when there is plenty of infinity already there in the universe? (-: I think an even better approach is to impose some extra structure to make things rigid to start with, rather than 0-truncating afterwards. For instance, consider the type of posets and the smallest subtype of it containing 0 and closed under adding a new top element. As posets, the finite cardinals are rigid, so this will be a 0-type already.
Moreover, it really works! I just blew a few hours coding this up in Coq, and I managed to finish proving the Peano axioms. It’s well-known that the Peano axioms suffice to characterize a NNO in a 1-topos, so we should at least get a recursion principle for eliminating into sets. I think a similar argument should work for eliminating into all types, but I haven’t formulated it carefully yet.
Assuming this works out, it means that any impredicative elementary -topos should automatically have an NNO (although actually writing out the proof in -categorical language might be a serious headache). Moreover, now that I think about it some more, the same argument that constructs W-types from an NNO in the impredicative 1-topos case might in fact still work in the -case (it would be a variant of the same argument constructing recursion from induction for the NNO itself). If so, there is no remaining objection to including an NNO and W-types in the definition of predicative elementary -topos (although it’s still unclear whether they could fail to exist).
I’ve not looked through the proof, but being able to construct a natural numbers object in this setting is quite a fun result! My guess is that it would still work for say -toposes? On the other hand, I don’t quite know what to make of it syntactically. I mean, one surely would not expect a natural numbers type to be derivable from dependent type theory without it. How we should think of your result from that point of view?
Yes, it should work fine for (2,1)-toposes.
In retrospect, I don’t find it very surprising. A NNO is basically an axiom of infinity; it basically says that the natural numbers are the smallest infinite set. And it’s well-known that with an impredicative set of truth values, if you have any X then you can construct the smallest X by intersecting all of the X’s. So all we need is some infinite set, and a type-theoretic universe closed under coproducts is intuitively infinite since it contains all the finite types. Univalence is needed in order to say that latter meaningfully, and the rest is fiddling around to deal with the fact that the universe isn’t 0-truncated.
My line of thought was more the following. If we are assuming universes internal to our type theory, then of course we basically have sitting in there already, and I agree that it is not surprising that your argument works in the presence of univalence and impredicativity. But it seems to me that then the definition of elementary -topos might be too strong. Take the example I suggested earlier, of finite colimits of . This seems like a good candidate for an elementary -topos to me, but I cannot imagine that it has internal universes?
If you mean the -category consisting of finite -colimits of diagrams of 1, then this is the category of finitely presented -groupoids, which fails to even have finite limits, so I don’t think it would be very reasonable to consider it an “elementary -topos”.
If we don’t assume any universes, then we should instead assume descent for our finite -colimits (which follows from universes). This gives a reasonable notion of “--pretopos”. I would still very much like to know whether such a thing must have an NNO, such as by constructing it from , and that remains an open question at this point.
However, what is it that makes a -pretopos into a topos? For 1-categories we assume a subobject classifier. For -categories it would seem weird to assume only a subobject classifier; the natural analogue is an object classifier.
Sorry, closure under finite -limits and -colimits would be closer to what I have in mind. Basically, the crucial distinction seems to me to be between category theory in which we disallow ’infinite tools’ (eg, infinite limits and colimits), and category theory in which we allow them. Thus I also would not object to throwing in further ’finite’ -categorical constructions to obtain my proposed ’elementary -topos’, just not any ’infinite’ ones.
There are two kinds of “infinite tools”, externally infinite and internally infinite. Infinite limits and colimits (in the ordinary sense) are external, and an elementary topos is supposed by meaning of that word to only have “externally-finite” structure. However, some externally-finite things are “internally infinite”, such as an NNO and a universe. An elementary 1-topos is also internally finite, but what we’re seeing here is that there may not be a corresponding notion of elementary -topos (or even (2,1)-topos) that is also internally finite, despite its external finiteness.
In particular, if you close up in under both finite limits and colimits, then you get from a finite colimit and then from a finite limit, and , so that category, whatever it is, has an NNO. So while it doesn’t have externally-infinite constructions, and I agree that it probably doesn’t have universes, it does have at least some “infinite constructions” in the internal sense.
Yes, I agree that external finiteness is what we should be looking at. I agree that this might not lead to internal finiteness. That there are ’infinite’ objects from the point of view of set-theoretic semantics is certainly the case (we should be a bit careful in general though, as being infinite in the set-theoretic semantics might not necessarily correspond to internal infiniteness, but we can brush over that for now). However, when you say that , I’m not sure that I agree yet. By , I would be looking for something similar to the gadget I suggested earlier in the discussion, and far as I know we cannot prove that? In other words, saying that we have the initial object equipped with an automorphism might not be enough, if we cannot go from that to something which has the properties we expect of an ’integer object’. Or?
In particular, I am thinking of Martin-Löf type theory without a natural numbers type. Now, I would certainly expect there to be locally cartesian closed -categories with finite limits and colimits which model this, but which do not model a natural numbers type. As otherwise we would be suggesting that one can always add a natural numbers type to Martin-Löf type theory, which does not seem possible (without universes, etc) to me. So either there is something very special about -topoi (without universes) as opposed to locally cartesian closed -categories which magically produces a natural numbers object, or else the homotopical semantics of Martin-Löf type theory is not as faithful as expected.
Plain MLTT is modeled by FinSet, which certainly has no NNO. In order to get anything interesting about , we need univalence. Without universes, “univalence” here is formulated as large elims out of HITs, which categorically corresponds to “descent” for -colimits, which is indeed a very special property of -toposes.
When I said it was in the context of subcategories of , and there it is certainly true. As I’ve said before, we don’t yet know how to prove internally that deserves that name unless we already have to compare it to.
Yes, then we agree. Thanks!
FWIW, I’ve now fully verified in Coq that this construction of a NNO has the required universal property, eliminating into all types (not just sets).
I’ve been chasing some references. However, it seems that we still do not know whether QIITs have a model in Set, or am I overlooking something?
Hi Bas,
please check out How to cite and record references.
(It’s not just a formality: If you care about the references you give, anchoring and linking them means that readers will be more likely to open them.)
Thanks. I had overlooked that.
I seem to recall that Richard also implemented a feature for a general citation database, but it does not appear to be in the HowTo.
I don’t think that database idea has become a reality yet. But all the more will it help if we format all our references uniformly now, for then there will be a chance to automatically collect them into a database later!
Worth a word on how it can be used to prove functional extensionality from propositional truncation?
Concerning #67, I would argue that “2 element type” is clearer than “booleans”.
Here is Martins email:
My post showing that ||2|| has the universal property of the interval (judgementally for the first order equations and propositional for the second order equations) was in this thread, back in July: https://groups.google.com/forum/#!topic/homotopytypetheory/KyJZKbbr1SM
The proof is easy and short. The only trick is to come up with a suitable proposition to work with.
Assume a type two with points 0,1:2, and let ||-|| denote the (-1)-truncation.
Define I = ||2||, and let seg : |0| = |1| the path arising from the definition of ||-|| (I call it the “truncation path”).
The end-points of I are taken to be |0| and |1|, of course.
Given points x0,x1:X and a path p:x0=x1, we wish to build g:I->X such that g|0|=x0 and g|1|=x1 (judgementally), and ap g seg = p (propositionally).
The trouble is that X is not assumed to be a proposition, and hence the recursion principle for ||-|| can’t be used.
So work instead with paths-from x0, i.e. Sigma(x:X).x0=x, which is a proposition.
Now define f:2->paths-from x0 by
f 0 = (x0, refl) f 1 = (x1, p)By the recursion principle for ||-||, f “extends” to g’:||2||->paths-from x0.
Now define g:||2||->X to be g’ composed with the first projection, which I call “endpoint” in this discussion.
You can check that g|0|=x0 and g|1|=x1 judgementally, by simply expanding the definitions (or with Agda, as the proof refl is accepted).
The proof that ap g seg = p is equally easy. It suffices to consider x0,x1 the same, say x, and p=refl x, in a proof by induction.
We have, in this case,
ap g’ seg = refl (x,refl x),
using the fact that ||2|| is an proposition and hence an set.
Applying the first projection (called “end-point”) to this path, we get
ap end-point (ap g’ seg) = ap end-point (refl (x,refl x)),
Now the lhs is equal to
ap (end-point o g’) seg
and in turn, by the definition of g, to
ap g seg.
And the rhs is refl by the definition of ap. Putting this together, we get
ap g seg = refl
and our proof by induction is complete. Q.E.D.
Moreover, it is known that recursion on I gives induction. However, as far as I know, it doesn’t give it judgementally. Hence in the Agda file I also include a proof that the induction principle for the interval does hold judgementally if we take I=||2||.
Additionally, the above proof technique can be used to show that if a function f:X->Y factors through |-|:X->||X||, then we can find a judgemental factorization. Also in that file. Nicolai then used this to define his mysterious pseudo-inverse of |-|:X->||X||.
To conclude, here is an observation. We discussed constancy (many times) in this list.
Mike’s definition is that f:X->Y is constant iff we are in possession of y:Y such that f=\lambda x.y. Let’s adopt this terminology. (In the Agda file I call this “constant-valued”.)
It is easy to see that f:X->Y has a factor through |-|:X->||X|| iff ||X||->constant f.
Martin
“booleans” is a pretty standard name for the 2-element type. Especially if it is hyperlinked, I don’t think there is a problem with using it.
Does the interval as truncation of the booleans have anything to tell us about cubical type theory?
Does the interval as truncation of the booleans have anything to tell us about cubical type theory?
The main novelty of cubical type theory is to move the interval (and other things) into the primitive syntax. So it is a kind of strictification/rigidification, and the result you are referring to could perhaps be viewed as partial indication that this is reasonable.
It would be more helpful for the change message to indicate what exactly was moved. It appears that what was moved was all the examples of HITs that are also QITs, except for set-quotients. While those examples should certainly be at quotient inductive type, I think it’s also helpful to at least list them at higher inductive type.
Added a section linking to and listing examples from quotient inductive type.
Adding reference
Anonymous
I have added publication data for these two items:
Kristina Sojakova, Higher Inductive Types as Homotopy-Initial Algebras, ACM SIGPLAN Notices 50 1 (2015) 31–42 [arXiv:1402.0761, doi:10.1145/2775051.2676983]
Steve Awodey, Nicola Gambino, Kristina Sojakova, Homotopy-initial algebras in type theory, Journal of the ACM 63 6 (2017) 1–45 [arXiv:1504.05531, doi:10.1145/3006383]
and added a cross-link with initial algebra over an endofunctor
this link in the entry doesn’t work for me:
In any case, I gather that it points not to a writeup but to a research grant landing page, and so I have clarified that in the entry.
to the item
I have added the label
(deprecated)
and added instead pointer to:
added pointer to:
added pointer to:
added these pointers:
Henning Basold, Herman Geuvers, Niels van der Weide, Higher Inductive Types in Programming, Journal of Universal Computer Science 23 1 (2017) 63-88 [pdf, slides pdf]
Niccolò Veltri, Niels van der Weide, Constructing Higher Inductive Types as Groupoid Quotients, Logical Methods in Computer Science 17 2 (2021) [arXiv:2002.08150doi:10.23638/LMCS-17(2:8)2021]
Adding reference
Anonymouse
1 to 87 of 87