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


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 an upper type on PP or a (0,1)-copresheaf on PP if AA comes with a term

λ: a:A p:P(m(a)p)×fiber(m,p)\lambda: \prod_{a:A} \prod_{p:P} (m(a) \leq p) \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 an upper set.

See also

Revision on March 12, 2022 at 18:36:46 by Anonymous?. See the history of this page for a list of all contributions to it.