×

How complete is PER? (English) Zbl 0717.03028

Logic in computer science, Proc. 4th Annual Symp., Pacific Grove/CA (USA) 1989, 106-111 (1989).
Summary: [For the entire collection see Zbl 0713.00018.]
The category of partial equivalence relations on the natural numbers (PER) has been used extensively in recent years to model various forms of higher-order type theory. It is well-known that PER can be viewed as a category of sets in a non-standard model of intuitionistic Zermelo- Fraenkel set theory. The use of PER as a vehicle for modelling type theory then arises from completeness properties of this category. The purpose of this paper is to demonstrate these completeness properties, and to show that, constructively, some complete categories are more complete than others.

MSC:

03G30 Categorical logic, topoi
18A35 Categories admitting limits (complete categories), functors preserving limits, completions

Citations:

Zbl 0713.00018