I am aware of similar question in MO https://mathoverflow.net/questions/400974/can-%E2%88%9E-category-be-defined-in-proof-assistants 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 (https://github.com/HoTT/Coq-HoTT), Agda HoTT library (https://agda.readthedocs.io/en/v2.6.3/language/cubical.html) which includes truncated, finite-n version (https://github.com/TOTBWF/agda-higher-categories). Isabelle HOTT, of course, have nothing about this. And the chats in Lean community does not show any signs of implementation (https://leanprover-community.github.io/archive/stream/113488-general/topic/Lean.20vs.20Coq.html, https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/quasicategories/near/165386120).

I am aware of https://github.com/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 https://ncatlab.org/schreiber/files/dcct161227.pdf 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 https://arxiv.org/abs/1705.07442 "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.

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.

I am aware of similar question in MO https://mathoverflow.net/questions/400974/can-%E2%88%9E-category-be-defined-in-proof-assistants 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 (https://github.com/HoTT/Coq-HoTT), Agda HoTT library (https://agda.readthedocs.io/en/v2.6.3/language/cubical.html) which includes truncated, finite-n version (https://github.com/TOTBWF/agda-higher-categories). Isabelle HOTT, of course, have nothing about this. And the chats in Lean community does not show any signs of implementation (https://leanprover-community.github.io/archive/stream/113488-general/topic/Lean.20vs.20Coq.html, https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/quasicategories/near/165386120).

I am aware of https://github.com/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 https://ncatlab.org/schreiber/files/dcct161227.pdf 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?

I am aware of similar question in MO https://mathoverflow.net/questions/400974/can-%E2%88%9E-category-be-defined-in-proof-assistants 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 (https://github.com/HoTT/Coq-HoTT), Agda HoTT library (https://agda.readthedocs.io/en/v2.6.3/language/cubical.html) which includes truncated, finite-n version (https://github.com/TOTBWF/agda-higher-categories). Isabelle HOTT, of course, have nothing about this. And the chats in Lean community does not show any signs of implementation (https://leanprover-community.github.io/archive/stream/113488-general/topic/Lean.20vs.20Coq.html, https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/quasicategories/near/165386120).

I am aware of https://github.com/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 https://ncatlab.org/schreiber/files/dcct161227.pdf 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 https://arxiv.org/abs/1705.07442 "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.