Showing changes from revision #2 to #3:
Added | Removed | Changed
Let be a preordered type, and let be a sub-preordered type of with a monic monotonic 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.
Last revised on June 9, 2022 at 23:46:01. See the history of this page for a list of all contributions to it.