I just refer to Idris when speaking about dependent types. If I talk about Coq, someone will usually make a joke, which is fine as a once off, but if I want to

I just refer to Idris when speaking about dependent types. If I talk about Coq, someone will usually make a joke, which is fine as a once off, but if I want to talk about it regularly I can see that being an issue. The funny thing is that people try to pin this issue on Anglo-Saxon puritanism, when the issue is clearly political correctness. But those are the contradictions in liberal thinking for you.