Showing changes from revision #1 to #2:
Added | Removed | Changed

Definition

Let $P$ be a preordered type, and let $A$ be a sub-preordered type of $P$ with a monicmonotonic function$m:A \subseteq P$. $A$ is a lower type on $P$ or a (0,1)-presheaf on $P$ if $A$ comes with a term

where $fiber(m, p)$ is the fiber of $m$ at $p$ and $\Vert [\mathrm{fiber}(m,p)]\mathrm{fiber}(m,p)\Vert $ \Vert \left[fiber(m, fiber(m, p) \Vert \right] says that the fiber of $m$ at $p$ is inhabited.

If $P$ is a set, then $A$ is also a set and thus called a lower set.