| Title: |
A Zoo of Continuity Properties in Constructive Type Theory |
| Authors: |
Baillon, Martin; Forster, Yannick; Mahboubi, Assia; Pédrot, Pierre-Marie; Piquerez, Matthieu |
| Contributors: |
Martin Baillon and Yannick Forster and Assia Mahboubi and Pierre-Marie Pédrot and Matthieu Piquerez |
| Publisher Information: |
Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| Publication Year: |
2025 |
| Collection: |
DROPS - Dagstuhl Research Online Publication Server (Schloss Dagstuhl - Leibniz Center for Informatics ) |
| Subject Terms: |
type theory; constructive mathematics; continuity; Coq |
| Description: |
Continuity principles stating that all functions are continuous play a central role in some schools of constructive mathematics. However, there are different ways to formalise the property of being continuous in constructive foundations. We analyse these continuity properties from the perspective of constructive reverse mathematics. We work in constructive type theory, which can be seen as a minimal foundation for constructive reverse mathematics. We treat continuity of functions F : (Q → A) → R, i.e. with question type Q, answer type A, and result type R. Concretely, we discuss continuity defined via moduli, making the relevant list L : LQ of questions explicit, dialogue trees, making the question-answer process explicit as inductive tree, and tree functions, making the question-answer process explicit as function. We prove equivalences where possible and isolate necessary and sufficient axioms for equivalence proofs. Many of the results we discuss are already present in the works of Hancock, Pattinson, Ghani, Kawai, Fujiwara, Brede, Herbelin, Escardó, and others. Our main contribution is their formulation over a uniform foundation, the observation that no choice axioms are necessary, the generalisation to arbitrary types from natural numbers where possible, and a mechanisation in the Coq/Rocq proof assistant. |
| Document Type: |
article in journal/newspaper; conference object |
| File Description: |
application/pdf |
| Language: |
English |
| Relation: |
Is Part Of LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.9 |
| DOI: |
10.4230/LIPIcs.FSCD.2025.9 |
| Availability: |
https://doi.org/10.4230/LIPIcs.FSCD.2025.9; https://nbn-resolving.org/urn:nbn:de:0030-drops-236245; https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.9 |
| Rights: |
https://creativecommons.org/licenses/by/4.0/legalcode |
| Accession Number: |
edsbas.3AC1C3BB |
| Database: |
BASE |