We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Fixing statement about the decidability of a restricted form of η for False
Update: clarifying when an heterogeneous is John Major, clarifying when extensionality is more than η, adding syntactic equality, clarifying the rôle of the polarity of a connective when formulating η, clarifying some conditions for η to be decidable or not, for adding various terminology (e.g. typal equality)
Some reworking
Add some concrete notations
Include definitional equality in the picture
initial version based on Zulip post by Hugo Herbelin