I can't be the only one who's very put off by PLFA referring to \Sigma (and coproducts) as "existentials" (and "disjunction"), right? Right?
@amy If you're not from the HoTT background then it's common to identify those things, especially because the inference rules correspond really closely. The Prop version of existence takes a lot more squinting to see the similarity to e.g. the first order logic rule.
I think the approach makes sense if you're trying to teach PL to the "average" computer scientist
@joey You can't define those with \Sigma! If you teach people that \exists is implemented by \Sigma, then they go on to find that e.g. the "image" of every function is isomorphic to its domain, and so they'll — rightly — tell you that what they've been taught is nonsense
@joey If you don't need a proper existential, that's fine, but \Sigma is \Sigma, not \exists. If you're gonna teach \Sigma, call it \Sigma
@amy Again, this seems like something that you care about if you're trying to make the foundation of mathematics or doing category theory or algebraic geometry, and less if you're trying to prove programs correct or mechanize the metatheory of a calculus.
Don't get me wrong, I'm not saying the HoTT way is bad, I just think it's important to recognize that it's not the *only* way and there are people who know what they're doing who get lots done a different way.
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.