@c_cube @ncf Yes… It is one of those things that could make sense as an admissible rule, depending on what sorts you have, but which cannot be derived in a way that respects variable scope. The usual “proofs” are just invalid in this sense — but these invalid proofs fail to cause problems because the sorts are interpreted by nonempty sets.
=> More informations about this toot | View the thread | More toots from jonmsterling@mathstodon.xyz
=> View c_cube@octodon.social profile | View ncf@types.pl profile
text/geminiThis content has been proxied by September (3851b).