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
    • CommentTimeMay 9th 2017
    • (edited May 9th 2017)

    I finally created an entry internal category in homotopy type theory.

    There is old discussion of this topic which I had once written at category object in an (infinity,1)-category in the sub-section HoTT formulation, but it’s probably good to give this a stand-alone entry, for ease of linking (such as from equivalence of categories now).

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2019

    Darin Morrison informs me that he thinks he managed to formalize general (n,r)(n,r)-categories for n,r{}n,r \in \mathbb{N} \sqcup \{\infty\} in Agda. His code is here:

    He promises to provide explanation and examples later, when he finds the time.

    diff, v8, current

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2019

    Interesting; I wonder whether it’s related to Eric Finster’s recent definition.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2019

    Right, when I pointed him to Eric’s stuff he said it didn’t look much related.

    • CommentRowNumber5.
    • CommentAuthorAli Caglayan
    • CommentTimeJan 20th 2019

    He is using –type-in-type, it will be interesting to see why this is the case.

    • CommentRowNumber6.
    • CommentAuthorGuest
    • CommentTimeJan 20th 2019
    Hi,

    Sorry for the lack of comments. I put that definition together in a bit of a hurry. I'll try to explain more soon.

    Just to respond to issues so far:

    1) it's not based on Eric's work but I am familiar with some of his stuff. From what I understand, he is using polynomials and opetopic cells. In contrast, I use inductive-recursive definitions for the telescopic discs and diagrams and the cells are what I guess one would call polygraphic (many-out).

    2) the use of type-in-type is nothing serious. Unfortunately the universe levels in Agda are pretty noisy. I have an earlier version which does not use the "r" parameter which is properly stratified. I'll fix that here soon.

    - Darin
    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeAug 24th 2019

    Checking just now, it seems that all traces or Darin Morrison’s agda-nr-cats have disappeared?!

    diff, v11, current

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeAug 25th 2019

    Intriguing.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2019

    Disappeared together with online traces of the man himself, I should add. Hope he is okay. And that his idea and code isn’t lost.

    • CommentRowNumber10.
    • CommentAuthorAHartNtkn
    • CommentTimeAug 25th 2019
    • (edited Aug 25th 2019)

    A fork of the repository is available here.

    However, it seems to be one commit behind the original.

    That fifth commit may have just added the readme, but I can’t tell.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2019
    • (edited Aug 25th 2019)

    Thanks! That’s a relief.

    I have updated the links on the nLab pages with this new pointer.

    But maybe we should store a copy of the code on the nLab server, for it not to be lost again.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeAug 25th 2019

    Simpler would just be for plenty of other people to fork it again on github. It looks like AHartNtkn already forked it, now so did I.

    • CommentRowNumber13.
    • CommentAuthorjonsterling
    • CommentTimeAug 26th 2019
    It looks like Darin has restored a repository here https://github.com/freebroccolo/agda-infinity-categories/, in which he presents the restriction to (n,1)-categories, where n can be $\infty$.
    • CommentRowNumber14.
    • CommentAuthorJonasFrey
    • CommentTimeAug 26th 2019
    • (edited Aug 26th 2019)
    nvm (is it possible to delete comments?)
    • CommentRowNumber15.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 27th 2019

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

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeAug 27th 2019

    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?

    • CommentRowNumber17.
    • CommentAuthorjonsterling
    • CommentTimeAug 27th 2019
    I haven't spoken with Darin about it in a while, but I think he was hoping that by restricting to the simpler case of (n,1) it would be easier for members of the community to understand his code and help check that it accomplishes what he hopes it does. I don't believe that Darin has discovered a flaw in the (n,r) version; however, to determine if this is a suitable definition, one has to construct some examples (such as basic constructions of infinity-categories). I hope that Darin will have time to do so -- I believe he has been very busy over the past year and it has been difficult from him to put time into this project.
    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2022

    cross-linked with the new article on Rezk completion

    diff, v14, current

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeJun 21st 2022

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

    diff, v19, current

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeAug 30th 2022

    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.

  1. 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

    diff, v20, current

    • CommentRowNumber22.
    • CommentAuthorGuest
    • CommentTimeAug 30th 2022

    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.

    • CommentRowNumber23.
    • CommentAuthorGuest
    • CommentTimeAug 30th 2022
    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeAug 30th 2022

    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.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeAug 31st 2022

    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”.

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

    Anonymous

    diff, v21, current

  3. adding motivation for (strict) univalent categories in set theory foundations

    Anonymous

    diff, v21, current

  4. better ideas section

    Anonymous

    diff, v26, current

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeSep 1st 2022

    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.)

  5. gaunt categories exist so modified the ideas section

    Anonymous

    diff, v28, current

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

    Anonymous

    diff, v28, current

  7. definitions pertaining to strict univalent categories moved to gaunt category

    Anonymous

    diff, v28, current

    • CommentRowNumber33.
    • CommentAuthorMike Shulman
    • CommentTimeSep 2nd 2022
    • 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.

    diff, v30, 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)