Does Coq (especially HoTT Coq) has formalised pre-∞-categories and ∞-categories? If not - what can it take to do so?

[alexandre-emmanuel]

Hello!

I am MS Computer Science student at one Eastern European University and I have in mind knowledge engineering project which I would like to do in HoTT as the most expressive formalism available (which still develops, taking account modalities). E.g. I would like to work in the category of theories https://www.sciencedirect.com/science/article/pii/S0001870818303062 and therefor I will need formalisation of ∞-categories. I am aware of https://rzk-lang.github.io/rzk/en/latest/ and their excellent paper https://arxiv.org/abs/2309.08340 which shows how to formalize them in the their 3-level theory.

While I like rzk very much, they acknowledge that they are still in the process (e.g. they have just one universe, no hierarchy). So - maybe Coq HoTT project can formalize them as well? Or is already formalized? Where? I didn't find the the Cat or Category directories.

And if the formalization of ∞-categories is still in progress in Coq, then what are roadblocks and can't I complete it myself. Just few word of guidance and caution would be great advice for me. Everything remaining I can read from papers.

Of course, I am eyeing on the formalization of semantics/model theory as well and that would be ∞-toposes, but that will follow after ∞-categories.

Maybe (cubical?) Agda or Lean are more mature in this respect.

Thx in advance!
Alex

[jdchristensen]

I think the closest we have is our wild-category library, which currently lets you talk about wild categories with specified objects, 1-morphisms, 2-morphisms and 3-morphisms, and which could be extended further. But we don't in general know how to encode ∞-categories in plain HoTT.