* Categories with 2-families @ 2018-03-05 21:29 Michael Shulman 2018-03-07 17:09 ` [HoTT] " Thomas Streicher 0 siblings, 1 reply; 9+ messages in thread From: Michael Shulman @ 2018-03-05 21:29 UTC (permalink / raw) To: HomotopyT...@googlegroups.com By a standard construction (described for example at https://ncatlab.org/nlab/show/categorical+model+of+dependent+types), categories with families are equivalent to categories with attributes, i.e. to comprehension categories that are discrete fibrations. However, it seems to me that the attributes-to-families construction can be applied to a non-discrete comprehension category as well, producing something that one might call a "category with 2-families" (or maybe "pseudo-families"?): a category C together with a representable morphism Tm -> Ty of pseudofunctors C^op -> Cat. Have such things been defined or used anywhere before? ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Categories with 2-families 2018-03-05 21:29 Categories with 2-families Michael Shulman @ 2018-03-07 17:09 ` Thomas Streicher 2018-03-07 20:15 ` Peter LeFanu Lumsdaine 0 siblings, 1 reply; 9+ messages in thread From: Thomas Streicher @ 2018-03-07 17:09 UTC (permalink / raw) To: Michael Shulman; +Cc: HomotopyT...@googlegroups.com On Mon, Mar 05, 2018 at 01:29:56PM -0800, Michael Shulman wrote: > By a standard construction (described for example at > https://ncatlab.org/nlab/show/categorical+model+of+dependent+types), > categories with families are equivalent to categories with attributes, > i.e. to comprehension categories that are discrete fibrations. That's misleading I think. One rather should think categories with attributes as full comprehension categories (like any surjective map from a class S to Ob(C) allows one construct a category equivalent to C whose collection of objects is S). Thomas ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Categories with 2-families 2018-03-07 17:09 ` [HoTT] " Thomas Streicher @ 2018-03-07 20:15 ` Peter LeFanu Lumsdaine 2018-03-07 20:30 ` Thomas Streicher 0 siblings, 1 reply; 9+ messages in thread From: Peter LeFanu Lumsdaine @ 2018-03-07 20:15 UTC (permalink / raw) To: Thomas Streicher; +Cc: Michael Shulman, HomotopyT...@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 3826 bytes --] > > On Mon, Mar 05, 2018 at 01:29:56PM -0800, Michael Shulman wrote: > > By a standard construction (described for example at > > https://ncatlab.org/nlab/show/categorical+model+of+dependent+types), > > categories with families are equivalent to categories with attributes, > > i.e. to comprehension categories that are discrete fibrations. > On Wed, Mar 7, 2018 at 6:09 PM, Thomas Streicher < stre...@mathematik.tu-darmstadt.de> wrote: > > That's misleading I think. One rather should think categories with > attributes as full comprehension categories I used to agree with the usual view of CwA’s as full split comprehension categories, but I’ve come round to believing that it’s significantly better to view them as discrete comprehension categories (at least for most purposes). This is for several reasons: - (1) The axioms for CwA’s themselves, and for logical structure on them, involve *lots* of on-the-nose equalities between types over a given context. This is perfectly natural when they’re seen as discrete comp cats (since then on-the-nose equality is the same as isomorphism in the fibre); seen as full split ones, it violates the principle of equivalence (i.e. respecting isomorphisms). - (2) The treatment of logical structure becomes more uniform between comp cats and CwA’s under the “discrete” viewpoint. In the Lumsdaine–Warren “Local Universes…” paper (https://arxiv.org/abs/1411.1736), where we followed the established “full split” view, we had to define two separate versions of each piece of logical structure: “strictly stable” structure as the natural notion for CwA’s, and “pseudo-stable” structure as the natural notion for comprehension cats. With the discrete viewpoint, these are a single notion: pseudo-stable structure on a discrete comp cat gives exactly strictly stable structure! - (3) 2-categorically, the picture is much nicer under the “discrete” view. This is a bit too much to fully describe in a quick email, but one manifestation is the fact that viewing CwA’s as discrete comprehension categories, one gets natural inclusion 2-functors CxlCat —> CwA —> CompCat which are each 2-full-and-faithful, i.e. induce equivalences on hom-categories. Here CxlCat is the usual 1-category, viewed as a locally discrete 2-category; CwA is a fairly natural 2-category of CwA’s (Voevodsky convinced me that this is much more natural than the 1-category of CwA’s more usually considered); and CompCat is a 2-category in the “obvious” way. A “toy model” of the issues involved: you can embed Set into Cat as either the discrete or the codiscrete categories. Viewed 1-categorically, both of these are perfectly nice full and faithful functors; but 2-categorically, while the “discrete” embedding is 2-full-and-faithful, the codiscrete embedding is *very* far from being so. And this can be seen as lying behind the various ways in which the “discrete” embedding Set —> Cat is more natural for almost all purposes. Going back to CwA’s/comp cats: the one big *advantage* I see of the “full split” embedding is for the categorical analysis of type-constructors — e.g. the analysis of Pi-types and Sigma-types as adjoints — since the constructions are on types, but their universal properties involve general context morphisms. This I agree is much cleaner under the “full split” view. On the other hand, it’s not lost in the “discrete” view — e.g. it can be seen as a statement that these constructors become adjoints after applying “fullification” to the discrete comp cat in question. (Thankyou for bringing this issue up, by the way… I’ve been looking for a good moment to air this heresy :-) ) –p. [-- Attachment #2: Type: text/html, Size: 5448 bytes --] ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Categories with 2-families 2018-03-07 20:15 ` Peter LeFanu Lumsdaine @ 2018-03-07 20:30 ` Thomas Streicher 2018-03-07 20:39 ` Peter LeFanu Lumsdaine 2018-03-07 21:20 ` Michael Shulman 0 siblings, 2 replies; 9+ messages in thread From: Thomas Streicher @ 2018-03-07 20:30 UTC (permalink / raw) To: Peter LeFanu Lumsdaine; +Cc: Michael Shulman, HomotopyT...@googlegroups.com But if you specialize the interpretation of type theory in comprehension categories to discrete ones you wan't be able to interpret terms (since the latter are interpreted as morphism in the fibers, namely as sections). So I am not sure what you mean... Thomas ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Categories with 2-families 2018-03-07 20:30 ` Thomas Streicher @ 2018-03-07 20:39 ` Peter LeFanu Lumsdaine 2018-03-07 21:01 ` Thomas Streicher 2018-03-07 21:20 ` Michael Shulman 1 sibling, 1 reply; 9+ messages in thread From: Peter LeFanu Lumsdaine @ 2018-03-07 20:39 UTC (permalink / raw) To: Thomas Streicher; +Cc: Michael Shulman, HomotopyT...@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 668 bytes --] On Wed, Mar 7, 2018 at 9:30 PM, Thomas Streicher < stre...@mathematik.tu-darmstadt.de> wrote: > But if you specialize the interpretation of type theory in > comprehension categories to discrete ones you wan't be able to > interpret terms (since the latter are interpreted as morphism in the > fibers, namely as sections). To clarify, by “discrete comprehension categories” I mean the ones Mike was talking about, i.e. where the fibration of types is a discrete fibration; I don’t mean that the base category is discrete. So there’s no problem here — terms are still interpreted as sections of dependent projections, just as usual. –p. [-- Attachment #2: Type: text/html, Size: 1031 bytes --] ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Categories with 2-families 2018-03-07 20:39 ` Peter LeFanu Lumsdaine @ 2018-03-07 21:01 ` Thomas Streicher 2018-03-07 22:16 ` Peter LeFanu Lumsdaine 0 siblings, 1 reply; 9+ messages in thread From: Thomas Streicher @ 2018-03-07 21:01 UTC (permalink / raw) To: Peter LeFanu Lumsdaine; +Cc: Michael Shulman, HomotopyT...@googlegroups.com > To clarify, by ???discrete comprehension categories??? I mean the ones Mike was > talking about, i.e. where the fibration of types is a discrete fibration; I > don???t mean that the base category is discrete. So there???s no problem here > ??? terms are still interpreted as sections of dependent projections, just as > usual. Ok, that's like interpretation in categories with attributes, where terms are interpreted in the base and only types in the fibers of the presheaf of types. But such guys considered as comprehension cats are full. Maybe you just say that non-full comprehension cats are not useful for type theory which I fully agree with! (In other contexts like fibrational approach to geom.morph's non-full comprehensions cats are most useful but not in full generality, one just requires the fibrations to have comprehension which is a property not structure.) But it's not enough to require the splitting for types. One also has to require it for the associate FULL comprehension cat. E.g. it's not sufficient to have it for Pi, you must also have it for eval. Thomas ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Categories with 2-families 2018-03-07 21:01 ` Thomas Streicher @ 2018-03-07 22:16 ` Peter LeFanu Lumsdaine 2018-03-08 10:11 ` Thomas Streicher 0 siblings, 1 reply; 9+ messages in thread From: Peter LeFanu Lumsdaine @ 2018-03-07 22:16 UTC (permalink / raw) To: Thomas Streicher; +Cc: Michael Shulman, HomotopyT...@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 3377 bytes --] On Wed, Mar 7, 2018 at 10:01 PM, Thomas Streicher < stre...@mathematik.tu-darmstadt.de> wrote: > > To clarify, by ???discrete comprehension categories??? I mean the ones > Mike was > > talking about, i.e. where the fibration of types is a discrete > fibration; I > > don???t mean that the base category is discrete. So there???s no > problem here > > ??? terms are still interpreted as sections of dependent projections, > just as > > usual. > > Ok, that's like interpretation in categories with attributes, where > terms are interpreted in the base and only types in the fibers of the > presheaf of types. Yes, that’s exactly what I mean… > But such guys considered as comprehension cats are full. > …and this is exactly where I differ — CwA’s can be identified with full split comp cats, but they can also (differently) be identified with discrete comprehension categories. That is, there are TWO very natural (2-)functors D, F : CwA —> CompCat giving two different ways of viewing CwA’s as certain comprehension categories, analogous to how there are two ways D, I : Set —> Cat of viewing sets as categories: “discrete categories” or “indiscrete categories”. You can say “sets are indiscrete categories”, I can say “sets are discrete categories”, and neither of us is absolutely right or wrong; one can identify Set with either of those two different subcategories of Cat, and each of these identifications is useful for some purposes. Back with CwA’s/comp cats, I’m suggesting, specifically, that the “discrete” identification is more fruitful than has generally been appreciated. (Almost all literature I know on comprehension categories, including my own paper with Michael Warren on them that I referenced before, uses the “full split” identification without question.) By the way, in our case, while the “discrete” viewpoint really does identify CwA with a sub (2-)category of CompCat, the “full split” viewpoint doesn’t, since splitness is extra structure on a fibration, and so the “full split” functor CwA —> CompCat isn’t full, either as a functor or as a 2-functor; so the “full split” viewpoint only lets us identify CwA with a sub (2-)category of CompCat_spl, not of CompCat. Maybe you just say that non-full comprehension cats are not useful for > type theory which I fully agree with! > No, I’m saying the opposite: I’m suggesting that non-full comprehension cats, and the discrete in particular, are *more* useful for type theory than we have generally realised before! But it's not enough to require the splitting for types. One also has > to require it for the associate FULL comprehension cat. E.g. it's not > sufficient to have it for Pi, you must also have it for eval. I’m well aware that you need strict commutation under reindexing for term-constructors as well as for type-constructors. But those conditions are just as natural to state when CwA’s are viewed as discrete comprehension categories, instead of as split full ones — if anything, they seem to me more natural under the “discrete” viewpoint. See point (2) in my original email, about how logical structure on CwA’s and comp cats can be defined more uniformly using the “discrete” identification. –p. [-- Attachment #2: Type: text/html, Size: 4366 bytes --] ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Categories with 2-families 2018-03-07 22:16 ` Peter LeFanu Lumsdaine @ 2018-03-08 10:11 ` Thomas Streicher 0 siblings, 0 replies; 9+ messages in thread From: Thomas Streicher @ 2018-03-08 10:11 UTC (permalink / raw) To: Peter LeFanu Lumsdaine; +Cc: Michael Shulman, HomotopyT...@googlegroups.com Dear Peter and Michael, in full comprehension cats there is no difference between interpreting in the fibers and interpreting in the base and that's why it doesn't make a difference. As I said for type theoretic purposes there is not much use for non-full comprehension cats. But I agree with Peter that there is no point in considering non-identity morphisms in the fibers since we interpret in the base anyway. Considering full comprehension cats leads to unnecessary doubling of information. Thomas ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [HoTT] Categories with 2-families 2018-03-07 20:30 ` Thomas Streicher 2018-03-07 20:39 ` Peter LeFanu Lumsdaine @ 2018-03-07 21:20 ` Michael Shulman 1 sibling, 0 replies; 9+ messages in thread From: Michael Shulman @ 2018-03-07 21:20 UTC (permalink / raw) To: Thomas Streicher; +Cc: Peter LeFanu Lumsdaine, HomotopyT...@googlegroups.com On Wed, Mar 7, 2018 at 12:30 PM, Thomas Streicher <stre...@mathematik.tu-darmstadt.de> wrote: > But if you specialize the interpretation of type theory in > comprehension categories to discrete ones you wan't be able to > interpret terms (since the latter are interpreted as morphism in the > fibers, namely as sections). I've never heard anyone say that terms are interpreted as morphisms in the fibers. For one thing, that's only possible if the fibers have terminal objects. It's true in the natural semantic models that a section of the projection G.A -> G in the base category is equivalently a map 1_G -> A in the fiber over G, and also in the syntactic model if you have a strict unit type, but I've never heard anyone suggest that for a general comprehension category (necessarily with terminal objects in the fibers) the "correct" way to interpret terms is as morphisms in the fibers rather than sections in the base. And I'm very interested to hear you say it, because I recently came across an application where this *does* seem to be what I want to do, but I was hesitant because it was different from what I've heard everywhere else. Is there a reference that takes this point of view? > > So I am not sure what you mean... > > Thomas ^ permalink raw reply [flat|nested] 9+ messages in thread
end of thread, other threads:[~2018-03-08 10:11 UTC | newest] Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-03-05 21:29 Categories with 2-families Michael Shulman 2018-03-07 17:09 ` [HoTT] " Thomas Streicher 2018-03-07 20:15 ` Peter LeFanu Lumsdaine 2018-03-07 20:30 ` Thomas Streicher 2018-03-07 20:39 ` Peter LeFanu Lumsdaine 2018-03-07 21:01 ` Thomas Streicher 2018-03-07 22:16 ` Peter LeFanu Lumsdaine 2018-03-08 10:11 ` Thomas Streicher 2018-03-07 21:20 ` Michael Shulman
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).