# 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

## Discussion Tag Cloud

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

• 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)$-categories for $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.

• 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?!

• 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

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

• CommentRowNumber19.
• CommentAuthorUrs
• CommentTimeJun 21st 2022