Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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).
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.
Interesting; I wonder whether it’s related to Eric Finster’s recent definition.
Right, when I pointed him to Eric’s stuff he said it didn’t look much related.
He is using –type-in-type, it will be interesting to see why this is the case.
Checking just now, it seems that all traces or Darin Morrison’s agda-nr-cats have disappeared?!
Intriguing.
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.
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.
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.
@Jonas no, but you can blank them as have.
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?
1 to 17 of 17