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.
Xuanrui Qi (Jun 27 2021 at 18:58):Hm, I have a follow-up question about contexts. Can't we just "work only with closed types and terms", as the naive types-as-objects approach would suggest? What would be the problem with this approach?
Mike Shulman (Jun 27 2021 at 21:09):Well, types are defined inductively, and the induction passes through open ones in the process of constructing closed ones. So you can't expect to define something like an interpretation function recursively over only closed types, since closed types aren't inductively defined all by themselves. It's possible you could play some tricky games to get around this, but I expect probably any resulting simplification would be outweighed by the extra complication of the trickery.
Mike Shulman (Jun 27 2021 at 21:10):I really think it's better to do things one step at a time: first construct a semantics that closely matches the behavior of syntax, like a multicategory or a category-with-families, then show how the "natural" categorical semantics can be massaged into the form of syntax-like semantics.