Not signed in (Sign In)

Start a new discussion

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 15th 2018

    I added the reference

    diff, v26, current

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 15th 2018

    Rasekh speaks of a future goal

    Blakers-Massey: One of the classical results of algebraic topology is the Blakers-Massey theorem. We already know it holds in a higher topos [Re05]. Thus the next natural question is to show it also holds in an EHT, using the fact that the proof mainly relies on the descent condition

    But we know this about the Blakers-Massey theorem already, no? It says thre about the HoTT proof that

    This translates to an internal language proof of Blakers-Massey valid in all (∞,1)-toposes (including elementary (∞,1)-toposes). Unwinding of the fully formal HoTT proof to ordinary mathematical language is, for the special case of the Freudenthal suspension theorem, in (Rezk 14).

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 16th 2018

    We may as well carry on discussion of this topic here, rather than the parallel thread, since the nLab software sends updates to elementary (infinity,1)-topos here.

    With the definition settling down :), perhaps this is a good moment to revisit Joyal-Kripke semantics for HoTT. It was raised back here as something needing some loving attention with regard to n-types cover.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeMay 16th 2018

    I’m still trying to finish up the semester, haven’t had a chance to really read Rasekh’s paper yet. Re #2, I guess the point is that Rezk’s manual unwinding should apply essentially verbatim in the elementary case, presuming that it only uses descent rather than any Grothendiecky stuff? (Otherwise, the claim would depend on the conjecture that HoTT is an internal language for (elementary) (,1)(\infty,1)-toposes.)

    • CommentRowNumber5.
    • CommentAuthornimarasekh
    • CommentTimeMay 16th 2018
    I might be able to explain where the Blakers-Massey came from. There is a good chance that I am over-complicating things and everything has already been done, but here is my perspective: There is already a proof in HoTT. That proof was translated to spaces by Charles Rezk. He also proves that it holds for a higher topos (using model categories). Ideally this means that the proof will also hold for an elementary higher topos, however, I don't know if that directly follows. In particular the arguments by Rezk are focused on spaces. As Mike pointed out the underlying idea should be that everything just depends on descent and other topos theoretic properties, but I personally think this is worth analyzing.

    There is also a second motivation I had in mind, which might be less clear from the HoTT perspective. I am hoping to convince more "traditional" algebraic topologists to consider topos theory/higher cats/HoTT. That is also why I called the section algebraic topology. It's interesting how results that are obvious to the HoTT community are surprising to many algebraic topologists. From that perspective having concrete proofs in the language of higher categories seems to be a benefit.
    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 17th 2018

    Thanks for joining in the conversation, Nima. Of course, do feel free to add to the entry elementary (infinity,1)-topos.

    results that are obvious to the HoTT community are surprising to many algebraic topologists.

    I’d be interested to hear of anything specific that can be said along these lines. Will HoTT insights be expressible as understandable maxims, or will they remain difficult to comprehend.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeMay 17th 2018

    There are two proofs by Rezk cited at Blakers-Massey theorem. The first, in Toposes and homotopy toposes, does indeed use model categories. But the second is the one that’s a translation of the HoTT proof and thus uses only elementary topos-theoretic properties, no model categories in sight. The latter writeup does talk about “spaces”, but he says at the beginning

    I expect that things go through in an arbitrary ∞-topos.

    I think one can just read his note essentially verbatim with “space” translated to “object”. I suppose maybe it would have been better if he’d written it in that language to start with and not trusted the reader to do the translation in their head?

    • CommentRowNumber8.
    • CommentAuthornimarasekh
    • CommentTimeMay 19th 2018

    OK, I am new to the forum and so my comments are more ambiguous than I expected. I will try to clarify.

    I’d be interested to hear of anything specific that can be said along these lines. Will HoTT insights be expressible as understandable maxims, or will they remain difficult to comprehend.

    When I was talking about the surprise among algebraic topologists I had the following in mind. There are many results that are well-known for spaces, such as truncations, factorizations, Blakers-Massey, … . Many of those results can be generalized, but very often the proof has to be changed. That’s exactly what resulted in the new proof of Blakers-Massey or truncations. In algebraic topology a standard way to construct truncations is the small object argument. That obviously doesn’t work in every setting, which is exactly why a new proof was necessary. As a result of this general fact algebraic topologists can react surprised that certain results about spaces can hold in other settings and I would like to change that.

    There are two proofs by Rezk cited at Blakers-Massey theorem. The first, in Toposes and homotopy toposes, does indeed use model categories. But the second is the one that’s a translation of the HoTT proof and thus uses only elementary topos-theoretic properties, no model categories in sight. The latter writeup does talk about “spaces”, but he says at the beginning.

    Yes, I had exactly those two proofs in mind in my previous post. I think you are right and the proof can be adjusted to a topos. The one thing that worries me are fiber-wise statements (like Lemma 1.4). By my understanding of the word fiber this only holds for spaces.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeMay 20th 2018

    Ah, I didn’t realize Rezk was lazy in his translation that way. Statements like that, of course, should be interpreted in the HoTT sense of “fiberwise”, as a dependent product internal to the topos. You’re right that there would be some additional work to be done in writing that in true \infty-categorical language. On the other hand, maybe that work was already done by ABFJ? Their generalized Blakers-Massey theorem is explicitly “valid in an arbitrary higher topos” (as well as “with respect to an arbitrary modality”) and it looks like their proof is written in \infty-categorical language.

    • CommentRowNumber10.
    • CommentAuthornimarasekh
    • CommentTimeMay 20th 2018

    I think ABFJ might be a more promising path forward. At least one issue is that some of their results on modalities rely on presentability conditions (for example Proposition 3.1.8 and Proposition 3.3.8). In particular it seems to be needed for the parts where you have to show that we get a factorization system. So, those parts need to be adjusted somehow.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMay 20th 2018

    Right, you do need to be in something like a locally presentable setting in order to generate modalities by an arbitrary set of maps. But the classical Blakers-Massey is, I believe, the special case of their theorem applied to the truncation modalities, and those should exist in the elementary case. Indeed, the fact that truncations can be constructed from finite colimits and an NNO is a big part of what motivated me to suggest that we were ready for a tentative definition of elementary (,1)(\infty,1)-topos. However, as far as I know, that proof hasn’t been written out in categorical language yet.

    But that problem is already mentioned as (III) in your “Algebraic topology” section, so if that’s the only obstacle to applying ABFJ in the elementary case then it doesn’t seem like your problem (II) is really open any more. (Also, I think even in (III) you should say explicitly that the theorem has already been proven in HoTT, and all that remains to do is translate it into categorical language.)

    • CommentRowNumber12.
    • CommentAuthornimarasekh
    • CommentTimeMay 27th 2018

    I agree I should mention the HoTT work on NNO and truncations in the problem section. Thank you for reminding me.

    On the ABFJ I am still uncertain. It’s seems promising (and it should be true that descent is enough) but I still need to check in detail to make sure presentability hasn’t snuck into any of the later results.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeMay 27th 2018

    That’s fair, but even before the checking has been done, their work (and Rezk’s) should still be mentioned in any discussion of this possibly-still-open problem.

    • CommentRowNumber14.
    • CommentAuthorspitters
    • CommentTimeJun 2nd 2018
    • (edited Jun 2nd 2018)

    Do we have a precise (classical) connection between Shulman/Rasekh and the work by Joyal, who uses model structures? Constructively, we would first need to develop a theory of \infty-categories, probably following Riehl/Shulman, perhaps along the lines of directed type theory and the work by Licata and Weaver slides.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJun 2nd 2018

    Which work by Joyal are you referring to?

    • CommentRowNumber16.
    • CommentAuthorspitters
    • CommentTimeJun 3rd 2018

    This one, the one linked to at that elementary+(infinity%2C1)-topos using tribes.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJun 3rd 2018

    Hmm. Well, I haven’t worked out the details, but I expect that one of his presents one of ours, whereas it’s an open question whether every one of ours could be presented by one of his. Some of his axioms (like fibrancy of \mathbb{N}) are very strict, so strict that I don’t even know whether every Grothendieck (,1)(\infty,1)-topos has a model satisfying them. Other than that issue, it looks like the main difference is that he assumes one fixed universe as part of the structure rather than the mere existence of as many universes as necessary, plus the effectiveness of groupoid objects (which is not “elementary” in the sense of “finite”).

    • CommentRowNumber18.
    • CommentAuthorspitters
    • CommentTimeJun 3rd 2018

    He seems to restrict to Grothendieck toposes over Reedy categories, I don’t know why he wants NN to be fibrant.

    It would be good to record this in any case, currently, the page read like the two notions are equivalent.

    • CommentRowNumber19.
    • CommentAuthornimarasekh
    • CommentTimeJun 3rd 2018

    Mike as a follow up to our previous discussion, do you have (or are aware of) a write up of a proof for how to build an NNO in an EHT? I’ve seen you mention this based on the fact that it holds in HoTT, but was wondering if there is an actual higher categorical argument out there.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJun 4th 2018

    I don’t think anyone has compiled the HoTT proof out into a topos-theoretic one. It’s kind of involved.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJun 4th 2018

    My guess would be that he wants N to be fibrant for the same reason the 2LTT people do, so that he can do things like define a fibrant type of semisimplicial types by induction over it.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeJun 4th 2018

    Added remarks on how Joyal’s definition differs from the one here.

    diff, v27, current

    • CommentRowNumber23.
    • CommentAuthornimarasekh
    • CommentTimeJun 4th 2018

    Yeah, that is what I was worried about. I think one important step in translating many of the results into an EHT is to have a concrete proof that we can construct an NNO. Well then let me rephrase my question. Do you know of a HoTT proof that would be more amenable to a translation to higher categorical language?

    • CommentRowNumber24.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 5th 2018

    Fixed a markdown-formatted link whose opening < was replaced by &lt;, so it had rendered looking like raw markdown.

    diff, v28, current

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeJun 5th 2018

    I think constructing an NNO out of the rest of the structure is more of a curiosity than an impediment to using the definition of EHT. Just like the question of whether we can construct colimits: the important thing is that colimits and the NNO are there; if we can remove them from the definition without changing the fact that they’re there, that’s nice, but it doesn’t make much of a difference in practice.

    • CommentRowNumber26.
    • CommentAuthornimarasekh
    • CommentTimeJun 5th 2018

    I thought we need an NNO to make the definition of an EHT work. Specifically the constructions by Egbert Rijke need colimits over countably infinite set. So we either have to assume it (which would be a non-finite assumption and so not elementary?) or we have to prove it.

    In particular in your blog post you suggest that one reason why we should not assume NNOs in a topos is exactly because we can prove it’s existence and then use that to recover the results of Rijke in the setting of an EHT.

    I think in that sense it is different from finite colimits. It am perfectly willing to assuming we have finite colimits (but it would be cool to know you can recover them), but I think it is important that we can build NNO to avoid assuming it.

    Based on your post are you suggesting we should just add the existence of an NNO to the definition of an EHT?

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeJun 5th 2018

    An NNO is perfectly finite and elementary. I don’t think it is any different from finite colimits. The only difference between them is that in the 1-categorical case an NNO is not usually included in the definition and doesn’t follow from it — but probably more theorems about elementary 1-toposes than not add the assumption of an NNO, and there aren’t many interesting examples that lack one; so arguably it could just as well have been included.

    I think in a paper proving (say) the Blakers-Massey theorem in an EHT it would be perfectly in order to state the definition including an NNO and then say “it is expected that the existence of an NNO can be proven from the other axioms; this has been shown in homotopy type theory, which is conjecturally the internal language of EHTs, but the general internal language theorem has not yet been proven and the construction of an NNO has not yet been manually compiled out into categorical language.”

    • CommentRowNumber28.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 5th 2018

    OT: about toposes without NNO… I guess sheaves of finite sets on a finite site, but are there finite versions of realisability topses? Lurie’s recent course on categorical logic ended up with \infty-pretoposes of finite homotopy types, which aren’t \infty-toposes, so that’s kind of an indication of the boundary between EHT and higher pretoposes as far as possessing NNO/W-types goes.

    • CommentRowNumber29.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 8th 2018
    • (edited Sep 8th 2018)

    Two new references

    • Nima Rasekh, Yoneda Lemma for Elementary Higher Toposes, (arXiv:1809.01736)

    • Nima Rasekh, Every Elementary Higher Topos has a Natural Number Object, (arXiv:1809.01734)

    What can be said already of the relation between what can be proved in HoTT and what holds in all elementary (∞,1)-toposes, and of processes to translate between such proofs?

    diff, v29, current

    • CommentRowNumber30.
    • CommentAuthorDavidRoberts
    • CommentTimeSep 8th 2018

    I guess every elementary higher topos should thus admit all W-types? Or at least all finitary ones (those associated to polynomial functors given by formal power series).

    • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTimeSep 8th 2018

    What can be said already of the relation between what can be proved in HoTT and what holds in all elementary (∞,1)-toposes, and of processes to translate between such proofs?

    At the moment, nothing general and precise. Being able to deduce automatically that HoTT theorems hold in elementary (∞,1)-toposes would require at least (with current technology) knowing how to present any elementary (∞,1)-topos by a suitable kind of fibration category, which is something that we almost know how to do with Grothendieck (∞,1)-toposes (the universes are still too weak in general), but in the elementary case we haven’t much of a clue. There is also the disputed initiality principle. In the other direction, one would need to show that the homotopy (∞,1)-category of the fibration category built out of HoTT syntax is an elementary (∞,1)-topos, which also has not been done; I think the best result we have is Chris Kapulkin’s theorem that it is locally cartesian closed. So at the moment we’re at the stage of only being able to translate proofs “by hand”, which unfortunately isn’t feasible for very long and involved ones like the impredicative construction of an NNO that I formalized in HoTT.

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeSep 8th 2018

    In addition, although I don’t understand Rasekh’s construction of an NNO yet, I do see that he uses non-elementary means, e.g. an infinite limit of categories of diagrams. It’s not immediately clear how to translate such an argument into HoTT manually, although if we believe that the homotopy (∞,1)-category of HoTT is an elementary (∞,1)-topos then there must be a way.

    • CommentRowNumber33.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 24th 2018
    • (edited Sep 24th 2018)

    I watched Mike’s very nice talk yesterday – Towards elementary infinity-toposes.

    I have a question. So you explain why we can have a subobject classifier straight away, but need to go about things more subtly with object classifiers, since monomorphisms are either equal or not. This shows they can be treated differently, but should they be?

    I recall from discussions several years ago, you thinking it better to keep a logical level separate from the type theory. I thought the realisation that the (1)(-1)-level is just one level and of no greater significance than any other was to be taken as a sign that ’logic’ is just an integral part of the whole, the result of a truncation. Shouldn’t the definition of elementary infinity-toposes keep to this egalitarian treatment?

  1. Added that talk.

    Anonymous

    diff, v30, current

    • CommentRowNumber35.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 24th 2018

    I think I should read up on propositional resizing - a page which needs to be created.

    • CommentRowNumber36.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 24th 2018

    If one were to imagine an \infty-Elephant, I guess the 6 section structure continues to make sense: as categories; 2-categorical aspects; as spaces; as theories; homotopy and cohomology; as mathematical universes. In fact, maybe some, like the fifth, work out much better.

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeSep 24th 2018

    But that’s the general phenomenon: \infty-Category theory has all the structures familiar from plain category theory, plus a bunch of improvements.

    From way back in 2007, when I first saw André Joyal speak at the Fields institute here, I (seem to) remember that this is how he introduced the topic of what we now call \infty-category theory. He started his talk (paraphrasing from memory) with saying: “In this talk I want to convince you that \infty-category theory exists, and behaves much like ordinary category theory.” Of course he said “quasi-categories” instead of “\infty-categories”.

    • CommentRowNumber38.
    • CommentAuthorspitters
    • CommentTimeSep 24th 2018

    Yes, Andre had the same message at 3WFTOP.

    • CommentRowNumber39.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 24th 2018

    I wasn’t presenting this as a surprise that much remains as before, but rather a chance to think on Johnstone’s choice of sixfold account, and how things might be organised from the \infty perspective. I could imagine some shuffling about at the very least.

    • CommentRowNumber40.
    • CommentAuthorUrs
    • CommentTimeSep 24th 2018

    I see. Regarding the Elephant, I was always thinking that the reason why volume 3 keeps (or kept?) being delayed is that the topic of that volume (cohomology) works really well only once passing from toposes to \infty-toposes.

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeSep 24th 2018

    I definitely agree with #40: Part E of the 1-Elephant was outdated before it was written. (-: Although I am still hoping to read Part F one day.

    This shows they can be treated differently, but should they be?

    They certainly need not be (funny how “need not” and “should not” have such different semantics in English). I wrote about this back here. But it’s a question of terminology: in the 1-category case, an “elementary topos” has an impredicative subobject classifier, so I think it’s best to stick to that usage in the \infty case, with alternative terms like “predicative (\infty-)topos” for the predicative case. That way we can say sensible-sounding things like “the category of 0-truncated objects in an elementary \infty-topos is an elementary 1-topos”.

    • CommentRowNumber42.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 24th 2018

    Thanks! I don’t even remember that thread. I see it ends

    I was already suspicious of the suboject classifier in toposes; type theory is much more elegant without an equivalent of this (Prop, the type of propositions)…Now that these inelegances are out of the way, I am much more interested in topos theory.

    Earlier, however, you’d linked elegance with predicativity, and effective computation with its opposite. But perhaps elegance is in the eye of the beholder.

    • CommentRowNumber43.
    • CommentAuthorMike Shulman
    • CommentTimeSep 24th 2018

    I assume you mean I linked elegance with impredicativity. Yes, elegance is certainly one of the things that’s in the eye of the beholder. However, I do see Itai’s point (he being the one you are quoting about the elegance of type theory). Roughly, the problem is that propositional resizing is an axiom, rather than something expressible as a rule. On the other hand you can formulate a type theory with a specified “type of propositions” PropProp that’s impredicative in the sense of admitting quantifications over types in arbitrary universes (for instance, Coq does this), but then you don’t know (unless you assert it as another axiom) that every type with the property of “being a proposition” (i.e. isprop(A) x,y:AId(x,y)isprop(A) \equiv \prod_{x,y:A} Id(x,y)) is equivalent to something in PropProp. In the traditional perspective on 1-topos theory, this rears its head as the fact that higher-order logic cannot prove the axiom of unique choice, even though it holds in all toposes (because HOL has other models, like strong-subobject logic in quasitoposes, where AUC fails).

    Maybe the point is that we’re applying the same adjective to different things: impredicative proofs are more elegant, but predicative formal systems are more elegant.

    • CommentRowNumber44.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 24th 2018

    Yes, impredicativity.

    Interesting stuff.

    • CommentRowNumber45.
    • CommentAuthorDavidRoberts
    • CommentTimeSep 24th 2018

    In your talk Mike, you responded to a comment I couldn’t hear by saying something like “that paper has a mistake” and that you were in contact with the author. What paper was that? I notice you didn’t mention Rasekh’s work on NNOs, so I was wondering if it was this.

    • CommentRowNumber46.
    • CommentAuthorMike Shulman
    • CommentTimeSep 24th 2018

    Yes, it’s that one.

    • CommentRowNumber47.
    • CommentAuthorDavidRoberts
    • CommentTimeSep 24th 2018

    OK, thanks. I was going to ask him if from NNOs one gets all W-types in an elementary \infty-topos, but I guess you’re the person to ask now :-)

    • CommentRowNumber48.
    • CommentAuthorMike Shulman
    • CommentTimeSep 25th 2018

    I haven’t worked it out, but I expect so, in the same way one does in an elementary 1-topos.

    • CommentRowNumber49.
    • CommentAuthorMike Shulman
    • CommentTimeSep 25th 2018

    Back on #42-43: On the other hand, one might argue that the most elegant formal system is the maximally impredicative one with Type:TypeType:Type

    • CommentRowNumber50.
    • CommentAuthorAlizter
    • CommentTimeSep 26th 2018
    • (edited Sep 26th 2018)

    Concerning #49: What are some good references about Type:Type? I understand that Girards paradox gives us a non-normalising well type term, but can one be a bit clever and avoid these kinds of terms? I have seen for example in the UniMath library that Type:Type is okay as long as one treads carefully. What exactly is meant by this?

    • CommentRowNumber51.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 26th 2018

    Perhaps this post – Universe Polymorphism and Typical Ambiguity – for a start.

    • CommentRowNumber52.
    • CommentAuthorMike Shulman
    • CommentTimeSep 26th 2018

    I have seen for example in the UniMath library that Type:Type is okay as long as one treads carefully. What exactly is meant by this?

    You’d have to ask the UniMath authors. The only thing I can think of that they might have meant by “tread carefully” is “only write down things that could be formalized using a hierarchy of universes instead”, i.e. don’t actually make any use of Type:Type. Universe polymorphism and typical ambiguity, as implemented in modern Coq, are ways that you can sometimes forget about this and just write “Type” whenever you want a universe, and the computer can make sure for you that universe hierarchy levels can be consistently assigned. (In practice, some manual universe level management seems often to be required whenever you’re working seriously with multiple universes, though this could just be a limitation of current tools.)

    People do sometimes like to use Type:Type when implementing new type theories, just because it’s simpler and doesn’t get in the way of understanding whatever new features you want to focus on. And if you’re regarding type theory as a programming language for actually writing real-world programs, then non-normalizing terms need not be worrisome, since real-world programming language usually include general recursion (and hence plenty of non-terminating programs) anyway. (And in fact, from Type:Type you can construct a looping combinator and thereby obtain general recursion.) To take an example I happened to be reading recently, this paper writes

    …we analyze and implement a partial type checking algorithm for the inconsistent theory Type:Type … The motivation for this work is to implement type checkers for dependently typed programming languages which support general recursion… We use Type:Type as a test case for a language with dependent types avoiding the syntactic complexity of a full programming language.

    The problem only comes in when you also want to use type theory to prove things, because a non-normalizing term of type \emptyset would be a proof of a contradiction. (I have some further thoughts about that, but they haven’t coalesced enough to talk about yet.)

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)