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.
created computational trinitarianism, combining a pointer to an exposition by Bon Harper (thanks to David Corfield) with my table logic/category-theory/type-theory.
I added a quotation from him. The key thought is a development must affect all three parts of the trinity to be important.
via Philip Thrift:
here are recent slides
(Hegel’s logic gets a mention :-)
Have added the pointer to the $n$Lab entry computational trinitarianism
I added to computational trinitarianism a link to my talk slides from the HoTT MRC JMM session last week.
Nice talk!
It is very nice to see cubical methods used so much. I have been working on other things for a few years, but for a few years before that I was working intensively on cubical homotopy theory, and at that time I felt that nobody had fully appreciated the benefits of working cubically; but once Thierry got interested, things exploded! Still I think there is a lot more that can be done on the models side, especially the higher categorical side.
I have masses of material and ideas from that earlier period, which I have tried occasionally to present bits of here, without really succeeding in finding a comfortable medium. One day I’ll hopefully get back to it. I’m happy to see that people are discovering are bits and pieces for themselves due to the needs of HoTT :-).
Is there a relation between what is good about a cubical version of type theory and why one wants a cubical version of homotopy theory?
Cubical diagrams are an essential concept for stating and understanding the generalized Blakers-Massey Theorems… (Cubical Homotopy Theory)
Or a cubical version of singular homology over a simplicial version (relative merits discussed at MO, including naturally Ronnie Brown)?
[I see Richard responded on the same theme.]
Nice. What is the entry “Licata-Shulman: spatial type theory” on slide 60?
I see people have thought of combining simplices and cubes. So a ’prismatic’ or ’prodsimplicial’ type theory?
I hope there won’t be further proliferation of shape-dependence of HoTT! :-) One of the great things about abstract homotopy theory is that it shows that the choice of shape is but an artifact of our perception, not intrinsic to the theory.
The big question still seems to be if there is a “compiler” from bookHoTT to cubical HoTT that takes elegant abstract proofs that don’t compute to more intricate proofs, that however compute. That’s anyway what I think cubical HoTT should be: A kind of unelegant but practical assembler implementation of an elegant higher language that however is not machine-executable.
Re 8. There are supercomplexes mentioned at cubical set and model+structure+on+cubical+sets. spatial type theory is developed in mike’s paper on the Brouwer fixed point theorem (and later work with Dan).
I fact, quite a few proofs do get simpler when using cubical methods. Also, much of HoTT can be developed developed in the internal logic of a topos based on an abstract interval. See Orton and Pitts and our work on guarded cubical type theory.
quite a few proofs do get simpler when using cubical methods
Consider the Blakers-Massey result in HoTT. It’s beauty and insight is precisely in its abstractness in that it does not make recourse to models for homotopy types, as the traditional proof does. If one does choose to prove by passing to a model for homotopy types, then it will generically happen that some models lend themselves to nicer proofs than others. But real elegance is a proof that does not make recourse to arbitrary choices that are not part of the statement being proven.
This is not to diminish in any way the accomplichment of cubical HoTT, just to put it in perspective.
I had in mind this paper by Mike and Dan that shows that cubical methods can be encoded an standard HoTT.
Dan and Guillaume, it seems.
What is the entry “Licata-Shulman: spatial type theory” on slide 60?
I had in mind adjoint logic and my BFP paper.
The big question still seems to be if there is a “compiler” from bookHoTT to cubical HoTT that takes elegant abstract proofs that don’t compute to more intricate proofs, that however compute.
I think that question is answered affirmatively. Cubical HoTT has all the same type constructors and rules as Book HoTT except that its identity types don’t satisfy the definitional J-computation rule, but Swan showed that one can define a different family of identity types that do satisfy that rule (though not the other definitional equalities that the cubical identity types do). So one can interpret Book HoTT into cubical HoTT in this way and thus compute it. (What it doesn’t answer is the homotopy canonicity conjecture as originally stated, because it’s not obvious whether the result that is computed in cubical HoTT can be proven in Book HoTT to equal the original term.)
I think that question is answered affirmatively.
That’s really amazing. I remember, years back in Nijmegen when Bas had come back from IAS, we were talking about whether this would ever become true. Exciting to hear that it is becoming true.
I hope some people are looking into writing code that actually does that “compilation”?
What I tried to convey in my talk (though perhaps this didn’t come through as well in the slides) is that in hindsight, the fundamental innovation of so-called “cubical type theory” is not about cubes at all. It’s that (1) identifications can be represented type-theoretically as functions out of an “interval” (just as they are in classical homotopy theory), and (2) transport should compute based on the type being transported in. These choices then seem to lead to some cubes arising naturally, but different type theories might have different levels of “cubicalness” built in.
quite a few proofs do get simpler when using cubical methods
If one does choose to prove by passing to a model for homotopy types, then it will generically happen that some models lend themselves to nicer proofs than others.
As Bas said, the point isn’t about cubical models for homotopy types. On one hand, the innovations I mentioned in #16 sometimes have a direct effect of simplification, which has little or nothing to do with any cubes. On the other hand, it’s sometimes useful, as in Dan and Guillaume’s paper, to notice and use “cube-shaped structure”; but this is not about passing to any model but rather using structure that is present in the abstract model-free world of HoTT. Other shapes are also already present in that world too, and will probably come up in other applications; but the abstract framework remains unchanged.
Regarding 16/17: exactly! This is fascinating. What this suggests is that there is ’cube-shaped structure’ fundamentally built into higher categories/homotopy types as well, so if one is interested in constructing models, which is certainly still important, a good place to start might be in a cubical setting, which has not been so much explored. This is not to disagree with the essence of the point that picking a shape is more of a tool, a means to an end. On the other hand, cubes have universal properties with respect to homotopies (cylinders), and are thus at least as fundamental as other shapes.
It would be very interesting if there were some kind of notion which combined Grothendieck’s idea of a ’coherator’ with that of a ’shape’. Coherators sort of try to abstract away from combinatorial details of the globular picture of higher categories, and one could perhaps hope for something like it for more general shapes/which was shape independent.
Re #17, so back to my question in #6, is it that some of what motivates people to develop a cubical homotopy theory (not the models, but the structure of the theory) is shared with the motivation for cubicalness in HoTT, even accepting Mike’s gloss (#16) that it’s not really about cubes at all?
For example, in the book I mentioned, Munson and Volic write:
This book makes the case for adding the homotopy limit and colimit of a punctured square (homotopy pullback and homotopy pushout) to the essential toolkit for a homotopy theorist. These elementary constructions unify many basic concepts and endow the category of topological spaces with a sophisticated way to “add” (pushout) and “multiply” (pullback) spaces, and so “do algebra”. Homotopy pullbacks and pushouts lie at the core of much of what we do and they build a foundation for the homotopy theory of cubical diagrams, which in turn provides a concrete introduction to the theory of general homotopy (co)limits and (co)simplicial spaces.
They make much of Goodwillie’s generalized Blakers-Massey theorem. Is it perhaps the case that the HoTT proof doesn’t yet extend to this generalization, and that a cubical HoTT would be the tool of choice?
Does the motivation for cubical HoTT in terms of its computational properties and in terms of greater convenience when doing synthetic homotopy theory overlap? E.g., for the latter we hear
In this paper, we have argued that there are benefits to working with cube and cube-over types. Higher cubes and cube-overs arise naturally when higher inductive types have two-dimensional (or higher) constructors (like the torus), when higher inductive types are nested (a pushout of pushouts, like in the three-by-three lemma), and when eliminations on higher inductive types are nested (like when mapping out of two circles).
Do such considerations have anything to do with what’s computationally attractive about HoTT?
Thanks, Mike, I see what you are saying. But just to nitpick a little:
identifications can be represented type-theoretically as functions out of an “interval” (just as they are in classical homotopy theory),
This is where the model sneaks in. Having an interval object is a property of a model for homotopy types, not available in abstract homotopy theory. (Of course you know this, I am just amplifying.) And once an interval object is assumed, its Cartesian powers give cube objects.
This is of course how Kan originally arrived at using cubical sets for modeling homotopy types, before abandoning them for simplicial sets.
I am not complaining nor saying that there is anything bad or wrong about this. Just highlighting that it still seems to me that it has to do with choices of model after all. No?
This is where the model sneaks in.
Dan and Guillaume write
While our approach fits nicely with work in progress on new cubical type theories [1, 7, 11, 25], the present paper can be conducted entirely by making appropriate definitions in “book homotopy type theory” [29] – Martin-Löf type theory with the univalence axiom and higher inductive types. Higher cubes can be defined in terms of higher paths, and cube-over-a-cube types can be reduced to homogeneous paths.
Are they using more than the interval as HIT?
Hi Urs, Mike is more than capable of answering for himself, of course, but I believe the point is that it is part of abstract homotopy theory, if one defines the latter as HoTT. That this a priori may be surprising is part of what makes the cubical type theory important, I think.
Thanks. Okay, so we agree and are reduced to the question whether a canonical interval exists in bookHoTT.
I suppose you are all meaning to point me to dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf.
Don’t have the leisure to read this in detail right now. But I assume the idea is to assume HITs and then define the interval type as the HIT with two generators in degree 0 and one in degree 1?
If one does this in abstact homotopy theory, the result is the homotopy colimit over
$\array{ && \ast \\ & \swarrow && \searrow \\ \ast && && \ast }$But this homotopy pushout is equivalent to the point, and abstract homotopy theory has no way to see it otherwise (being “non-evil”).
The only way that this homotopy pushout really is “the interval” is to pass to a model for homotopy types with standard cofibrant replacement functor, which replaces one (or both) of the above maps by the cofibration $\ast \hookrightarrow Interval$.
Now I am no expert on the details of HIT implementation in HoTT. Is the claim maybe that HITs come out not up to propositional equality but up to judgemental equality?
If so, then this does give a canonical interval type. But then that would be due to the definition of HITs being model-dependent.
I am just stating the obvious. Either of you can shortcut my second-guessing (I am sort of busy with something else…) by making explicit how that would-be canonical interval in book HoTT is meant to appear.
If you define “abstract homotopy theory” as “book HoTT”, then no, it doesn’t have an “interval” in the same way that cubical HoTT does. But the point I’m making is that so-called cubical HoTT is, a priori, just as good of a notion of “abstract homotopy theory”. The a posteriori justification for this is still a little weaker, since for instance Book HoTT is closer to being known to have models in all $(\infty,1)$-toposes than cubical HoTT is, but in principle there’s no reason that “cubical HoTT” couldn’t also have semantics in all homotopy theories. Perhaps such semantics would go by finding presentations of such homotopy theories using cubical sets, but that would be no more model-dependent than the fact that the current approaches to semantics for Book HoTT use presentations involving simplicial sets.
Moreover, even #23 is wrong: the interval HIT is not totally indistinguishable from the point in Book HoTT. There’s no property of types $P : Type \to Type$ such that $P(\ast)\neq P(\mathtt{I})$, by univalence, but (for instance) the presence of an interval HIT implies function extensionality, which is not provable in plain MLTT. Even Book HoTT has a strict “judgmental” equality, which is not reified as a type, but nevertheless is essential to the proper functioning and usability of the theory. I don’t see how this makes it “model dependent”, since HITs and judgmental equality are a property of the syntax having nothing to do with any model (and indeed were studied abstractly before we knew how to model them at all). But if you define “abstract homotopy theory” you mean some conjectural theory in which there is no strict equality at all, and “model dependent” to mean “not abstract homotopy theory in this sense”, then I guess you would then call Book HoTT “model dependent” – but I would argue that no “abstract homotopy theory” in this sense is known to exist, probably can’t exist, and if it did exist would be wholly impractical.
Note also that the “interval” in cubical HoTT is also a sort of “judgmental fiction”, not really a type. It can be reified as an interval HIT, but then the latter is really no different from the HIT interval in Book HoTT (except that it computes better, like all HITs in cubical HoTT).
Thanks, I see what you are saying. I’ll think about it.
By the way, is “reifying” a technical term here?
Not really; at least I couldn’t give a precise definition of it. But if it helps, HTS is a theory in which the strict judgmental equality is reified.
Someone can probably answer this easily:
Consider the rules of inference associated with product and hom. If beta reduction and eta convertion correspond to counit and unit, and there are type formation rules for product and hom, are the two computation rules for product and coproduct analogous to the triangle laws for an adjunction?
Mike explains the computational rules in category theoretic terms in this thread. See also link there.
The short answer is that I think it’s better to think of each type former as giving a representing object for some functor. The intro and elim rules give maps back and forth between the functor and the corresponding representable, and the beta and eta rules say that both composites are the identity.
added pointer to
1 to 32 of 32