Not signed in (Sign In)

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 12th 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

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2023

    Added remark that the clause “Acyclic cofibrations are preserved by pullback along fibrations” (added in rev 11) is implied by the previous conditions.

    diff, v22, current