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
   • CommentTimeOct 14th 2016
   • (edited Oct 14th 2016)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThis is to ask for advice on advice: I am in contact with a young HoTT postdoc who has been studying issues related to C-systems but would like to connect now to modal homotopy type theory of the kind that Felix Wellen did ([here](https://ncatlab.org/schreiber/show/Formalizing+Cartan+Geometry+in+Modal+HoTT)). His interest is however neither in geometric interpretation, nor in formalization in proof checkers, but his interest is in the special kind of meta theory that leads one to be interested in C-systems. He is asking me for suggestions of questions to study. Moreover, he would prefer a question in the form of a precisely formulated conjecture. What to suggest? So I am looking at the recent article * Chris Kapulkin, Peter LeFanu Lumsdaine, "The homotopy theory of type theories" ([arXiv:1610.00037](https://arxiv.org/abs/1610.00037)), and I am wondering if its perspective might be a good starting point to suggest here. I suppose the "contextual categories" considered there are more or less the same as C-systems. Might it be a good idea to consider the problem of extending the results presented in that article to a category of contextual categories that are equipped with a suitably homotopical idempotent monad?

   This is to ask for advice on advice:

   I am in contact with a young HoTT postdoc who has been studying issues related to C-systems but would like to connect now to modal homotopy type theory of the kind that Felix Wellen did (here). His interest is however neither in geometric interpretation, nor in formalization in proof checkers, but his interest is in the special kind of meta theory that leads one to be interested in C-systems.

   He is asking me for suggestions of questions to study. Moreover, he would prefer a question in the form of a precisely formulated conjecture.

   What to suggest?

   So I am looking at the recent article

   • Chris Kapulkin, Peter LeFanu Lumsdaine, “The homotopy theory of type theories” (arXiv:1610.00037),

   and I am wondering if its perspective might be a good starting point to suggest here.

   I suppose the “contextual categories” considered there are more or less the same as C-systems. Might it be a good idea to consider the problem of extending the results presented in that article to a category of contextual categories that are equipped with a suitably homotopical idempotent monad?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeOct 14th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexA modal notion of contextual category would be great to have, along with a construction of such things from model categories. That is, to make progress on Remark 7.5 of [BFP in RCoHoTT](https://arxiv.org/abs/1509.07584). The type theory presented in that paper might be a good place to start defining the appropriate notion of contextual category.

   A modal notion of contextual category would be great to have, along with a construction of such things from model categories. That is, to make progress on Remark 7.5 of BFP in RCoHoTT. The type theory presented in that paper might be a good place to start defining the appropriate notion of contextual category.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeOct 15th 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, excellent. I'll forward this.

   Thanks, excellent. I’ll forward this.