added pointer to:

- Kobe Wullaert, Ralph Matthes, Benedikt Ahrens,
*Univalent Monoidal Categories*[arXiv:2212.03146]

Added a talk on univalent categories delivered at the HoTT Electronic Seminar Talks

Anonymous

]]>Added link to the 1lab page on univalent categories

Anonymous

]]>- Reworked the idea section a lot, and moved part of it to a new “comparing notions of category” section after the definition.
- Added a bunch of reasons why univalent categories are the “correct” notion of category in HoTT/UF at least.
- Used “precategory” everywhere where that is meant, avoiding the bare word “category” in this article.
- Added a remark about when and where univalence should and shouldn’t be discussed on other nLab pages.

definitions pertaining to strict univalent categories moved to gaunt category

Anonymous

]]>moved set theory examples section to gaunt category and replaced it with a comment that all gaunt categories are strict univalent categories

Anonymous

]]>gaunt categories exist so modified the ideas section

Anonymous

]]>On reading, I don’t like this. While it’s true that the bare definition of “univalent category” can be written down word-for-word in any dependent type theory, and then ported from extensional type theory to set theory, the resulting notion behaves so differently from in homotopy type theory that I don’t think it deserves the same name. I think it would be better for the page to be mostly written purely in homotopy type theory – or at least intensional type theory – with a brief remark further down about what happens if you try to do it in extensional type theory or set theory. (We also already have a page on what you get in that case, with a different name – gaunt category.)

]]>better ideas section

Anonymous

]]>adding motivation for (strict) univalent categories in set theory foundations

Anonymous

]]>added section on univalent categories in extensional type theory and set theory.

Anonymous

]]>It’s a good point that these notions make sense more broadly than homotopy type theory. I think their main interest is in univalent type theory, since that’s the case in which the natural examples of categorical structures turn out to be univalent, but we can be more general. I do still think that we don’t need separate pages about univalent dagger-categories and dagger-precategories, but maybe we can keep that page name as “univalent dagger-category” and just redirect to it from “dagger precategory”.

]]>Yes, cubical type theories and higher observational type theory are homotopy type theories. The specific implementation of HoTT given by MLTT+UA+HITs is called “Book HoTT”, after the HoTT Book.

]]>Is De Morgan or Cartesian cubical type theory or higher observational type theory a homotopy type theory? Or does homotopy type theory only refer to the flavour of Martin-Löf type theory with the univalence axiom and higher inductive types.

]]>On the note of having two separate articles for precategory and univalent category, we have separate articles for Segal space and complete Segal space and separate articles for preorder and partial order (as well as Heyting prealgebra and Heyting algebra), where the key difference in the pairs of articles is that one structure has a Rezk completion condition and the other does not.

]]>renaming to univalent category for the time being.

The definition makes sense in any intensional type theory, some of which like Thomas Streicher’s groupoid model of types do not accept the univalence axiom and thus are not homotopy type theories.

Univalent categories are also well defined in the presence of axiom K or UIP: they are strict univalent categories like the walking parallel pair or any poset in that context.

Anonymous

]]>This page needs a new name. The adjective “internal” isn’t really appropriate; that refers to internalizing things inside a category, not to phrasing them in type theory. (The connection is that when something is phrased in type theory and then the type theory is interpreted in a category, the end result is internalizing in the category.)

I was about to rename it to “category in homotopy type theory” when I realized someone recently created precategory, so by comparison it would be appropriate for this page to be called univalent category (which it already redirects from).

However, I *don’t* think we should have separate “pre” and “univalent” pages for all categorical notions in homotopy type theory. For instance, I believe the current page univalent dagger category should discuss both “dagger precategories” and “univalent dagger categories” and their relationship, rather than having separate pages for them, and it should thus be renamed to something like “dagger-category in homotopy type theory”. Do we think this distinction is sustainable? If not, then probably we should merge this page with precategory to produce a single page called “category in homotopy type theory”, serving as an example for other pages about categorical structures in HoTT.

cross-linked with the new entry *synthetic $(\infty,1)$-category theory*

cross-linked with the new article on *Rezk completion*

Thanks for the new link!

But so what may have been happening? Does it look like Darin abandoned the (n,r)-category code (maybe after discovering a flaw?) in favour of just (n,1)? Or is the new code just supplementing the previous one?

]]>@Jonas no, but you can blank them as have.

]]>