Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeJan 13th 2017
   • (edited Jan 13th 2017)
   • PermaLink
   Author: Urs
   Format: MarkdownItexSuppose somebody formally minded is looking for a good problem in the topic of [[contextual categories]] (C-systems). How about this: fix a given C-system, with your preferred set of extra type constructor data on it, and then ask the question: for any given small site, is the category of sheaves on that site with values in that C-system again canonically a C-system with the same collection of extra type constructors? I gather aspects of this play a role in most discussions of type theory model building, but is there any systematic discussion? I suppose the difficulty and interest in this question considerably varies with what the set of "extra type constructors" includes. A while back I had asked a similar question where "extra type constructors" was "modalities". Maybe that was overambitious for the person who I am asking for, so I am trying to see if something along these lines but more tractable would be a good thing to aim at.

   Suppose somebody formally minded is looking for a good problem in the topic of contextual categories (C-systems). How about this:

   fix a given C-system, with your preferred set of extra type constructor data on it, and then ask the question: for any given small site, is the category of sheaves on that site with values in that C-system again canonically a C-system with the same collection of extra type constructors?

   I gather aspects of this play a role in most discussions of type theory model building, but is there any systematic discussion?

   I suppose the difficulty and interest in this question considerably varies with what the set of “extra type constructors” includes. A while back I had asked a similar question where “extra type constructors” was “modalities”. Maybe that was overambitious for the person who I am asking for, so I am trying to see if something along these lines but more tractable would be a good thing to aim at.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeJan 18th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexSorry that I haven't answered this yet. I don't really know a comprehensive answer, but I can try to find someone who does. But I don't think a general answer is known, even for presheaves.

   Sorry that I haven’t answered this yet. I don’t really know a comprehensive answer, but I can try to find someone who does. But I don’t think a general answer is known, even for presheaves.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeJan 19th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexChris Kapulkin says > One result along those lines is Prop. 5.1 from: > <https://arxiv.org/abs/1610.00037> > but that: 1. covers only presheaves, 2. works with CwA's rather than contextual categories, 3. requires the indexing category to be inverse. > I don't think anything is known about the contextual categories though.

   Chris Kapulkin says

   One result along those lines is Prop. 5.1 from:

   https://arxiv.org/abs/1610.00037

   but that: 1. covers only presheaves, 2. works with CwA’s rather than contextual categories, 3. requires the indexing category to be inverse.

   I don’t think anything is known about the contextual categories though.

