Toot

Written by Jon Sterling on 2024-11-11 at 18:04

@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

Mentions

=> View antidote@mathstodon.xyz profile | View isAdisplayName@mathstodon.xyz profile | View rahulc29@mathstodon.xyz profile

Tags

Proxy Information
Original URL
gemini://mastogem.picasoft.net/toot/113465638760327306
Status Code
Success (20)
Meta
text/gemini
Capsule Response Time
225.726327 milliseconds
Gemini-to-HTML Time
0.673451 milliseconds

This content has been proxied by September (3851b).