A pequiv is a partial equivalence, a representation of a bijection between a subset of α and a subset of β