The Integers as a Higher Inductive Type
| العنوان: | The Integers as a Higher Inductive Type |
|---|---|
| المؤلفون: | Luis Scoccola, Thorsten Altenkirch |
| المصدر: | LICS |
| بيانات النشر: | ACM, 2020. |
| سنة النشر: | 2020 |
| مصطلحات موضوعية: | FOS: Computer and information sciences, Discrete mathematics, Computer Science - Logic in Computer Science, Recursion, Agda, 020207 software engineering, Natural number, Mathematics - Logic, 0102 computer and information sciences, 02 engineering and technology, Function (mathematics), Mathematical proof, 01 natural sciences, Logic in Computer Science (cs.LO), 010201 computation theory & mathematics, FOS: Mathematics, 0202 electrical engineering, electronic engineering, information engineering, Homotopy type theory, Inductive type, Logic (math.LO), computer, Universe (mathematics), computer.programming_language, Mathematics |
| الوصف: | We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to an explosion of cases. An alternative is to use set-quotients, but here we need to use set-truncation to avoid non-trivial higher equalities. This results in a recursion principle that only allows us to define function into sets (types satisfying UIP). In this paper we consider higher inductive types using either a small universe or bi-invertible maps. These types represent integers without explicit set-truncation that are equivalent to the usual coproduct representation. This is an interesting example since it shows how some coherence problems can be handled in HoTT. We discuss some open questions triggered by this work. The proofs have been formally verified using cubical Agda. 11 pages |
| DOI: | 10.1145/3373718.3394760 |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c44e066d7ecc17880cb9aa62d148e50c https://doi.org/10.1145/3373718.3394760 |
| Rights: | OPEN |
| رقم الانضمام: | edsair.doi.dedup.....c44e066d7ecc17880cb9aa62d148e50c |
| قاعدة البيانات: | OpenAIRE |
| DOI: | 10.1145/3373718.3394760 |
|---|