Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

category: redirected to nlab

Let $P$ be a preordered type, and let $A$ be a sub-preordered type of $P$ with a 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**.

- posite?
- upper type
- ideal?
- filter

Last revised on June 9, 2022 at 23:46:01. See the history of this page for a list of all contributions to it.