Thank you for the term "quotient types", that's the first time I'm hearing that!!! I agree that this would be an amazing thing to have, but I've never seen tho

Thank you for the term "quotient types", that's the first time I'm hearing that!!! I agree that this would be an amazing thing to have, but I've never seen those anywhere in practice (not even in Idris). My gut-feeling tells me that it might not work in combination with composability in the sense that there might never be a proper global "equal" that everyone can agree one. I'm curious - besides the ones mentioned, are there any other fundamental type concepts that you would build into your own programming language? :)