Announcement of the Agda fork by amy@types.pl:

The Agda developers have recently proposed codifying their official stance on LLM-generated contributions: they are "concerned about the negative effects of large language models (LLMs) on many individuals, our society, and our planet", but refuse to take any concrete action to address their own contribution to these.

Other extensions to the type theory are kept despite known inconsistencies (sized types), or being impossible to adopt without complete vertical buy-in (cumulativity, erased cubical), or simply for backwards compatibility (--guarded/@lock). In the best cases, these features are championed by a single maintainer, and keeping them well-tested against the continuous adoption of new features is a struggle when very little code uses them. Our plan is to focus on exactly one variant of the language ("full --cubical"), and to drop support for all the language features which are explicitly deprecated, inconsistent, or simply ill-understood in conjunction with this fragment.

I tried it out using Amélia's library (https://1lab.dev/) to show that free modules are projective. This is known to be equivalent to the axiom of choice and that informed the definition of projective to have mere existence of the lifted homomorphism. It was pretty ergonomic, details regarding homotopy levels were handled by hlevel and universe levels weren't bad. Automatic proof search worked with a sufficiently fleshed out structure