# 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

## Site Tag Cloud

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

• starting some minimum

• Currently nothing but a pointer to page 16 of

Just so as to sort out the issue with where the term appears, as discussed in another thread here.

• Creating the page. Described briefly both the usual Lack model structure and the model structure using semi-strict equivalences coming from my thesis. A lot more could be added.

• Added some references on the categorical point of view on AECs. I think ideally this page would be rewritten to take that perspective from the start, in line with the nPOV, but I certainly don’t have the time (or background) to do that myself.

• I worked on brushing up (infinity,1)-category a little

• mostly I added in a section on homotopical categories, using some paragraphs from Andre Joyal's message to the CatTheory mailing list.

• in this context I also rearranged the order of the subsections

• I removed in the introduction the link to the page "Why (oo,1)-categories" and instead expanded the Idea section a bit.

• added a paragraph to the beginning of the subsection on model categories

• added the new Dugger/Spivak references on the relation between quasi-cats and SSet-cats (added that also to quasi-category and to relation between quasi-categories and simplicial categories)

• Made a note that he died this year.

• brief category:people-entry for hyperlinking references at orbispace

• Page created, but author did not leave any comments.

• Created a page for the homonymous cartesian theory.

• to be !includeed as a floating table of contents into relevant entries

• Following discussion in some other threads, I thought one should make it explicit and so I created an entry

Currently this contains some (hopefully) evident remarks of what “dependent linear type theory” reasonably should be at least, namely a hyperdoctrine with values in linear type theories.

The entry keeps saying “should”. I’d ask readers to please either point to previous proposals for what “linear dependent type theory” is/should be, or criticise or else further expand/refine what hopefully are the obvious definitions.

This is hopefully uncontroversial and should be regarded an obvious triviality. But it seems it might be one of those hidden trivialities which deserve to be highlighted a bit more. I am getting the impression that there is a big story hiding here.

Thanks for whatever input you might have.

• Started a page on lax extranatural transformations. I’ll add more material to here (very) slowly as needed for the page on lax biends.

• Started a page on lax biends. For now it is just a stub, but I will add more material to here (very) slowly.

• added pointer to p. 245 of Sets for Mathematics for the idea of

$U X \;\colon\; \array{ comodal X &\longrightarrow& X &\longrightarrow& modal X \\ opposite\;1 && unity && opposite\;2 }$
• I gave Sets for Mathematics a category:reference entry and linked to it from ETCS and from set theory, to start with.

David Corfield kindly alerts me, which I had missed before, that appendix C.1 there has a clear statement of Lawvere’s proposal from 94 of how to think of categorical logic as formalizing objective and subjective logic (to which enty I have now added the relevant quotes).

• I added to Tim’s stub on cellular homology. Still a bit rough around the edges perhaps. An example (say real projective space) would also be nice.

• Creating the page, which I intend to use at Lack fibration. If I have not made a mistake, this is a 2-groupoid model of the 2-truncation of the 2-sphere, and I have added remarks of this nature to the page, along with a ’computation’ of $\pi_{2}\left(S^{2}\right)$ using this model.

• Changed localy to locally

Anonymous