You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Bar Roytman (Sep 07 2020 at 18:08):There are many proposed definitions of weak infinity-groupoids which include some algebraic ones. Homotopy type theory expresses internal logic for the (infinity, 1)-category of infinity-groupoids where, to my understanding, an infinity-groupoid is determined by its (potentially context dependent) terms and terms of its iterated identity types. I am curious about why I cannot find a non-type theoretic definition of infinity-groupoids as an algebraic structure whose operations arise from valid judgements in type theory with only constructor being the identity type. Is type theory with only identity types too weak to capture the notion of an infinity-groupoid in this way?
Morgan Rogers (he/him) (Sep 08 2020 at 10:26):I don't know if they will have an answer, but I remember @Jacques Carette mentioning they were working on setoids, and they might have something interesting to say. (If I'm mistaken, my apologies!)
Jacques Carette (Sep 08 2020 at 13:38):I personally don't have anything interesting to say about this.
However, you might want to look into the work of Altenkirch and Ripacek A syntactical approach to weak ω-Groupoids (there's also some slides available), as well as Finster and Mimram's A type-theoretical definition of weak ω-categories.
The main issue in doing this are the coherence laws.