@antidote @isAdisplayName @rahulc29 I think the big one is "Equality is proved by tactics anyway, so there is no need to ensure that definitional equality has any global properties whatsoever". This leads to bad technical conclusions, like "It is OK that definitional equality is not transitive, you use 'simp' instead and nobody expects 'simp' to be able to reason transitively anyway".
This harmful idea is related to another harmful idea embedded in the project, namely "We don't need no stinkin', pointy-headed type theorists”.
=> More informations about this toot | View the thread | More toots from jonmsterling@mathstodon.xyz
=> View antidote@mathstodon.xyz profile | View isAdisplayName@mathstodon.xyz profile | View rahulc29@mathstodon.xyz profile
text/gemini
This content has been proxied by September (3851b).