Let be a preordered type, and let be a sub-preordered type of with a monicmonotonic function . is an upper type on or a (0,1)-copresheaf on if comes with a term
where is the fiber of at and says that the fiber of at is inhabited.
If is a set, then is also a set and thus called an upper set.