A topological reading of inductive and coinductive definitions in Dependent Type Theory
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909160932638720 |
|---|---|
| author | Sabelli, Pietro |
| author_facet | Sabelli, Pietro |
| contents | In the context of dependent type theory, we show that coinductive predicates have an equivalent topological counterpart in terms of coinductively generated positivity relations, introduced by G. Sambin to represent closed subsets in point-free topology. Our work is complementary to a previous one with M.E. Maietti, where we showed that, in dependent type theory, the well-known concept of wellfounded trees has a topological equivalent counterpart in terms of proof-relevant inductively generated formal covers used to provide a predicative and constructive representation of complete suplattices. All proofs in Martin-Löf's type theory are formalised in the Agda proof assistant. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_03494 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A topological reading of inductive and coinductive definitions in Dependent Type Theory Sabelli, Pietro Logic Logic in Computer Science In the context of dependent type theory, we show that coinductive predicates have an equivalent topological counterpart in terms of coinductively generated positivity relations, introduced by G. Sambin to represent closed subsets in point-free topology. Our work is complementary to a previous one with M.E. Maietti, where we showed that, in dependent type theory, the well-known concept of wellfounded trees has a topological equivalent counterpart in terms of proof-relevant inductively generated formal covers used to provide a predicative and constructive representation of complete suplattices. All proofs in Martin-Löf's type theory are formalised in the Agda proof assistant. |
| title | A topological reading of inductive and coinductive definitions in Dependent Type Theory |
| topic | Logic Logic in Computer Science |
| url | https://arxiv.org/abs/2404.03494 |