4. • CommentRowNumber4.
   • CommentAuthorp_l_lumsdaine
   • CommentTimeJan 20th 2017
   • PermaLink
   Author: p_l_lumsdaine
   Format: MarkdownItexExpanding a bit on Chris’s answer: - [I’ll write “contextual category” throughout; read it as “C-system” if you prefer.] - given an inverse category $\J$ and a CwA $\C$, there’s a CwA $\C^\J$ whose objects are $\J$-diagrams in $\C$ and whose types are “Reedy types”, i.e. like Reedy fibrations, but using the types of $\C$. (Chris and I state this in Prop. 5.1 of [arXiv:1610.00037](https://arxiv.org/abs/1610.00037), and look explicitly at it for some specific inverse categories $\J$; we’re writing up the fully general construction in a companion paper. It’s very analogous to Mike’s Reedy diagrams in type-theoretic fibration categories.) - the traditional standard type-constructors — Σ-types, Π-types, Identity types, universes — lift from $\C$ to $\C^\J$ fairly straightforwardly, as do various axioms (e.g. funext). Plenty of less-standard ones should too, I think (though have not thought hard about this) — e.g. modalities, various HIT’s, univalence. But I would *not* expect this to work for “arbitrary reasonable-looking type-constructors” — for all these constructors, the lifting relies on the fact that their rules imply at least a little bit of some kind of functoriality. Articulating exactly what is required would be a *very* interesting question, I think! - given a contextual category $\C$, you can consider it as a CwA, take inverse diagrams in it, and then take its contextual core $\core(\C^\J)$. This is I think the natural thing to consider as “the contextual category of $\J$-diagrams in $\C$”. (I wouldn’t expect $\C^\J$ to itself be contextual except in extremely degenerate cases, and I don’t think one should want it to be — its contextual core is I’m pretty sure the right thing to be looking at, if one wants to do (pre)sheaves in the contextual world.) - the core construction preserves *all* logical structure; so all the constructors that lifted to $\C^\J$ will further lift to $core(\C^\J)$. - Chris and I also consider *homotopical* inverse diagrams $\C_\h^\J$, i.e. with certain maps of the diagrams asked to be equivalences. This is I guess a very restricted case of the (homotopical) sheaf condition. The CwA/contextual category aspect of this will be just the same as for the plain inverse diagrams above. - Lifting constructors to $\C_\h^\J$ gets more subtle. The finite-limit-like constructors (Σ, Id) are always inherited from $\C^\J$. Chris and I have some (quite restrictive) conditions on $\J$ under which $\Pi$-types are also inherited from $\C^\J$. I would hope that $\C_\h^\J$ may have $\Pi$-types for more general $\J$, but these can’t in general be just inherited from $\C^\J$. I haven’t thought about other constructors — Chris or Mike, have you? These should be fun and accessible questions. - Sheaves for more general coverages on inverse categories, still using Reedy types: haven’t thought about this at all! But I think it should be somewhat do-able, at least for restricted classes of coverages (e.g. finitely generated, for a start) — some such restriction is I think inevitable in order for sheafification to be available, just like when doing the same thing with e.g. elementary toposes. This is I’m pretty sure wide open, and would definitely be very interesting, though might turn out to be quite large. It’d be nice even to see some specific toy example of this considered. - Going beyond the case of inverse categories/Reedy types: not sure at all. It’s not clear to me how generally one should expect this to work. I guess Mike may have ideas about this, from the fibration category setting? (I’d expect the situation with CwA/cxl cat setting to continue to be fairly analogous to the situation with fib cats.) - In a different direction: what about *internal* (pre-)sheaves, for an internal category/site in the original CwA/contextual category? I’ve definitely discussed this with a few people in the past, but I’m afraid don’t remember at all clearly who it was or how much they or I had had figured out at the time. I think some people have looked a bit at internal presheaves, but I’m not sure if it ever made it to print, and I don’t remember hearing of anyone considering internal sheaves at all! So I think this is also pretty open, and would be very interesting.

   Expanding a bit on Chris’s answer:

   • [I’ll write “contextual category” throughout; read it as “C-system” if you prefer.]

   • given an inverse category $\J$ and a CwA $\C$, there’s a CwA $\C^\J$ whose objects are $\J$-diagrams in $\C$ and whose types are “Reedy types”, i.e. like Reedy fibrations, but using the types of $\C$. (Chris and I state this in Prop. 5.1 of arXiv:1610.00037, and look explicitly at it for some specific inverse categories $\J$; we’re writing up the fully general construction in a companion paper. It’s very analogous to Mike’s Reedy diagrams in type-theoretic fibration categories.)

   • the traditional standard type-constructors — Σ-types, Π-types, Identity types, universes — lift from $\C$ to $\C^\J$ fairly straightforwardly, as do various axioms (e.g. funext). Plenty of less-standard ones should too, I think (though have not thought hard about this) — e.g. modalities, various HIT’s, univalence. But I would not expect this to work for “arbitrary reasonable-looking type-constructors” — for all these constructors, the lifting relies on the fact that their rules imply at least a little bit of some kind of functoriality. Articulating exactly what is required would be a very interesting question, I think!

   • given a contextual category $\C$, you can consider it as a CwA, take inverse diagrams in it, and then take its contextual core $\core(\C^\J)$. This is I think the natural thing to consider as “the contextual category of $\J$-diagrams in $\C$”. (I wouldn’t expect $\C^\J$ to itself be contextual except in extremely degenerate cases, and I don’t think one should want it to be — its contextual core is I’m pretty sure the right thing to be looking at, if one wants to do (pre)sheaves in the contextual world.)

   • the core construction preserves all logical structure; so all the constructors that lifted to $\C^\J$ will further lift to $core(\C^\J)$.

   • Chris and I also consider homotopical inverse diagrams $\C_\h^\J$, i.e. with certain maps of the diagrams asked to be equivalences. This is I guess a very restricted case of the (homotopical) sheaf condition. The CwA/contextual category aspect of this will be just the same as for the plain inverse diagrams above.

   • Lifting constructors to $\C_\h^\J$ gets more subtle. The finite-limit-like constructors (Σ, Id) are always inherited from $\C^\J$. Chris and I have some (quite restrictive) conditions on $\J$ under which $\Pi$-types are also inherited from $\C^\J$. I would hope that $\C_\h^\J$ may have $\Pi$-types for more general $\J$, but these can’t in general be just inherited from $\C^\J$. I haven’t thought about other constructors — Chris or Mike, have you? These should be fun and accessible questions.

   • Sheaves for more general coverages on inverse categories, still using Reedy types: haven’t thought about this at all! But I think it should be somewhat do-able, at least for restricted classes of coverages (e.g. finitely generated, for a start) — some such restriction is I think inevitable in order for sheafification to be available, just like when doing the same thing with e.g. elementary toposes. This is I’m pretty sure wide open, and would definitely be very interesting, though might turn out to be quite large. It’d be nice even to see some specific toy example of this considered.

   • Going beyond the case of inverse categories/Reedy types: not sure at all. It’s not clear to me how generally one should expect this to work. I guess Mike may have ideas about this, from the fibration category setting? (I’d expect the situation with CwA/cxl cat setting to continue to be fairly analogous to the situation with fib cats.)

   • In a different direction: what about internal (pre-)sheaves, for an internal category/site in the original CwA/contextual category? I’ve definitely discussed this with a few people in the past, but I’m afraid don’t remember at all clearly who it was or how much they or I had had figured out at the time. I think some people have looked a bit at internal presheaves, but I’m not sure if it ever made it to print, and I don’t remember hearing of anyone considering internal sheaves at all! So I think this is also pretty open, and would be very interesting.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeJan 20th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWhat a comprehensive answer! Thanks a whole bunch Peter. This should be recorded somewhere, either on the nlab or the hott wiki. I have not thought about lifting constructors to your $C^J_h$. What I have thought about is sheaves in a context where we have arbitrary HITs: if $J$ is any site such that we can give some meaning to $C^J$ as a contextual category with HITs, then the coverage on $J$ should be incarnated internally as a type family that we can localize at to produce a lex modality --- and the modal types for any lex modality on a contextual category should again be a contextual category with all the same type constructors, except that positive types will have to be reflected and thus might not have as strict of a universal property. As for when $C^J$ exists beyond $J$ inverse, one needs to figure out what the "fibrant" diagrams should be. In the case of model categories, the only general answer that seems to work is "injectively fibrant", but no one knows a concrete description of the injectively fibrant diagrams that could be used in the fibration category case. And in the absence of small-object-argument sort of things that you have in model categories, I don't see how any construction like this would have a fibrant replacement and how you would get type constructors preserved. I feel like Thorsten Altenkirch might be a good person to ask too, especially as regards internal presheaves. To do internal presheaves homotopically, you have the problem of infinite objects; but if you have UIP, then you could presumably imitate the construction of internal presheaves in an elementary topos.

   What a comprehensive answer! Thanks a whole bunch Peter. This should be recorded somewhere, either on the nlab or the hott wiki.

   I have not thought about lifting constructors to your $C^J_h$. What I have thought about is sheaves in a context where we have arbitrary HITs: if $J$ is any site such that we can give some meaning to $C^J$ as a contextual category with HITs, then the coverage on $J$ should be incarnated internally as a type family that we can localize at to produce a lex modality — and the modal types for any lex modality on a contextual category should again be a contextual category with all the same type constructors, except that positive types will have to be reflected and thus might not have as strict of a universal property.

   As for when $C^J$ exists beyond $J$ inverse, one needs to figure out what the “fibrant” diagrams should be. In the case of model categories, the only general answer that seems to work is “injectively fibrant”, but no one knows a concrete description of the injectively fibrant diagrams that could be used in the fibration category case. And in the absence of small-object-argument sort of things that you have in model categories, I don’t see how any construction like this would have a fibrant replacement and how you would get type constructors preserved.

   I feel like Thorsten Altenkirch might be a good person to ask too, especially as regards internal presheaves. To do internal presheaves homotopically, you have the problem of infinite objects; but if you have UIP, then you could presumably imitate the construction of internal presheaves in an elementary topos.