daniel gratzer on Nostr: The lack of injective type-constructors is also pretty rough (related but distinct ...

The lack of injective type-constructors is also pretty rough (related but distinct from lack of decidable equality). It means that a hypothetical type-checker will not only be at best a semi-decision procedure, but also require a lot of annotations if it's to be robust at all.

That said, I use ETT all the time in my work, just limited to pen-and-paper work rather than formalized in a proof assistant.