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 Bob 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 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
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 .
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 -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 such that , 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
added pointer to:
I have added an ISBN to
(can’t find any linkable electronic trace of the book).
But mainly I have added (here) a new section to the entry on a quantum version (with its own nForum thread here)
actually, looking back to Melliès 06, the linear/quantum version is already stated there on p. 5.
I have added the graphics that Melliès 06 provides for the triality and editing in more of Melliès 06 to the entry.
In particular, I am changing, hereby, the page title from Harper11’s whimsical “trinitarianism” (not to speak of his “holy trinity”) to Melliès06’s original and sober “trilogy” – whose dictionary (Wikipedia) definition fits rather well: “three works of art that are connected and can be seen either as a single work or as three individual works”
I have edited a fair bit:
Introduced a system of four sub-sections, for all for cases of classical/quantum and plain/parameterized.
Added more and more detailed pointers to references (in particular to Melliès’s article, but also others.)
Mover the big table to a new last section “Rosetta stone”, not to get it in the way of laying out the picture first.
added mentioning (here) of the insights needed to pass from the “classical plain” to “classical parameterized” version.
(here the adjectives “plain” and “parameterized” are not really doing justice to what’s going on – maybe we can think of better single adjectives for the section titles)
Now that there are several subsections, I have added a lead-in sentence in an Idea-section at the beginning, and a survey diagram towards the end.
You have “Programming laguage” twice in ComputationalTrilogyTopologizedQuantized.jpg.
I don’t think “trilogy” fits at all. These three things are not works of art, and they don’t go in any kind of sequence. What was wrong with “trinitarianism”?
Well, for Wikipedia a trilogy needn’t be ordered:
A trilogy is a set of three works of art that are connected and can be seen either as a single work or as three individual works.
On the other hand, in their original form as Greek plays, there was a narrative ordering.
I can see what was attractive about the idea of three manifestations of the same thing in ’trinitarianism’, and it does convey that it’s a kind of regulative thesis. But I hear that the religious tone was off-putting to some, in a way reminiscent of ’evil’.
But then ’trilogy’ doesn’t seem to be the right part of speech.
While we’re at it, why name one of the three, the ’computational’ in ’computational trilogy/trinitarianism’?
@David C
Maybe triptych, then?
Even if we fought out whether “computation” is better described as “a piece of art” or as part of the “holy trinity” (seriously, Mike?) it wouldn’t matter, since there is exactly one (according to nLab records) citable publication to go by, and that’s the original
who introduced the idea with the term “trilogy”.
A whimsical 2-page worth of weblog comment from 5 years later wouldn’t trump this, even if it had been meant as more than the over-the-top language that makes a good whimisical weblog post.
Luckily, it’s really un-important, either way.
But I hear that the religious tone was off-putting to some, in a way reminiscent of ’evil’.
This is getting ridiculous. Who are these people? I can go along with avoiding “cleavage” because it could be taken as a sexist joke, and I can go along with dropping “evil” because it has the wrong connotation of “something you should never do” when in fact it’s often very useful to work with strict structures. But I can’t think of any valid reason to be offended by this.
“Trilogy” just doesn’t make any sense. Regardless of what the dictionary says (and FWIW Merriam-Webster defines it as a series of works, hence ordered – NB a “series” is “a number of things or events of the same class coming one after another in spatial or temporal succession”), in modern everyday usage a trilogy is always ordered. But worse, it just doesn’t even evoke anything of the same meaning. There is no sense in which these three things are “works of art” – they are points of view on the same thing. That’s why the reference to the holy trinity – “distinct yet one essense” – is so a propos.
And fortunately, the nLab is not Wikipedia, so we are not bound to use only terminology that appears in citable publications. Frequently we create our own terminology.
If the word “trinitarianism” is too much of a mouthful or sounds too ecclesiastical, how about “computational trinity”? Merriam-Webster says that when not capitalized, “trinity” means “a group of three closely related persons or things”.
I agree that, with the usual reading, “trilogy” is not appropriate. If it’s three versions of the ’same’ idea, you can see why Rosetta Stone is taken as an analogy, and one would not call that a trilogy.
Again, I don’t see why “computational” makes it into the term, whatever follows. Melliès doesn’t include it – he just speaks of “trilogy”. Naming one corner undermines the point.
It’s not as though the threefold aspect is fixed either. The article goes on to broaden to “tetralogy” and Baez and Stay have a four-fold Rosetta stone for “physics, topology, logic and computation”, with category theory providing the common ground (Table 4).
Well, we have to put some adjective in front. Maybe “type-theoretic trinity”? Or “structural trinity”?
I do have to point out that apart from this single bibliographic reference, the phrase “computational trilogy” does not appear to be in use anywhere else.
In fact, after searching for “computational trilogy” (in quotes, to ensure exact matches), I found only two nLab pages and two more Twitter posts, both of which complain about “computational trinitarianism” being renamed to “computational trilogy”.
On the other hand, searching for “computational trinitarianism” (again in quotes, to ensure exact matches), reveals hundreds of relevant sources.
I would suggest sticking to “computational trinitarianism” as (by far!) the most widespread terminology. I do not see how it could possibly be considered religious in this context.
It’s probably going to be a passing term anyway. In a number of years it will just seem rather obvious that logic, categories and computing (and physics?) are talking about the same structures. ’Computational trinitarianism’ is playing a slogan-like role at the moment, encouraging people to look for commonality. Bring your understanding of one corner to bear on another. For those who understand, it barely needs saying, as though the physicist had to be reminded to use mathematics.
’Rosetta stone’ has a similar inspirational feel. Understand one part and you can unlock the secrets of the others. So I think we don’t need to shy away from a somewhat dramatic term.
On the other hand, with comments such as Bob Harper’s “three manifestations of one divine notion of computation” (The Holy Trinity), I doubt Bill Lawvere would like it.
Eh, Bill Lawvere really doesn’t like -categories, and that’s actual mathematics. What’s he got to do with it?
This kind of thought:
There was always the suspicion among scientists that such extra-mathematical publicity movements concealed an agenda for re-establishing belief as a substitute for science.
I always took it as compounded hyperbole and metaphor, much like John B uses “god-given” not infrequently. But point taken.
Since mysterious triality is in the news, relating physics to algebraic topology to algebraic geometry, why did we never consider ’computational triality’? (But ’triality’ is mentioned in #35.)
Maybe this goes back to the difference between what duality means for a mathematician and duality in physics:
One should beware that the use of the word “duality” in physics is in general different from concepts called “duality” in mathematics.
Added a couple of words, to indicate Harper’s shift to ’trinitarianism’ rather than ’trilogy’.
I still think ’triality’ would have been a better term.
With the advance down the page to the “classically controlled quantum computational tetralogy” could one say that what begins as something rather mysterious
three superficially different-looking fields of mathematics,
becomes more comprehensible?
Anonymous
I forgot again to sign in on the nLab.
Perhaps mention should be made at the moments when ’tetralogy’ occurs that this is (first?) posited by Baez and Stay in their choice of topics – Physics, Topology, Logic and Computation, though in their own table they add a fifth column – Category theory, Physics, Topology, Logic and Computation (pentalogy?).
The two tetralogies on this nLab page have entries: Logic, Computation, Category Theory, Topology.
Computation then is seen to combine computation/physics in the second one, i.e., where quantum circuits appear in a column about programming languages.
Not a true pentalogy for them. One is the common language to make sense of what is common in the other four:
category theory can serve to clarify the analogies between physics, topology, logic and computation.
I think that instead of talking about a trinity of computation, which seems to me to be too restrictive with regard to non-decidable logics such as first-order logic, we should talk about a logical triality between proof theory, type theory and category theory. Thus we associate a sequent calculus (let’s say LJ) with a type system (let’s say the simple types for the lambda-calculus) and with a family of categories (let’s say the CCCs).
I’m not an expert in this field, so I’d like your point of view.
Anon
Do you mean you don’t think first-order logic should be called “computational” because there’s no algorithm to decide the truth of a first-order statement? I don’t think that’s what “computational” is supposed to refer to – first-order logic can still be computational in the sense that its proofs can be interpreted as terms in a type theory and executed as a programming language.
1 to 60 of 60