Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Made a pdf copy for:
To further clarify this it would help to hyperlink “extensionality principles”. We have extension (semantics), but currently this does not really explain much.
Looking around, I see that the first paragraph of Wikipedia’s entry Extensionality is helpful. It would be nice if we had something along these lines on the nLab.
I have added reference to
and added pointers in the text to where concretely (on which pages) Streicher and then Hofman touch on the issue at hand.
I have also adjusted the wording throughout, in particular in the “Remark on terminology” (now here).
(It is a pity that such an important topic ended up with such a murky and confusing terminology.)
1 to 5 of 5