Post #2121595

@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