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.
and now I even ended up creating a new floating table of contents: equality and equivalence - contents
(all I wanted to originally was to create an elementary entry linear equation…)
I have added to equality and equivalence - contents all the qualifiers of “equality” that I think we have:
definitional, propositional, computational, judgemental, extensional, intensional, decidable
Many of these currently just redirect to equality itself. But that could change.
I created a stub for judgmental equality since it was requested by other entries. Mainly this stub currently points to an article by Robin Adams, which I gather is regarded as important.
Then I also added the list with all of the notions of equivalences of categories that I know we have, I might be missing some, though:
equivalence of categories, adjoint equivalence, weak equivalence of internal categories, Morita equivalence, equivalence of 2-categories, equivalence of (∞,1)-categories
There might be more to be added.
(And of course I have added this as a floating TOC to all the relevant entries.)
1 to 2 of 2