Definition. The category of partial equivalence relations [math-W6F9]

2025-03-09 · Lîm Tsú-thuàn
Categorical Logic and Type Theory

The category of PERs is consist of

  1. Each object is a PER R∈PERR \in \text{PER}
  2. Morphisms R→SR \to S are functions f:N/R→N/Sf : \N / R \to \N / S between the quotient sets, which are tracked, i.e. for some code e∈Ne \in \N, one has ∀n∈∣R∣.f([n]R)=[e⋅n]S\forall n \in |R|. f([n]_R) = [e \cdot n]_S where e⋅ne \cdot n stands for Kleene application: apply ee-th partial function ϕe\phi_e to nn.

terminal object [local-1]

{(0,0)}\{ (0,0) \} and N×N\N \times \N both are terminal objects of the category.

Proof [local-0]

For S={(0,0)}S = \{ (0,0) \}, we can see the unique function ff is

∀n∈∣R∣.f([n]R)=[e⋅n=ϕe(n)=0]S\forall n \in |R|. f([n]_R) = [e \cdot n = \phi_e(n) = 0]_S

since the only element of N/{(0,0)}\N / \{ (0,0) \} is [0][0], ϕe\phi_e just need to be a constant function maps to 00. In fact, it's easy to see why for each a∈Na \in \N, the relation {(a,a)}\{ (a,a) \} is a terminal object.

For S=N×NS = \N \times \N, we can see the unique function ff is

∀n∈∣R∣.f([n]R)=[e⋅n]S\forall n \in |R|. f([n]_R) = [e \cdot n]_S

ϕe\phi_e can be any function that codomain is N\N, because for all n∈Nn \in \N, the [n]S[n]_S is the same.