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.
Reading some of the other discussion, it’s possible that I misinterpreted what was meant here. Did you mean to be talking about categories enriched over prop-valued equivalence relations, rather than over setoids?
It seems clear that there are endless variations on these structures, but it’s not clear to me that we need pages about all of them. I think it’s sensible to have a page about E-categories because they are a standard concept in type theory, but I don’t know that we need a page about equivalence-relation-enriched categories. Is there some intended application?
Also, please sign your edits with a distinguishable pseudonym!
1 to 5 of 5