Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: mathematics

Topic: GATs with dependent contexts

Kevin Arlin (Oct 25 2023 at 23:55):

I've just made the quite informal LocalCharts post linked below where I muse a bit about how to most easily extend basic GAT syntax into something that would allow us to write down the theory of multicategories and other similar nicely-infinite theories in a finite number of lines of code. In short, I propose (though most of the idea is due to @Owen Lynch) a two level type theory that basically wraps an untyped $\lambda$-calculus around ordinary GAT syntax. The variables in the outer type theory are then to be interpreted as actual integers semantically. I'm curious whether anybody around here can recognize the right context to put this kind of idea into. Very much appreciate any thoughts, as I've been trying to think about type theory a bit lately but am absolutely not a type theorist!

Kevin Arlin (Oct 25 2023 at 23:55):

https://www.localcharts.org/t/a-generalization-of-gat-syntax/9836

Mike Shulman (Oct 26 2023 at 02:31):

The usual way to "solve" this problem is to introduce another sort for "finite lists of objects", with constructors saying that there is an empty list and any list can be extended by a single object. In other words, the constructors of "contexts" in type theory. I put "solve" in quotes because it doesn't exactly describe multicategories, but something more general (some relative of a CwF). But for many purposes it's just as good or better.

Mike Shulman (Oct 26 2023 at 02:33):

One minor comment on the post: the type $\mathsf{Nat}\to T$ isn't equivalent to $T\times (T\to T)$. The latter is the type of data for defining a recursive function $\mathsf{Nat} \to T$, but multiple "recursion datas" can define the same function, and not every function is recursively defined.

Kevin Arlin (Oct 26 2023 at 15:57):

Oh, of course, thanks for the correction, and for the suggestion, I'll think about that.