Just to wrap this up:

At *setoid* I have now compiled a list of references (here) for who says what about the definition of setoids.

If people got into a habit of citing where they draw their ideas from, this would be easier, but a pretty clear picture emerges:

Originally, starting with Martin Hofmann’s original definition’in 1995, people took setoids to be equivalence relations, and all of the StacksPropject, Wikipedia and haskell.hackage still think that this is the accepted definition. Also, one can argue that this is what Bishop actually had in mind, back in the 1960s.

However, starting around 2012, apparently, people started dropping the prop-truncation axiom on the relation and hence consiered setoids to be pseudo-equivalence relation. On the one hand this may feel more natural in type theory, on the other hand it’s the version of the definition that makes the category of setoids be an exact completion, and that last fact seems to have been drawing more attention, lately.

]]>The main point that should be highlighted up front is who says that setoids are pseudo-equivalence relations and why and how that squares with Bishop’s writings which suggest, I think, that it should actually be equivalence relations. But I guess we should have this discussion in the other thread…

]]>Oh, I see. I’m not expert either, but I’m glad you dug that out.

The article setoid has some good stuff in it, but it doesn’t look easy to read in its current state. I’ll try to make some time to look it over and see if I can make any improvements.

]]>as was explained

This needs attention. What happened was that the entry *setoid* had no references or other justification for its terminology, when an anonymous editor came in here with a major rewrite. In reaction I tried tried to dig out the original references I could find. But I am not an expert on the (thorny) history of notions of construcive mathematics and nobody who is has touched the entry since.

Re #25: no, as was explained at setoid, the term traces to Martin Hoffman’s 1995 PhD thesis, and is widely used I believe. (’Culprit’ is not a nice word, IMO.)

]]>added another historical reference

- George W. Mackey, §11 of:
*Ergodic theory and virtual groups*, Mathematische Annalen**166**(1966) 187–207 [doi:10.1007/BF01361167]

and grouped the early writings of Higgins with this.

Incidentally, Higgins attributes the study (if not the definition) of groupoids to

- Charles Ehresmann,
*Catégories et structures*, Dunod, Paris, (1965)

which recently we have been trying in vain to get hold of, elsewhere.

]]>I suspect that Toby Bartels might be the original culprit on the nlab behind the use of “setoid” to mean a “set with an equivalence relation”, with other editors later following him in that step.

]]>removing query box

+– {: .query} Mike: It’s not clear to me that the notion of “free equivalence relation” doesn’t make sense. Can’t I talk about a left adjoint to the forgetful functor from equivalence relations to, say, directed graphs? Maybe sets-equipped-with-a-binary-relation would be more appropriate, but either one works fine.

Ronnie: Are you sure this forgetful functor equivalence relations to directed graphs has a left adjoint? Suppose the directed graph $\Gamma$ has one vertex $x$ and one loop $u:x \to x$. The free groupoid on $\Gamma$ is the group of integers, which as a groupoid is not an equivalence relation.

*Toby*: But there is still a free setoid (set equipped with an equivalence relation) on $\Gamma$; it is the point. As a groupoid, it is not the same as the free groupoid on $\Gamma$, although it *is* the same as the free setoid on the free groupoid on $\Gamma$. If there's an advantage to working with groupoids, perhaps it's that the free groupoid functor preserves distinctions that the free setoid functor forgets? (In this case, a distinction preserved or forgotten is that between $\Gamma$ and the point, which as a graph does not have $u$.)
=–

Anonymous

]]>A groupoid is a category $C$ with a contravariant endofunctor $(-)^{-1}:C^\op \to C$ which is the identity-on-objects and which satisfies $f \circ f^{-1} = 1_B$ and $f^{-1} \circ f = 1_A$ for all morphisms $f:Hom(A, B)$.

]]>Typos

]]>added pointer to:

- Birgit Richter, Section 1.2 of:
*From categories to homotopy theory*, Cambridge Studies in Advanced Mathematics 188, Cambridge University Press 2020 (doi:10.1017/9781108855891, book webpage, pdf)

changed all “delooping groupoid” in the page to “delooping groupoid” and will give this its own little page now.

]]>Mentions codiscrete groupoids.

Yuning Feng

]]>typo

]]>@Marc you are right, thank you for the clarification (i wasn’t thinking of $\eta(y)$ as a morphism)

giorgio s

]]>@giorgio: o.k. let’s dissect the statement of Lemma 2.7 step by step:

(1) $F_2$ and $F^{'}_2$ are functors from $\mathcal{G}_2$ to $\mathcal{G}_3$.

(2) So the natural map $\eta : F^{'}_2 \to F_2$ should assign to every object $y \in \mathcal{G}_2$ a morphism $\eta(y) \in \mathcal{G}_3(F^{'}_2(y),F_2(y))$.

(3) Precomposing with $F_1$ gives for every object $x \in \mathcal{G}_1$ first the object $F(x) \in \mathcal{G}_2$ and then (with $y = F_1(x)$ in (2)) a morphism $\eta(F_1(x)) \in \mathcal{G}_3(F^{'}_2(F_1(x)),F_2(F_1(x)))$.

(4) Applying $F_3$ to $\eta(F_1(x))$ from (3) then gives a morphism $F_3(\eta(F_1(x))) \in \mathcal{G}_4(F_3(F^{'}_2(F_1(x))),F_3(F_2(F_1(x))))$.

So I think indices are the correct ones.

]]>@Marc, i am sorry if i am missing something but your correction (that was also necessary) still doesn’t change the fact that $\eta$ is acting on $F_1(x)\in\mathcal{G}_2$ while i think that $\eta$ can only act on elements of $\mathcal{G}_3$

giorgio s

]]>found the right ’-combination for superscript.

]]>fixed typo in component of natural map, adjusted ’ superscript in first diagram for horizontal composition and and changed $F_2$ to $F_3$.

]]>@David_Corfield regarding the same lemma (here), i don’t understand the line $(F_2 \cdot \eta \cdot F_1)(x) \;\coloneqq\; F_2(\eta(F_1(x))) \,.$

$\eta$ is said to be a homotopy. Homotopies between groupoids are defined some paragraphs before this lemma, and they can act only on the codomain of the functors they transform, therefore $\eta$ should act on $\mathcal{G}_3$. But writing $\eta(F_1(x))$ means it is acting on $\mathcal{G}_2$

]]>@David_Corfield yes, and also the same diagram is now going $\mathcal{G}_1 \rightarrow \mathcal{G}_2$ but it think it should be $\mathcal{G}_1 \rightarrow \mathcal{G}_4$. I suppose this is just a typo but, since i wasn’t completely sure, i did not correct it myself

giorgio s

]]>I’ve removed the prime off the lower $F_2$ there. Is that what you meant?

]]>giorgio s ]]>

Avoid floating first figure to display better on a mobile.

]]>