Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
In this work we consider an extension MFcind of the Minimalist Foundation MF for predicative constructive mathematics with the addition of inductive and coinductive definitions sufficient to generate Sambin's Positive topologies, namely Martin-L\"of-Sambin formal topologies equipped with a...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-11-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/7321/pdf |