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.
Could we add some references on usage of this terminology? Or else a comment that it’s meant to be new terminology?
But I see that this is material being ported over from extensional category (homotopytypetheory) (which doesn’t attribute the terminology either).
This page is also unneeded, since the functor into Set for any concrete category is faithful, and because Set is well pointed and morphisms out of the terminal object in Set are in bijection with elements, morphisms of any concrete category satisfy function extensionality.
Anonymous
While I don’t regret that the entry is gone, I don’t understand that this is the reason to remove it: Certainly the point of the entry was to apply to foundations where the assumptions in #3 fail.
1 to 4 of 4