Not signed in (Sign In)

Start a new discussion

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeSep 24th 2013
    • (edited Sep 24th 2013)

    added to the references-section of the stub type-theoretic model category pointers to André Joyal’s slides on “typoses” (he is currently speaking about that again at CRM in Barcelona).

    (maybe that entry should be renamed to “categorical semantics for homotopy type theory” or the like, but I won’t further play with it for the time being).

    I am also pointing to Mike’s article and to his course notes. I will maybe ask André later, but I am a bit confused about (was already in Halifax) how he presents his typoses, without mentioning of at least very similar categorical semantics that has been discussed before. Maybe I am missing some sociological subtleties here.

    • CommentRowNumber2.
    • CommentAuthorzskoda
    • CommentTimeSep 24th 2013
    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMar 31st 2014

    I have edited the stub entry type-theoretic model category a bit: added some actual content to the Idea-section and moved what used to be there into the (mostly empty) Definition-section.

    Mainly I added more specific pointers to where Mike defines this. In particular previously the entry seemed to point ot the wrong article.

    I also made some slight corresponding edits at locally cartesian closed (infinity,1)-category and at relation between type theory and category theory, just editorial edits, trying to bring out the point more clearly (which seems to still not have penetrated too far into the community…)

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJan 14th 2019

    Greatly expanded, with a list of many possible hypotheses that could be included, multiple citations to papers that make similar nonce definitions, and a summary of which hypotheses suffice for which type-theoretic constructions.

    diff, v11, current

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeJan 14th 2019

    Once again I hit the weird bug that the rendered page wasn’t updated after this edit until I made another trivial edit.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeJan 14th 2019

    Added a warning about ensuring that the interpretation of type theory actually sees the same homotopy theory as the whole model category.

    diff, v12, current

    • CommentRowNumber7.
    • CommentAuthorspitters
    • CommentTimeJan 15th 2019

    The connection with (algebraic?) model structures on constructive cubical models is missing. I don’t have the time to chase references now, but maybe someone knows this by heard.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeJan 15th 2019

    I don’t know that connection. What I know of the constructive cubical models has a rather different flavor; but I’m certainly not up to date on all the most recent cubical developments.

    • CommentRowNumber9.
    • CommentAuthorspitters
    • CommentTimeJan 15th 2019

    Christian spoke about this in Bonn for example video. I don’t know whether there is a write up. There was a discussion on the HoTT list after, IIRC.

    • CommentRowNumber10.
    • CommentAuthorspitters
    • CommentTimeJan 16th 2019

    I was thinking of this discussion that the cartesian cubical model is an elementary oo-topos, but not equivalent to oo-groupoids.

    • CommentRowNumber11.
    • CommentAuthorUlrik
    • CommentTimeJan 16th 2019

    Make a reference to type theoretic model structure, itself TDB.

    diff, v13, current

    • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 16th 2019

    Why have you removed the hyphen from ’type-theoretic’? This is requesting that a new page be set up.

    • CommentRowNumber13.
    • CommentAuthorUlrik
    • CommentTimeJan 16th 2019

    David, I don’t think I removed the hyphen anywhere? For now I changed the name of type-theoretic model structure and made sure both pages had redirects for the non-hyphen versions.

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 16th 2019
    • (edited Jan 16th 2019)

    I meant the link you have in #11. That was wanting a new page, but now you’ve put in the redirect it’s fine.

    Or did I get mixed up with type-theoretic model category/type-theoretic model structure? Anyway, there’s now consistent naming.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJan 16th 2019

    Re #10 I don’t think that has anything to do with the model-category-theoretic conditions, does it?

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJan 16th 2019

    What is going to be at type-theoretic model structure? It seems a terrible idea if a “type-theoretic model category” is not the same as a category equipped with a “type-theoretic model structure”.

    • CommentRowNumber17.
    • CommentAuthorUlrik
    • CommentTimeJan 16th 2019
    • (edited Jan 16th 2019)

    Re #16 yes, that problem did cross my mind :)

    It’s going to be about Christian’s model structures built using gluing. We used to call these “Sattler model structures” but Christian objected, so for moment they go by type-theoretic model structure. But as you point out, that’s not ideal. I don’t know a good solution, though.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJan 16th 2019

    Is that the kind of “gluing” coming from the “glue types” used for cubical univalence, not the standard term Artin gluing that’s also been used to build models of type theory? (-:O Maybe if we finally find a good name for those “glue types” that doesn’t conflict with established terminology, it would give us a good name for these model structures. Or vice versa.

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 11th 2019

    Added simplicial local cartesian closure to the definition of “good model category” from Lumsdaine-Shulman. (This is not currently in the paper, but needs to be, and will be added in the next arXiv update.)

    diff, v15, current

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)