Hung out with
bhudson in the afternoon. Saw the science & industry museum, had some dinner, chatted about theory and PL and academia and stuff. Good times.I had a thought or two about partial equivalence relations in the shower this morning --- they're something I remember Andrej Bauer being very big on when he was back around CMU working with Dana Scott. The definition's really simple: a partial equivalence relation (often shortened to PER) is a relation that's transitive and symmetric. Just like an equivalence relation, but you drop reflexivity.
I seem to recall the setting in which you use them in realizability theory is the underlying set is typically something like the natural numbers thought of as Gödel-numbers of some data structure, and you're allowed to say that some numbers aren't valid codes at all (the partiality of the relation) and some numbers despite being different numbers code up the same data structure (the equivalence aspect of the relation).
So "cutting down a set to leave just the good stuff" and "quotienting by some relation" are two really common themes in mathematics generally, and in category theory we call them "taking equalizers" and "taking coequalizers". I found it interesting that PERs are sort of doing both at once, and not in any particular order: I could think of a PER as beginning life as a set that is first cut down and then quotiented out, or as a set that's first quotiented out and then cut down.
I then found myself meditating on a diagram that can be derived from any PER, namely
A ->> B v v | | v v N ->> C
Where N is the underlying set of the PER, A is the subset of N for which reflexivity holds, B is the set of equivalence classes in the PER, and C is the union of B together with every point of N for which reflexivity falis.
The funny thing is that this diagram is (I think) both a pushout and a pullback.
Is there anything special about such diagrams in other categories? Do they behave kind of like "PER objects"?