Homotopy Type Theory lower type > history (Rev #2)

 Definition

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

λ: a:A p:P(pm(a))×[fiber(m,p)]\lambda: \prod_{a:A} \prod_{p:P} (p \leq m(a)) \times \left[fiber(m, p) \right]

where fiber(m,p)fiber(m, p) is the fiber of mm at pp and [fiber(m,p)]\left[fiber(m, p) \right] says that the fiber of mm at pp is inhabited.

If PP is a set, then AA is also a set and thus called a lower set.

See also

Revision on April 21, 2022 at 13:20:00 by Anonymous?. See the history of this page for a list of all contributions to it.