Questions tagged [soft-question]

For questions whose answers can't be objectively evaluated as correct or incorrect, but which are still relevant to this site. Please be specific about what you are after.

Filter by
Sorted by
Tagged with
14 votes
2 answers
202 views

What are the advantages to impredicativity?

Mostly when I read about impredicativity I see people bemoaning its downsides. But it's not clear to me why I would want impredicativity in the first place. Impredicativity is useful for analyzing ...
user avatar
11 votes
1 answer
148 views

Naming conventions (letter case, underscores, &c) for Coq

Does Coq have an established convention/style for constructors, variables, terms, &c? An established convention that isn't exceptionless is totally fine. For example, terms should be lowercase ...
user avatar
  • 2,467
14 votes
1 answer
255 views

Why should you "never resort to polymorphism when initiality would do"?

In the concluding statement of "universe hierarchies", Conor McBride calls it [...] that key lesson which I learned from James McKinna: never resort to polymorphism when initiality will do. ...
user avatar
8 votes
2 answers
281 views

Which proof assistant would you advise me to learn (in 2022) considering my interests?

I am a math teacher in college. I’m very interested in type theory. So far, I got the general idea of it but I would like to go deeper. I am interested in philosophy of maths, in foundations of maths, ...
user avatar
  • 181