Inverse Semigroupoid Semantics

[TOTBWF]

The semantics for NuPRL's types are based off of Partial Equivalence Relations, where a : A if a = a in A under the associated PER. In short, the types form partial setoids. However, this discards a lot of very interesting information, namely, why things are equal.

With this in mind, we can see that NuPRL's types are really just h-sets/0-truncated. However, Groupoids aren't quite the model we are looking for, as they miss out on the Partial portion of PER. Taking this into consideration, we can see that types form Inverse Semigroupoids over the set of (closed) terms.