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.
Nathaniel Virgo (Mar 26 2022 at 02:05):I've picked up some ideas about dependent sets here and there, but my understanding of the topic isn't as systematic as I'd like. I find notation like or useful, but I have to think pretty hard every time I use it, and I feel I'm probably missing some basic ideas that would make it easier. Does anyone know of a good introduction to "how to think about dependent sets", for someone who knows a bit of category theory but not really any type theory or functional programming beyond the basics?
Naso (Mar 26 2022 at 08:52):I think the first chapter of the HoTT book is pretty good https://homotopytypetheory.org/book/
Nathaniel Virgo (Mar 27 2022 at 01:03):That seems great for the type theory perspective, and very readable - I'll go through it in detail, much appreciated.
What I really want to know, in addition, is how to connect those ideas to the category theory perspective, where dependent sets are modelled in terms of the slice functor , where has pullbacks. This is outlined very briefly in David Spivak's generalised lens categories paper, and on nlab at [[dependent sum]] and [[dependent product]], but it's super condensed in those places and I'm really hoping to find something that spells it out in a bit more of a step-by-step and conceptual way. Does anyone know of a resource like that?
Bruno Gavranović (Mar 27 2022 at 11:02):Are you looking for something like this?
Nathaniel Virgo (Mar 27 2022 at 11:10):Oh, that looks like exactly what I was looking for, thanks!