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.
Tim Campion (May 04 2022 at 15:21):I learned a bit about higher category theory (by which I mostly mean weak -categories in the current context) before I learned anything about type theory. I'm currently working with an undergraduate student who has an interesting leg up on past me -- she's taken a course in homotopy type theory (the course Emily Riehl taught last semester following Egbert Rijke's book), and now wants to learn about weak -categories. I'm trying to think of some good papers / expositions to direct her towards which can take advantage of her background here.
Tim Campion (May 04 2022 at 15:23):I already noticed one nice thing -- when she asked "what does 'strict' mean", I was able to say "It means roughly that lots of identities are definitional when they really should not be" and that kind of meant something to her.
Ulrik Buchholtz (May 04 2022 at 18:32):My guess is that anything that uses the complete Segal space model will be easier than quasicategories in this case, at least in the beginning. This could perhaps be paired with a simultaneous reading of Riehl–Shulman's paper on a simplicial type theory. But one can't really escape quasicategories, at least not yet…
Tim Campion (May 04 2022 at 19:45):Ulrik Buchholtz said:
My guess is that anything that uses the complete Segal space model will be easier than quasicategories in this case, at least in the beginning. This could perhaps be paired with a simultaneous reading of Riehl–Shulman's paper on a simplicial type theory. But one can't really escape quasicategories, at least not yet…
Thanks! That makes some sense. I didn't realize there were introductory sources using complete Segal spaces!
Zhen Lin Low (May 04 2022 at 23:03):Carlos Simpson's book uses Segal categories (i.e. Segal spaces with a discrete space of objects). I don't think I've seen any text that works with complete Segal spaces, other than the HoTT book (but only for 1-categories).
Mike Shulman (May 05 2022 at 00:23):Clearly this hole in the literature needs to be remedied! (-:
Tom Hirschowitz (May 05 2022 at 06:10):How about Eric Finster and @Samuel Mimram's type-theoretic definition of weak -categories?