Post #2121594

2025-10-28 09:25 UTC

@ltchen In Bishop's books, "setoid" is like a type, and "set" is a setoid (in his sense) equipped with an equivalence relation. So a completely different use of the terminology. Which definitions do you have in mind?

Replies (1)

@ltchen@mathstodon.xyz 2025-10-29 01:03

@MartinEscardo @typeintype recently gave a talk at TYPES'25 summarising definitions of setoids in type theory, depending on how equivalence relations are valued https://pujet.fr/pdf/types2025slides.pdf (repo: https://github.com/loic-p/setoid-universe) On top of that, Erik Palmgren gave another "setoid" intuitively by combining CZF and iterative sets: https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/from-type-theory-to-setoids-and-back/EF78A7C132460C0F20FA93CD77E9E432 Also, partial and total setoids have been considered, but I am not sure if the partial version is still in use anywhere: https://www.cambridge.org/core/journals/journal-of-functional-programming/article/setoids-in-type-theory/6A223F72737E421BD9D642C14EB5600B

Open ##2121595