On Church’s thesis in cubical assemblies
| Autor: | Taichi Uemura, Andrew Wakelin Swan |
|---|---|
| Rok vydání: | 2021 |
| Předmět: | |
| Zdroj: | Mathematical Structures in Computer Science. 31:1185-1204 |
| ISSN: | 1469-8072 0960-1295 |
| Popis: | We show that Church’s thesis, the axiom stating that all functions on the naturals are computable, does not hold in the cubical assemblies model of cubical type theory. We show that nevertheless Church’s thesis is consistent with univalent type theory by constructing a lex modality in cubical assemblies such that Church’s thesis holds in the corresponding reflective subuniverse. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|