Homotopy Type Theory upper type > history (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

<upper set


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

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