Not signed in (Sign In)

Start a new discussion

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeJul 21st 2015
    • (edited Jul 21st 2015)
    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 3rd 2017

    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.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeMar 3rd 2017

    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.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 3rd 2017

    Thanks. I’ve added your remarks.

    Presumably if HITs are part of HoTT, the internal language of (,1)(\infty, 1)-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?

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeMar 3rd 2017

    I would say rather that it’s the nature of HITs that will determine the notion of elementary (,1)(\infty,1)-topos. Grothendieck (,1)(\infty,1)-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 (,1)(\infty,1)-toposes can be described finitarily by something that deserves the name “higher inductive type”? The slides I linked to give one possible answer.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 4th 2017
    • (edited Mar 4th 2017)

    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?

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeMar 5th 2017

    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 nn-types for n>0n\gt 0, 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 nn-truncation modalities — ought to exist in any “elementary (∞,1)-topos” worthy of the name. But now that it’s been shown that nn-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?

    • CommentRowNumber8.
    • CommentAuthorKarol Szumiło
    • CommentTimeMar 5th 2017

    it’s been shown that nn-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?

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeMar 5th 2017

    I put the citation on the page: https://arxiv.org/abs/1701.07538.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeMar 6th 2017

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

    • CommentRowNumber11.
    • CommentAuthorKarol Szumiło
    • CommentTimeMar 6th 2017

    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 AA is a (connected for simplicity) space and we are trying to construct A n+1\| A \|_{n + 1}, then we are picking a particular component of 𝒰 A\mathcal{U}^A. Since I assumed that AA is connected, these components are of the form (BAutF) A(\mathrm{B}\,\mathrm{Aut} F)^A so we just need to identify the right FF. If we pick a point aAa \in A we can set F=Ω(A,a) nF = \| \Omega(A, a) \|_n so that A n+1=(BAut(Ω(A,a) n)) A\| A \|_{n + 1} = (\mathrm{B}\,\mathrm{Aut} (\| \Omega(A, a) \|_n) )^A.

    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 𝒰 A\mathcal{U}^A as spaces, but so much was written about classifying spaces that something like this may be hidden somewhere in the literature.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeMar 6th 2017

    Urs: of course, feel free to fix it.

    • CommentRowNumber13.
    • CommentAuthorEgbertRijke
    • CommentTimeMar 6th 2017
    • (edited Mar 6th 2017)

    It is not quite as simple, as we can see if we plug in the infinite real projective space BAut(2)BAut(2) for AA. This is a pointed connected 1-type, but the type BAut(Ω(BAut(2)) 0) BAut(2)=BAut(2) BAut(2)BAut(\|\Omega(BAut(2))\|_0)^{BAut(2)}=BAut(2)^{BAut(2)} has (at least) two connected components (of the identity function, and the constant map) so it is not equivalent to (the 1-truncation of) BAut(2)BAut(2). However, following Karol’s idea, we can still see that BAut(2)BAut(2) is the connected component of the identity function BAut(2)BAut(2)BAut(2)\to BAut(2).

    It is still the case that if AA is pointed connected, then following the construction of the paper A n+1\|A\|_{n+1} is a connected component of the space 𝒰 A\mathcal{U}^A. Using again that AA is pointed connected, we see that any connected component of 𝒰 A\mathcal{U}^A is also a connected component of BAut(ΩA n) ABAut(\|\Omega A\|_n)^A. 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 (n+1)(n+1)-truncation of AA: namely that of the pointed map ABAut(ΩA n)A\to BAut(\|\Omega A\|_n) that is induced by the unit ΩAΩA n\Omega A \to \|\Omega A\|_n.

    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)

    • CommentRowNumber14.
    • CommentAuthorEgbertRijke
    • CommentTimeMar 6th 2017

    I just thought that maybe the place to look for something similar is in the literature of reflective sub-\infty-categories, because the construction of the (n+1)-truncation can be generalized to the construction of separated objects for a higher modality.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMar 6th 2017

    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 BB, the curried identity type B𝒰 BB \to \mathcal{U}^B is an embedding. Hence, if BB is pointed and connected, it exhibits BB as equivalent to a connected component of 𝒰 B\mathcal{U}^B, namely the connected component of ΩB\Omega B. And if B=A n+1B = \Vert A\Vert_{n+1}, then ΩB=ΩA n+1=ΩA n\Omega B = \Omega \Vert A \Vert_{n+1} = \Vert \Omega A \Vert_n , while its connected component in 𝒰\mathcal{U} is an n+1n+1-type so that maps into it from BB are the same as maps into it from AA. Egbert’s observation is that if we don’t already have A n+1\Vert A \Vert_{n+1} then we can use this as a definition of it, with the “small image” construction ensuring that it lives in the same universe.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeMar 6th 2017

    There is not much literature on reflective sub-\infty-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.

    • CommentRowNumber17.
    • CommentAuthorKarol Szumiło
    • CommentTimeMar 6th 2017

    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 (n+1)(n + 1)-truncation by applying nn-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.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeMar 6th 2017

    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!

    • CommentRowNumber19.
    • CommentAuthorEgbertRijke
    • CommentTimeMar 6th 2017

    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.

    • CommentRowNumber20.
    • CommentAuthorEgbertRijke
    • CommentTimeMar 6th 2017

    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.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeMar 7th 2017

    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 \infty-case.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMar 7th 2017

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

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeMar 7th 2017

    Why are reflexive coequalizers pushouts homotopically?

    Oh, I think I see: given f,g:ABf,g:A\to B with s:BAs:B\to A and fs=gs=1f s = g s = 1, we have

    ( p:BX q:BX(pf=qg)) = p:BX q:BX H:pf=qg K:p=q(Hs=K) = p:BX q:BX K:p=q H:pf=qg(Hs=K) = p:BX H:pf=pg(Hs=1)\begin{aligned} \Big(\sum_{p:B\to X} \sum_{q:B\to X} (p f = q g)\Big) &= \sum_{p:B\to X} \sum_{q:B\to X} \sum_{H:p f = q g} \sum_{K:p=q} (H s = K)\\ &= \sum_{p:B\to X} \sum_{q:B\to X} \sum_{K:p=q} \sum_{H:p f = q g} (H s = K)\\ &= \sum_{p:B\to X} \sum_{H:p f = p g} (H s = 1) \end{aligned}

    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 n=2n=2 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.

    • CommentRowNumber24.
    • CommentAuthorEgbertRijke
    • CommentTimeMar 7th 2017

    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 π((X))=X*X\pi(\nabla(X))=X\ast X. As we show in the paper, the mere propositions are precisely the fixed points of π\pi\circ\nabla.

    One can do this in an arbitrary cohesive 1-topos: the composite of the outer adjoints π\pi\circ\nabla 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 \infty-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 \infty-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:

    1. I found that I use global function extensionality (regardless of the size of the types involved). From univalence you only get function extensionality for small types, but the object classifiers in the definition are seemingly unrelated to each other (maybe I’m missing something) so I’m not sure if global function extensionality follows just from having enough object classifiers. Shouldn’t it be the case that if you have a pullback square (say, involving f *pf^\ast p and pp), then the object classifier associated to f *pf^\ast p embeds in the object classifier associated to pp, or something along those lines?
    2. I would like it more if the NNO would be in the predicative \infty-topos by assumption (because that way you can do stuff like internal long exact sequences, sequential colimits, n-truncations, and so on), but of course I could live with having to say “predicative \infty-topos with NNO”. The point is maybe that with an NNO they become more interesting objects of study?
    3. Why is there both an assumption about an NNO and about W-types in the definition of elementary \infty-topos? Isn’t it the case in this setting that the NNO is just the W-type associated to the map 1 -> 1+1 as usual?
    4. Would it be reasonable to ask that in an elementary \infty-topos you can localize at an arbitrary class of maps? This is not covered (as far as I can see, but maybe it follows) in the current proposed definition.
    • CommentRowNumber25.
    • CommentAuthorEgbertRijke
    • CommentTimeMar 7th 2017
    1. In the current proposed definition of a predicative elementary \infty-topos, I suppose that you can show that the loop space of the circle is the initial object with a point and an automorphism. I don’t think you need an NNO for that. Would you still be able to show that this is a 0-type, and then extract the NNO from this?
    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeMar 7th 2017

    Good questions, Egbert.

    1. 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 f *pf^\ast p is a pullback of pp, then any object classifier that classifies pp of course also classifies f *pf^\ast p; but there will also be other object classifiers containing f *pf^\ast p that it doesn’t contain. However, any object classifier that classifies f *pf^\ast p can be embedded in an object classifier that also classifies pp. In fact, more generally given any object classifier q:U˜Uq:\tilde{U} \to U and any map p:XYp:X\to Y, we can embed qq in an object classifier that also classifies pp, simply by finding some object classifier that classifies q+p:U˜+XU+Yq+p : \tilde{U} + X \to U + Y and using extensivity. In particular, we get a sort of cumulativity for universe extensions: for any object classifier q:U˜Uq:\tilde{U} \to U, there is an object classifier in which qq embeds and which also classifies U1U\to 1 itself.

    2. 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 \infty-case it seems that there is much less you can do without an NNO even in the impredicative case, due partly to the \infty nature of \infty 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 (,1)(\infty,1)-topos? I could be convinced.

    3. 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 \infty-case it is strictly weaker. I suppose one might argue for the inclusion of all W-types in an elementary (,1)(\infty,1)-topos, predicative or not…

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

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

    • CommentRowNumber27.
    • CommentAuthorEgbertRijke
    • CommentTimeMar 7th 2017

    Let’s try to solve 5, because it would be interesting to see whether any predicative elementary \infty-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 loop nloop^n, because that would use a natural numbers object. However, maybe we can take the type N:ΩS 1TypeN:\Omega S^1\to \mathrm{Type} given by

    N(x):=Π (A:ΩS 12)Π (p:A(refl))Π (i:Π (y:ΩS 1)A(y)A(loopy))A(x)N(x):=\Pi_{(A:\Omega S^1\to 2)}\Pi_{(p:A(\mathrm{refl}))}\Pi_{(i:\Pi_{(y:\Omega S^1)} A(y)\to A(\mathrm{loop}\cdot y))}A(x)

    In other words: NN is the intersection of all decidable subsets of ΩS 1\Omega S^1 that contain refl\mathrm{refl} and are closed under composition by loop\mathrm{loop} (i.e. they are inductive), writing A(x)A(x) as an abbreviation for A(x)=trueA(x)=\mathrm{true}. The proposal for the natural numbers object would then be the total space of NN. Note that by ranging only over the decidable subset, we ensure that N(x)N(x) is small, and this ought to be sufficient.

    It is clear from the definition of NN that NN contains refl\mathrm{refl} and that NN is closed under successors. Now we need to find a way to prove that it is initial.

    • CommentRowNumber28.
    • CommentAuthorKarol Szumiło
    • CommentTimeMar 8th 2017

    About constructions of nn-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 (,1)(\infty, 1)-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 (,1)(\infty, 1)-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?

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeMar 8th 2017

    Karol: correct. That’s also true in a Grothendieck (,1)(\infty,1)-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.

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeMar 8th 2017

    Egbert: I had essentially the same idea, although I was thinking of using all subsets of ΩS 1\Omega S^1 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 NN is closed under path-concatenation in ΩS 1\Omega S^1, and that NN satisfies all of Peano’s postulates except possibly 0succ(n)0\neq succ(n). To show this last postulate it would suffice to exhibit, for each n:Nn:N, a type XX and an automorphism f:XXf:X\to X such that f n+1idf^{n+1} \neq id; 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 NN is a NNO for hsets at least.

    • CommentRowNumber31.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 8th 2017

    So can we glimpse elementary but not Grothendieck (,1)(\infty, 1)-toposes? We were on the trail of realizability (,1)(\infty, 1)-toposes once.

    • CommentRowNumber32.
    • CommentAuthorEgbertRijke
    • CommentTimeMar 8th 2017
    • (edited Mar 8th 2017)

    Okay, lets focus on the impredicative case. Here’s a sketch of a proof that succ(n)0\mathrm{succ}(n)\neq 0 for all n:Nn:N.

    If n:Nn:N has the property that succ(n)=0\mathrm{succ}(n)=0, then we can show that for all x:ΩS 1x:\Omega S^1, we have N(x)N(loop 1x)N(x)\to N(\mathrm{loop}^{-1}\cdot x). Indeed we have N(0)N(loop 10)N(0)\wedge N(\mathrm{loop}^{-1}\cdot 0), basically by our assumption, and if N(x)N(loop 1x)N(x)\wedge N(\mathrm{loop}^{-1}\cdot x), then we certainly have N(loopx)N(loop 1loopx)N(\mathrm{loop}\cdot x)\wedge N(\mathrm{loop}^{-1}\cdot\mathrm{loop}\cdot x). We get the implication from the fact that NN is the least inductive subset containing 00. Thus, we see that NN is closed under succ\mathrm{succ} as well as succ 1\mathrm{succ}^{-1}. Now we see that succ\mathrm{succ} is an automorphism on NN, and hence that NN is all of ΩS 1\Omega S^1.

    We use this automorphism to construct an automorphism ee on N+NN+N, taking inl(n)\mathrm{inl}(n) to inr(n)\mathrm{inr}(n) and inr(n)\mathrm{inr}(n) to inl(succ(n))\mathrm{inl}(\mathrm{succ}(n)). We can use this automorphism to show that looploop=0\mathrm{loop}\cdot\mathrm{loop}=0, because e 2e^2 is an automorphism on N+NN+N that splits as the sum succ+succ\mathrm{succ}+\mathrm{succ}. However, there exists an automorphism of order three, so this leads to a contradiction.

    • CommentRowNumber33.
    • CommentAuthorEgbertRijke
    • CommentTimeMar 8th 2017

    Hmm… Actually I don’t see how to make the last step work :(

    So we have that if succ(n)=0succ(n)=0 for some n:Nn:N, then N=ΩS 1N=\Omega S^1. It is somehow hard to come up with a predicate on ΩS 1\Omega S^1 that contains 00, is inductive, but doesn’t contain everything, if we don’t already have a natural numbers object, or to see that N=ΩS 1N=\Omega S^1 leads to an inconsistency. I’ve tried some things but I don’t see how to do it.

    • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeMar 9th 2017

    I had the same sort of idea to construct an automorphism on N+NN+N, but I also wasn’t able to get it to work. (-:

    • CommentRowNumber35.
    • CommentAuthorMike Shulman
    • CommentTimeMar 9th 2017
    • (edited Mar 9th 2017)

    Good question David. Closely related to what I’m talking about with Egbert, it’s worth noting that the non-Grothendieck elementary 1-topos FinSetFinSet has no apparent (,1)(\infty,1)-analogue. Of course object classifiers are a problem, but even worse than that, the category of finite groupoids lacks finite colimits (the coequalizer of 111\rightrightarrows 1 is the infinite groupoid S 1S^1) while the category of finitely presented groupoids lacks finite limits (ΩS 1\Omega S^1 is infinite).

    I suspect that a fairly easy non-Grothendieck elementary (,1)(\infty,1)-topos to construct would be a filterquotient.

    • CommentRowNumber36.
    • CommentAuthorEgbertRijke
    • CommentTimeMar 9th 2017

    (I don’t think BS 1BS^1, which is P \mathbb{C}P^\infty, is finitely presented because it can be written as the sequential colimit of the P n\mathbb{C}P^n, but this is probably a typo and you meant S 1S^1 instead of BS 1B S^1.)

    In the setting of a predicative elementary \infty-topos, possibly with an impredicative subobject classifier but without an assumed NNO or W-types, how do you detect that ΩS 1\Omega S^1 is infinite or not finitely presented?

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeMar 9th 2017
    • (edited Mar 9th 2017)

    Regarding possible generalization of the elementary topos FinSetFinSet to \infty-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 \infty-groupoid means, namely homotopy type with finite homotopy groups.

    At the very least the collection of these has a natural \infty-topos theoretic characterization: they are the coherent objects in the coherent \infty-topos of all \infty-groupoids (here).

    • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeMar 9th 2017

    Yes, of course I meant ΩS 1\Omega S^1. 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 (,1)(\infty,1)-topos lacking a NNO.

    The homotopy types with finite homotopy groups are also not closed under colimits, e.g. S 1=coeq(11)S^1 = coeq(1\rightrightarrows 1) does not have finite homotopy groups.

  1. What about simply taking finite colimits of 11? This would agree with FinSetFinSet in the 00-truncated case, of course.

    • CommentRowNumber40.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2017
    • (edited Mar 9th 2017)

    Regarding the discussion about constructing a natural numbers object, you are basically trying to construct the set \mathbb{N} from the set \mathbb{Z}, as far as I see. Can’t you simply take the equaliser of ||\left| - \right| and idid from \mathbb{Z} to \mathbb{Z}? I am assuming of course that ||\left| - \right| can be constructed, but it is certainly possible if we think of \mathbb{Z} as a quotient of the inductive type defined by zero:zero : \mathbb{Z}, pos:pos : \mathbb{Z} \rightarrow \mathbb{Z}, neg:neg : \mathbb{Z} \rightarrow \mathbb{Z}, and I would certainly believe that ΩS 1\Omega S^{1} can be identified with such a \mathbb{Z}.

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeMar 10th 2017

    I don’t think there is an obvious way to construct absolute value on ΩS 1\Omega S^1; 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 00 and closed under coproducts with 11, but this wouldn’t be a NNO since it wouldn’t be a set.

    • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTimeMar 10th 2017
    • (edited Mar 10th 2017)

    Here is an argument that doesn’t seem to quite work. (-:O First note that with an impredicative PropProp, we can define the propositional truncation as A= P:Prop(AP)P\Vert A \Vert = \prod_{P:Prop} (A\to P) \to P. Now with NN defined as the smallest sub-type of ΩS 1\Omega S^1 containing reflrefl (i.e. 00) and closed under concatenation with looploop (i.e. succsucc), we can prove propositions about n:Nn:N by induction (but no more).

    Consider the property P(n)=P(n)= “there (merely) exists a set XX and an automorphism ff of 1+X1+X such that f n+1(inl())inl()f^{n+1}(inl(\star)) \neq inl(\star)”. For n=0n=0, this is true; take X=1X=1 and the swapping automorphism. Now suppose it to be true for nn, witnessed by XX and ff, and let Y=1+XY=1+X and define g:1+Y1+Yg:1+Y\to 1+Y by

    g(inl()) =inr(f(inl())) g(inr(inl())) =inl() g(inr(inr(x))) =inr(f(inr(x))) \begin{aligned} g(inl(\star)) &= inr(f(inl(\star)))\\ g(inr(inl(\star))) &= inl(\star)\\ g(inr(inr(x))) &= inr(f(inr(x))) \end{aligned}

    Then we can similarly define g 1:1+Y1+Yg^{-1}:1+Y\to 1+Y by

    g 1(inl()) =inr(inl()) g 1(inr(y)) ={inr(inr(x))) f 1(y)=inr(x) inl() f 1(y)=inl() \begin{aligned} g^{-1}(inl(\star)) &= inr(inl(\star))\\ g^{-1}(inr(y)) &= \begin{cases} inr(inr(x))) &\qquad f^{-1}(y) = inr(x)\\ inl(\star) &\qquad f^{-1}(y) = inl(\star) \end{cases} \end{aligned}

    making gg an automorphism of 1+Y1+Y. Intuitively, however, to show g n+2(inl())inl()g^{n+2}(inl(\star)) \neq inl(\star), we need to know not just that f n+1(inl())inl()f^{n+1}(inl(\star)) \neq inl(\star) but that f m+1(inl())inl()f^{m+1}(inl(\star)) \neq inl(\star) for all mnm\le n, i.e. we need “strong induction”.

    We can try to define nmn\le m by saying that {mnm}\{ m \mid n\le m\} is the smallest sub-type of NN containing nn and closed under succsucc, and strengthen the inductive hypothesis P(n)P(n). But then we have a problem with the base case, since showing that n0n=0n\le 0 \to n=0 is tantamount to what we’re trying to prove in the first place. Bah.

    • CommentRowNumber43.
    • CommentAuthorMike Shulman
    • CommentTimeMar 10th 2017

    A really wacky possibility is to consider the sub-type of the universe consisting of all types (merely) equal to BAut(n)B Aut(n) for some n2,6n\neq 2,6. 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 \mathbb{N}. However, it’s far from clear to me whether we could show anything of the kind in the absence of an assumed NNO.

    • CommentRowNumber44.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 10th 2017
    • (edited Mar 10th 2017)

    In case it was not clear, my #39 was intended as a suggestion for an analogue of FinSetFinSet in an (,1)(\infty,1)-setting, not as a construction of a natural numbers object.

    Regarding #41: what you describe is a universal property. Surely one can prove that \mathbb{Z} with the obvious point and automorphism has the same universal property, and hence identify ΩS 1\Omega S^{1} with \mathbb{Z}? Surely this \mathbb{Z} is (predicatively as well) a set?

    • CommentRowNumber45.
    • CommentAuthorMike Shulman
    • CommentTimeMar 10th 2017

    The point is that we don’t have a definition of “\mathbb{Z}” other than ΩS 1\Omega S^1. In particular, we’re not assuming that any recursive inductive types exist, which rules out in particular the one you suggested in #40.

    • CommentRowNumber46.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 11th 2017
    • (edited Mar 11th 2017)

    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 ||\left| - \right| for ΩS 1\Omega S^{1}, e.g. in the case of \mathbb{Z} it exhibits \mathbb{Z} as the co-equaliser of idid and change of signs (i.e. multiplication by 1-1), 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 ΩS 1\Omega S^{1} as a homotopy limit, to construct ||\left| - \right|, but I could not see it after a quick attempt.

    Of course, it might also be that something other than ΩS 1\Omega S^{1} is easier to work with.

    • CommentRowNumber47.
    • CommentAuthorMike Shulman
    • CommentTimeMar 11th 2017

    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.

    • CommentRowNumber48.
    • CommentAuthorEgbertRijke
    • CommentTimeMar 11th 2017

    Just a thought, that using an impredicative subobject classifier we can also construct the n-truncation (taking n as an external parameter), as follows:

    1. First we observe that from the impredicative encoding of the propositional truncation we also obtain an impredicative encoding of the image of any map f:AXf : A \to X. There are multpiple ways to do this, given that propositional truncation determines an orthogonal factorization system on \mathcal{E}. It isn’t clear (to me, at least) that this image is small whenever AA is small and XX is locally small, so let’s see where we get if the image is large.
    2. Since the impredicative encoding of propositional truncation ranges over all propositions, the universal property isn’t limited to a specific universe. I thought that this was worth observing, because the impredicative encoding of for instance the natural numbers gives rise to an induction principle that can only be applied to types in the impredicative universe. We conclude that the image of a map also has the universal property of the image with respect to all embeddings, regardless of their size.
    3. Now suppose AA is an object that is classified by 𝒰\mathcal{U}, and suppose we have n-truncation. We can construct the image of 𝒴 n:AA𝒰\mathcal{Y}_n:A\to A\to \mathcal{U} given by 𝒴 n(a,b):=a=b n\mathcal{Y}_n(a,b):=\|a=b\|_n. The proof that im(𝒴 n)\mathrm{im}(\mathcal{Y}_n) is (n+1)-truncated and has the universal property doesn’t use an internal natural numbers object as far as I can see, so it seems that it should be possible to give a similar argument in an elementary \infty-topos. However, we should observe that A n+1\|A\|_{n+1} is in a higher universe than A n\|A\|_n, unless we’re able to show that the image of a map from a small type into a locally small type is small.
    4. This way we obtain the (n-connected,n-truncated) factorization system on an elementary \infty-topos \mathcal{E} (without assumed NNO or W-types), even though it is possible that the ‘universe levels’ aren’t properly respected.

    Now we can take the smallest subuniverse containing 00 and closed under coproduct with 11, 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.

    • CommentRowNumber49.
    • CommentAuthorMike Shulman
    • CommentTimeMar 12th 2017

    Good idea; why are we messing around with S 1S^1 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 (,1)(\infty,1)-topos should automatically have an NNO (although actually writing out the proof in \infty-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 \infty-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 (,1)(\infty,1)-topos (although it’s still unclear whether they could fail to exist).

    • CommentRowNumber50.
    • CommentAuthorMike Shulman
    • CommentTimeMar 12th 2017
  2. 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 (2,1)(2,1)-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?

    • CommentRowNumber52.
    • CommentAuthorMike Shulman
    • CommentTimeMar 13th 2017

    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.

  3. My line of thought was more the following. If we are assuming universes internal to our type theory, then of course we basically have \mathbb{N} 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 (,1)(\infty,1)-topos might be too strong. Take the example I suggested earlier, of finite colimits of 11. This seems like a good candidate for an elementary (,1)(\infty,1)-topos to me, but I cannot imagine that it has internal universes?

    • CommentRowNumber54.
    • CommentAuthorMike Shulman
    • CommentTimeMar 13th 2017

    If you mean the (,1)(\infty,1)-category consisting of finite \infty-colimits of diagrams of 1, then this is the category of finitely presented \infty-groupoids, which fails to even have finite limits, so I don’t think it would be very reasonable to consider it an “elementary (,1)(\infty,1)-topos”.

    If we don’t assume any universes, then we should instead assume descent for our finite \infty-colimits (which follows from universes). This gives a reasonable notion of “(,1)(\infty,1)-Π\Pi-pretopos”. I would still very much like to know whether such a thing must have an NNO, such as by constructing it from ΩS 1\Omega S^1, and that remains an open question at this point.

    However, what is it that makes a Π\Pi-pretopos into a topos? For 1-categories we assume a subobject classifier. For (,1)(\infty,1)-categories it would seem weird to assume only a subobject classifier; the natural analogue is an object classifier.

    • CommentRowNumber55.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 13th 2017
    • (edited Mar 13th 2017)

    Sorry, closure under finite (,1)(\infty,1)-limits and (,1)(\infty,1)-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’ (,1)(\infty,1)-categorical constructions to obtain my proposed ’elementary (,1)(\infty,1)-topos’, just not any ’infinite’ ones.

    • CommentRowNumber56.
    • CommentAuthorMike Shulman
    • CommentTimeMar 13th 2017

    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 (,1)(\infty,1)-topos (or even (2,1)-topos) that is also internally finite, despite its external finiteness.

    In particular, if you close up 11 in Gpd\infty Gpd under both finite limits and colimits, then you get S 1S^1 from a finite colimit and then =ΩS 1\mathbb{Z} = \Omega S^1 from a finite limit, and \mathbb{Z} \cong \mathbb{N}, 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.

  4. 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 =ΩS 1\mathbb{Z} = \Omega S^{1}, I’m not sure that I agree yet. By \mathbb{Z}, 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?

    • CommentRowNumber58.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 13th 2017
    • (edited Mar 13th 2017)

    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 (,1)(\infty,1)-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 (,1)(\infty,1)-topoi (without universes) as opposed to locally cartesian closed (,1)(\infty,1)-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.

    • CommentRowNumber59.
    • CommentAuthorMike Shulman
    • CommentTimeMar 14th 2017

    Plain MLTT is modeled by FinSet, which certainly has no NNO. In order to get anything interesting about ΩS 1\Omega S^1, we need univalence. Without universes, “univalence” here is formulated as large elims out of HITs, which categorically corresponds to “descent” for \infty-colimits, which is indeed a very special property of (,1)(\infty,1)-toposes.

    When I said =ΩS 1\mathbb{Z}=\Omega S^1 it was in the context of subcategories of Gpd\infty Gpd, and there it is certainly true. As I’ve said before, we don’t yet know how to prove internally that ΩS 1\Omega S^1 deserves that name unless we already have \mathbb{Z} to compare it to.

  5. Yes, then we agree. Thanks!

    • CommentRowNumber61.
    • CommentAuthorMike Shulman
    • CommentTimeMar 16th 2017

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

    • CommentRowNumber62.
    • CommentAuthorspitters
    • CommentTimeJun 25th 2018

    Some updates, further updating seems needed.

    diff, v32, current

    • CommentRowNumber63.
    • CommentAuthorspitters
    • CommentTimeJun 25th 2018

    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?

    • CommentRowNumber64.
    • CommentAuthorUrs
    • CommentTimeJun 25th 2018
    • (edited Jun 25th 2018)

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

    • CommentRowNumber65.
    • CommentAuthorspitters
    • CommentTimeJun 25th 2018

    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.

    • CommentRowNumber66.
    • CommentAuthorUrs
    • CommentTimeJun 25th 2018

    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!

    • CommentRowNumber67.
    • CommentAuthorspitters
    • CommentTimeOct 10th 2018

    interval as truncation of the booleans.

    diff, v34, current

    • CommentRowNumber68.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 10th 2018

    Worth a word on how it can be used to prove functional extensionality from propositional truncation?

    • CommentRowNumber69.
    • CommentAuthorAlizter
    • CommentTimeOct 10th 2018
    • (edited Oct 10th 2018)

    Concerning #67, I would argue that “2 element type” is clearer than “booleans”.

    • CommentRowNumber70.
    • CommentAuthorAlizter
    • CommentTimeOct 10th 2018

    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

    • CommentRowNumber71.
    • CommentAuthorMike Shulman
    • CommentTimeOct 10th 2018

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

    • CommentRowNumber72.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 11th 2018

    Does the interval as truncation of the booleans have anything to tell us about cubical type theory?

    • CommentRowNumber73.
    • CommentAuthorRichard Williamson
    • CommentTimeOct 11th 2018
    • (edited Oct 11th 2018)

    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.

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

  • (Help)