首页    期刊浏览 2024年11月25日 星期一
登录注册

文章基本信息

  • 标题:Functions out of Higher Truncations
  • 本地全文:下载
  • 作者:Paolo Capriotti ; Nicolai Kraus ; Andrea Vezzosi
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2015
  • 卷号:41
  • 页码:359-373
  • DOI:10.4230/LIPIcs.CSL.2015.359
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:In homotopy type theory, the truncation operator ||-||n (for a number n greater or equal to -1) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate into n-types, which makes it hard to construct functions ||A||n -> B if B is not an n-type. This makes it desirable to derive more powerful elimination theorems. We show a first general result: If B is an (n+1)-type, then functions ||A||n -> B correspond exactly to functions A -> B that are constant on all (n+1)-st loop spaces. We give one "elementary" proof and one proof that uses a higher inductive type, both of which require some effort. As a sample application of our result, we show that we can construct "set-based" representations of 1-types, as long as they have "braided" loop spaces. The main result with one of its proofs and the application have been formalised in Agda.
  • 关键词:homotopy type theory; truncation elimination; constancy on loop spaces
国家哲学社会科学文献中心版权所有