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.
Alexander Gietelink Oldenziel (Mar 13 2021 at 19:42):How do filtered colimits appear in Type theory (HoTT or Martin-Lof for instance)?
Is it some inductive-recursive-inductive-something type?
Mike Shulman (Mar 14 2021 at 02:51):Can you say a bit more about what you mean by "appear"? Do you mean how do we construct filtered colimits when working in type theory as a foundation for mathematics? Basically just like any other colimit, as a non-recursive higher inductive type. (Although, again like any other colimit, in HoTT there are issues with expressing (homotopy) colimits of arbitrary types (rather than just sets) over infinite diagram categories.)
Alexander Gietelink Oldenziel (Mar 14 2021 at 06:51):Mike Shulman said:
Can you say a bit more about what you mean by "appear"? Do you mean how do we construct filtered colimits when working in type theory as a foundation for mathematics? Basically just like any other colimit, as a non-recursive higher inductive type. (Although, again like any other colimit, in HoTT there are issues with expressing (homotopy) colimits of arbitrary types (rather than just sets) over infinite diagram categories.)
Ah, right. I think I was hoping that filtered colimits had some kind of interesting type-theoretic characterization rather than being a particular kind of general colimits/non-recursive HIT if that makes sense?
Mike Shulman (Mar 14 2021 at 12:01):Well, I don't think they do. Although some of the applications of filtered colimits can be achieved directly with recursive HITs. Plus filtered colimits are less generally useful in the absence of choice principles, since then there are fewer compact objects.