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