Toot

Written by Nathaniel Burke on 2024-11-11 at 19:19

@rahulc29 @jonmsterling @antidote @isAdisplayName

The root cause is Lean allowing subsingleton elimination of inductive propositions (including the prop-valued accessibility predicate).

The ideal definitional equality that respects transitivity (and other nice properties) in this setting is undecidable, so any implementation inherently has to be broken somehow (see section 3.1 of https://github.com/digama0/lean-type-theory/releases for an example).

=> More informations about this toot | View the thread | More toots from LordQuaggan@hachyderm.io

Mentions

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

Tags