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 yeah this really irks me… there’s so much ??? when it comes to the pedagogy around Sigma types

@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 @joey If they're working in MLTT, they should eventually learn that, to get the isomorphisms you want/don't want, you need setoids. In that case, ∃ *is* implemented by Σ, with a specific choice of equivalence relation.

@amy @joey Well, if you follow on directly from PLFA, you do.

@amy Right but if you don't have univalence then who cares if they're isomorphic?

@joey because the image should be a subtype of the codomain?

@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.

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.