1
$\begingroup$

I am aware of similar question in MO whose comment nicely lists zoo of possible models and only such models can be formalized. But I have not found any implementation so far which I could use or extend.

I searched Coq HoTT library, Agda HoTT library which includes truncated, finite-n version. Isabelle HOTT, of course, have nothing about this. And the chats in Lean (here and here) community does not show any signs of implementation.

I am aware of homotopy-io and it is not even a formal math, just JavaScript. So, maybe one can start by rewriting this for some proof assistant.

My question is - are there any implementation of any model of ∞-categories for any proof assistant. And if not - what is the challenge and is it so hard to solve it?

I see that ∞-category field is thriving. There are efforts to transfer notions from the classical category theory to ∞-categories, so - lot of new and more general theories. There is monumental work in physics which is done in ∞-toposes. So, any automation of such theory building or application requires formalization of ∞-categories again. And everything that is being done by Jacob Lurie or Emily Riehl deserves formalization too.

How shall we move forward with formalization and automation of this part of math?

Note added. I am reading "A type theory for synthetic ∞-categories" and this article, as I understand, figures out that HoTT types are quite general, but it also constructs types which correspond to (∞,1)-categories. So - it may be so, that formalization of ∞-categories reduces to writing down this article. It was announced in 2017, so, it may be possible that someone has done it or is actively doing it. These may be good news, that the hardest part has been done.

Note added. I have no requirement, that formalization should be done in the environment with the trusted core. However, I feel, that it is better to have formalization as part of library of some ecosystem (which in its entirety can be used in machine learning) and not as implementation of standalone calculus from which is hard to make links to the wider libraries.

Improve this question
$\endgroup$
8
  • 3
    $\begingroup$ I don't quite understand the javascript part. Does rewriting, say, agda using javascript (it is currently written in haskell) discredit its results somehow? $\endgroup$
    – Trebor ♦
    Commented Aug 11, 2023 at 11:33
  • 3
    $\begingroup$ Agda doesn't have a trusted core, in fact homotopy.io probably has fewer bugs than agda. But if what you want is that level of trustworthiness it is fine, and you should probably include that in your question. $\endgroup$
    – Trebor ♦
    Commented Aug 11, 2023 at 14:12
  • 1
    $\begingroup$ Agda has a lot of cubical type theory going on. $\endgroup$
    – Ronald J. Zallman
    Commented Aug 11, 2023 at 19:49
  • 1
    $\begingroup$ Mathlib does not appear to have the Whitehead theorem. $\endgroup$
    – Ronald J. Zallman
    Commented Aug 11, 2023 at 19:51
  • 2
    $\begingroup$ Since you talk about synthetic inf-category theory, do you know that it is implemented in the proof assistant rzk? $\endgroup$
    – Trebor ♦
    Commented Aug 12, 2023 at 17:19

2 Answers 2

Reset to default
2
$\begingroup$

I believe rzk is the Proof Assistant and sHoTT is the formalisation. :)

On the other hand, they work with synthetic ∞-categories, not a model, so maybe this doesn't really answer your question...

Improve this answer
$\endgroup$
1
  • $\begingroup$ I wrote the answer first and only after that looked at the comments to the question, sorry... 😅 $\endgroup$
    – Alex Chichigin
    Commented Aug 15, 2023 at 7:22
2
$\begingroup$

Much of current research is aimed at developing a nice theory in which one can reason about higher categories directly, as opposed to taking traditional models of higher categories and verifying them in a proof assistant.

I understand the "synthetic" approach to homotopy and higher category theory as attempts to develop a "logic for higher structures", so they give a new way to talk about higher structures in a computationally well-behaved and convenient way.

All Cubical Agda, rzk, homotopy.io and rewalt follow a synthetic approach, but are based on different proposals to what the logic of higher structures could be: Cubical type theory is inspired by cubical sets, rzk by simplicial sets, homotopy.io by globular associative n-categories, and rewalt by diagrammatic sets.

So I'd suspect that the reason that there is little work on formalising models of higher categories is that we don't yet know what the best way to do it is. One could take traditional models and enter them in Coq, Lean or Agda, but this would require a considerable amount of work and would probably not be of much use. The hope is that reasoning synthetically will at some point be easier than traditional approaches to higher category theory and that mathematicians using higher categories can simply work in a proof assistant based on one of the ones which are currently being explored.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.