Showing changes from revision #1 to #2:
Added | Removed | Changed
Definition
Let be a preordered type, and let be a sub-preordered type of with a monicmonotonic function . is a lower type on or a (0,1)-presheaf 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 a lower set.