[[!redirects (0,1)-presheaf]] [[!redirects lower set]] ## Definition ## Let $P$ be a [[preordered type]], and let $A$ be a sub-preordered type of $P$ with a [[monic function|monic]] [[monotonic 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 $$\lambda: \prod_{a:A} \prod_{p:P} (p \leq m(a)) \times \left[fiber(m, p) \right]$$ where $fiber(m, p)$ is the [[fiber]] of $m$ at $p$ and $\left[fiber(m, p) \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__. ## See also ## * [[posite]] * [[upper type]] * [[ideal]] * [[filter]]