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 opetopic type theory with a bit of explanation based on what I understood based on what Eric Finster explained and demonstrated to me today.
This is the most remarkable thing.
I have added pointers to his talk slides and to his online opetopic type system, but I am afraid unguided exposition to either does not reveal at all the utmost profoundness of what Eric made me see when he explained and demonstrated OTT to me on his notebook. I hope he finds time and a way to communicate this insight.
This is really awesome (and I don’t fully understand it), but from what I do understand I wouldn’t call it an internal language for -categories, not in the same way that HoTT is the internal language of an -category. I would say it’s a deductive system for describing the cells and higher cells in an -category, rather than for reasoning about its objects internally.
Yes, it seems to be language of absolute types, no dependent types yet.
We talked a while about how to bring dependent types in. Eric kept making the point that quite a few constructions which one might naively think to add by hand to the system are, or seem to be, automatically contained already.
In particular since OTT may say “adjunction” and may “shift itself out of its own universe”, it seems not implausible that one could say “type of slice opetopes” and “pullback” on that and then get dependent sum and product.
Eric voiced a more concrete idea for how to do that, but I am not sure if this is for public consumption yet.
Be that as it may, what I saw him do I would have found unbelievable just yesterday. I tried to find out from him how those opetopic Kan filler conditions, which are both clear and easy while apparently being fully suffcient, did escape wider attention. It seems his answer was that he deduced them from something that some Thorsten Palm presented in completely different terms and that nobody else has yet really looked into it.
Maybe I don’t know about this “opetopic Kan filler condition”.
So given an opetope, there is the evident concept of its “horns”, now called “nooks”, given by removing the top dimensional cell and one of the codimension-1 cells. There is one outer horn/nook given by removing the unique outgoing codimension-1 cell, the others are inner. Entirely straightforward as one would hope.
And then Eric uses the straightforward filler conditions: every outer horn has a filler (this is now the “term introduction rule” for a term of type the shape of the outer opetope) which is marked an equivalence if all the other codim-1 faces were, and every inner horn has a filler if all the codim-1 faces are marked equivalences and the inner filler is marked an equivalence. So this, too, is just what one would expect.
And the claim is that this is all there is to it.
Apparently some Thorsten Palm gave lectures on this not long ago at a meeting in Warsaw. But I have not seen any account of that. If I remember well what Eric told me, then Palm in turn got this from, hm, Makkai, maybe. But I may be misremembering. I haven’t found any article saying this yet.
Palm apparently gave a proof that if a horn of an opetope has a filler, than any opetopic pasting diagram containing that horn as a subdiagram still has that filler “whiskered” in the higher dimensional sense. This proof is unpublished and Palm apparently left academia right afterwards, and maybe the only copy of his work is now on Eric’s computer.
Eric said that this proof is really to be thought of as a general transport theorem, with “transport” in the sense of transport in HoTT. He also said that this does everything that one would think univalence would do for one, without there being a univalence axiom. (But I may not be remembering this in the right detail.) He also amplified that, contrary to univalence, this manifestly computes.
Is there some “completeness” property as well, saying that everything you would expect to be an equivalence is marked as such?
My immediate guess is that when you add such a completeness property, then in defining which cells you “expect” to be equivalences you’d end up back at the original definition of opetopic -category.
Hi Mike, yes, that’s my understanding, that whenever you produce a filler from a horn/niche/nook all whose codim-1 faces are marked as equivalences, then the filler is marked as an equivalence. Eric has this video Orchard 4 – Identities and invertibility. That seems not to recall the general rule, but it gives the simplest examples.
And yes, I suppose Eric’s system is meant to be the rules of opetopic omega-categories. But I am not sure which version precisely. There is no extra universality condition in Eric’s rules, instead universality of fillers is automatic (or meant to be and checkably so in examples, but I am not sure if there is a proof(?)).
I guess the system is meant to formalize something by Makkai. But I am not sure where exactly to look in Makkai’s writing. You might know more.
Ah, so apparently every filler is marked “universal”, for composition that’s at 5:17-5:36 in the video Orchard 3 – Composition and associativity.
Have added pointer to Kock-Joyal-Batanin-Mascari 07 for that “higher-dimensionsal string diagram”-notation (“zoom complexes”) that Eric uses.
Eric Finster seems to have moved, so links from that old webpage aren’t working. Has he moved here?
Thanks for the alert. I have emailed Eric now to check.
That was where he was still in October!
Re #2,
from what I do understand I wouldn’t call it an internal language for -categories
but the page still says
to be thought of as the internal language of omega-categories.
Regarding the elusive online whereabouts of Eric, presumably opetopic.net is his.
By the way, Denis-Charles claims in private communication that he figured out a working 1-directed HoTT, i.e. the would-be internal language for -toposes. He says the single extra type constructor he adds is one for joins. He says that he is writing a book on -category theory from scratch, and he is teaching from it in Regensburg, and that the model-independent proofs he gives in that book are, secretly, derived in this 1-directed HoTT. (Probably it’s this text here: pdf, though this may not contain yet all that he talked to me about.)
He said that he thinks he can use this to make sense of “homotopy-coherent semantics” for ordinary HoTT (i.e. interpreting it genuinely in an -category, not passing through a 1-categorical presentation) and that thereby he thinks he solves the problem of interpreting ordinary HoTT+UV in general -stack -toposes.
He says the single extra type constructor he adds is one for joins.
Is that in the sense of (non-disjoint) union, so a kind of classical disjunction rather than an intuitionist one?
I see the database theorists have a range of kinds of join.
Ah, no, in the sense of join of simplicial sets.
From Rijke’s article at that page, it seems there’s a connection:
the join of embeddings is just the union of subtypes. Thus, we see that in particular the join generalizes the union of subtypes
Re the point I recalled of Mike’s in #14 that this opetopic type theory is not an internal language, is that broadly the same point as Mike from elsewhere?
Generally I think of string diagrams and type theory as parallel. They serve the same general purpose — a syntactic presentation of free categories that simplifies proofs internal to some kind of structured category — but in very different ways.
I’d still like to get a little clearer on the difference. On the one hand, there’s the matter of forming the dual picture in a string diagram. But staying at the level of a comparison and here, I see the Yoneda embedding is invoked. The type theoretic notation is a “direct reflection” of the embedding.
Later in the Dependent type section,
now the denotes not postcomposition with a morphism, but pullback along a morphism.
But with univalence, presumably one could have postcomposition with the object classifier to .
Does this Yoneda construction point to anything important in the difference between the notations?
I changed the page to say just “type theory for omega-categories” rather than “internal language for omega-categories”. I’m no longer as sure of the distinction I was trying to draw back in #2. Opetopic type theory, as I understand it, is “a type theory for -categories” in the same way that HoTT is “a type theory for -toposes”. Type theory is a very general kind of thing and there can be many different “type theories” that present free categories of a given sort.
I’m not sure exactly what an “internal language” is or isn’t. On the one hand, whenever we have a kind of type theory that corresponds to a kind of category, there is some kind of adjunction in which the right adjoint takes each category to a “universal” type theory for reasoning about that category in particular, and that type theory is often called the “internal language” of the category. In this sense, every opetopic -category ought to give rise to a particular opetopic type theory called its “internal language” relative to OpTT. On the other hand, there is a general sense in which we say things like “IHOL is an internal language for 1-toposes” to mean essentially that IHOL is a type theory that presents free 1-toposes, and again in this sense I guess one could say that OpTT is an internal language for opetopic -categories. I do feel like there’s something different about OpTT that makes me resist calling it an “internal language”, but I have trouble pinning down exactly what that is.
As for the difference between type theory and string diagrams, in general a “syntax for X-categories” (such as toposes, lcccs, -categories, etc.) is a way of constructing the free (or presented) X-category on some data. Then we can do proofs using that construction, and nevertheless conclude that the theorem applies to all X-categories by mapping universally out of the free/presented X-category that is constructed out of our data. A given presentation for an X-category always generates an X-category in a “tautological” way by simply freely adding all the operations that exist in an X-category and quotienting by all the axioms that must hold; this corresponds to reasoning in the ordinary category-theoretic syntax for X-categories with objects and morphisms and commutative diagrams.
In type theory we instead construct a “free structure” of a different sort, perhaps quotient it (although usually the quotient is smaller or unnecessary), and then prove that it also happens to be the free X-category. For instance, the tautological presentation of the free category on a graph is obtained by adding free composites like , then quotienting by associativity and unit laws and so on. The “type-theoretic” presentation is instead obtained as the free structure generated by identity morphisms and having a “postcomposition with generators” operation, giving us only composites that look like (in type-theoretic syntax , of which no quotienting is necessary. We then have to prove that these are a category (the definition of composition is called “cut-elimination” or “admissibility of substitution”) and that they are the free category, after which we can use type-theoretic proofs to tell us things about categories. The content, as it were, of using type theory rather than category theory is in the nontriviality of the proof that type-theoretic syntax does give the free category.
(Actually, though, the generality of type theory means that the “tautological” presentation can also be given using a different sort of type theory; type theory is a very general syntax for describing free structures of many sorts.)
String diagrams proceed similarly, except that the construction is different: now we describe the free X-category in terms of some kind of labeled topological graph, quotiented by a relation of isotopy. Unlike for type theory, this description is not itself tautologically “free” in any way; it’s built out of topology and geometry. The equivalence relation of isotopy is in some sense even “bigger” than in the tautological case; but it’s very “intuitive” to use (just move things around) and therein lies the advantage.
I wrote more about this in the logic of space and in my categorical logic notes.
Great thanks, Mike! Plenty for me to digest here. And I’d forgotten about those notes. I’ll take a look over Easter.
SInce I’m invigilating a test and have some time now, I’ll send any typos I find:
they implicit in what ; that it generates is has ; a set of “edges” for each ; the identity and composition rules too, with and
One more
(p. 25)
Thanks!
thish rule
And in the second point of proof of 1.3.1:
If it ends with the rule
should be
then and so
should be
Re #20, I was wondering in view of Girard’s “A logic without cut elimination is like a car without an engine” what there is to say about cut-elimination in a string diagrammatic logic. Richard White’s A Cut-Elimination Theorem for a Peircean Logic talks about this for Alpha graphs.
Re #15,
By the way, Denis-Charles claims in private communication that he figured out a working 1-directed HoTT,
It would be interesting to see how his approach compares with Mike and Emily’s new paper.
added pointer to
Added recent paper
Anthony Hart
Interesting, thanks for the pointer!
I skimmed over it, but don’t have a detailed understanding yet. Would it be right to think of this as implementing the opetopic type theory that Eric had previously, sort of stand-alone, but now manipulating MLTT types? Or the otgher way around – which seems to be what the authors descrbe by adding a monad universe to (?) HoTT – to add these opetopic type formation rules to HoTT?
1 to 31 of 31