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

 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 \Vert fiber(m, p) \Vert

where fiber(m,p)fiber(m, p) is the fiber of mm at pp and fiber(m,p)\Vert fiber(m, p) \Vert 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 March 12, 2022 at 23:31:58 by Anonymous?. See the history of this page for a list of all contributions to it.