# Homotopy Type Theory upper type > history (changes)

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 monic monotonic function $m:A \subseteq P$. $A$ is an upper type on $P$ or a (0,1)-copresheaf on $P$ if $A$ comes with a term

$\lambda: \prod_{a:A} \prod_{p:P} (m(a) \leq p) \times \Vert fiber(m, p) \Vert$

where $fiber(m, p)$ is the fiber of $m$ at $p$ and $\Vert fiber(m, p) \Vert$ says that the fiber of $m$ at $p$ is inhabited.

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