added this pointer:

- Eric Finster,
*The $(\infty,1)$-category of Types*, talk at CQTS (Dec 2022) [slides: pdf, video: rec]

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?

]]>Added recent paper

- {#AlliouxFinsterSozeau20} Antoine Allioux, Eric Finster, Matthieu Sozeau,
*Types are internal infinity-groupoids*(PDF)

Anthony Hart

]]>added pointer to

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

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

]]>thish rule

And in the second point of proof of 1.3.1:

If it ends with the rule $f$

should be $f R$

then $B \in \mathcal{G}$ and so $\vdash A \; type$

should be $\vdash B \; type$

]]>Thanks!

]]>One more

]]>$id_A : (A \vdash B)$ (p. 25)

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 $\mathcal{G}(A, B)$ of “edges” for each $x, y \in \mathcal{G}$; the identity and composition rules too, with $\circ$ and $id$

Great thanks, Mike! Plenty for me to digest here. And I’d forgotten about those notes. I’ll take a look over Easter.

]]>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 $\omega$-categories” in the same way that HoTT is “a type theory for $(\infty,1)$-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 $\omega$-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 $\omega$-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, $\omega$-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 $k(((f1)g)h))$, then quotienting by associativity and unit laws $(f g)h \equiv f(g h)$ 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 $k(f(g(h1)))$ (in type-theoretic syntax $x:A \vdash k(f(g(h(x)))):B$, 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.

]]>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 $B \stackrel{f}{\to} A$ and $x\colon B \vdash f(x)\colon A$ 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 $\vdash$ denotes not postcomposition with a morphism, but pullback along a morphism.

But with univalence, presumably one could have postcomposition with the object classifier to $Type$.

Does this Yoneda construction point to anything important in the difference between the notations?

]]>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 $A \union B$ of subtypes

Ah, no, in the sense of *join of simplicial sets*.

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.

]]>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 $(\infty,2)$-toposes. He says the single extra type constructor he adds is one for joins. He says that he is writing a book on $\infty$-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 $\infty$-category, not passing through a 1-categorical presentation) and that thereby he thinks he solves the problem of interpreting ordinary HoTT+UV in general $\infty$-stack $\infty$-toposes.

]]>Re #2,

from what I do understand I wouldn’t call it an internal language for $\omega$-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.

]]>That was where he was still in October!

]]>Thanks for the alert. I have emailed Eric now to check.

]]>Eric Finster seems to have moved, so links from that old webpage aren’t working. Has he moved here?

]]>Have added pointer to Kock-Joyal-Batanin-Mascari 07 for that “higher-dimensionsal string diagram”-notation (“zoom complexes”) that Eric uses.

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

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

]]>