Various new theorems in constructive univalent mathematics written in Agda

This development was started by Martin Escardo in 2010 as an svn project, and transferred to github Monday 5th February 2018.

If you contribute, please add your full (legal or adopted) name and date at the place of contribution.

An html rendering of the Agda code is hosted at Martin Escardo's institutional web page.

How to cite

You can use the following BibTeX entry to cite TypeTopology:

@misc{type-topology,
  title    = {{TypeTopology}},
  author   = {Escard\'{o}, Mart\'{i}n H. and {contributors}},
  url      = {https://github.com/martinescardo/TypeTopology},
  note     = {{Agda} development},
}

If you are citing only your own files, then create a different bibtex file with only your name as author.

Current contributors in alphabetical order of first name

• Alice Laroche
• Andrew Sneap
• Ayberk Tosun
• Brendan Hart
• Chuangjie Xu
• Cory Knapp
• Ettore Aldrovandi
• Fredrik Nordvall Forsberg (ii)
• Igor Arrieta (iii)
• Jon Sterling
• Keri D'Angelo
• Marc Bezem (i)
• Martin Escardo
• Nicolai Kraus (ii)
• Ohad Kammar
• Paul Levy (i)
• Paulo Oliva
• Peter Dybjer (i)
• Thierry Coquand (i)
• Todd Waugh Ambridge
• Tom de Jong
• Vincent Rahli

(i) These authors didn't write any single line of Agda code here, but they contributed to constructions, theorems and proofs via the hands of Martin Escardo.

(ii) These authors didn't write any single line of Agda code here, but they contributed to constructions, theorems and proofs via the hands of Tom de Jong.

(iii) These authors didn't write single line of Agda code here, but they contributed to constructions, theorems and proofs via the hands of Ayberk Tosun.

Publications resulting from TypeTopology

1. Martín H. Escardó. Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics. The Journal of Symbolic Logic, Volume 78 , Issue 3 , 2013 , pp. 764 - 784.

   https://doi.org/10.2178/jsl.7803040

2. Martín H. Escardó. Continuity of Gödel's system T functionals via effectful forcing. Electronic Notes in Theoretical Computer Science, Volume 298, 2013, Pages 119-141. MFPS XXIX

   https://doi.org/10.1016/j.entcs.2013.09.010

3. Nicolai Kraus, Martín H. Escardó, T. Coquand, T. Altenkirch. Generalizations of Hedberg's Theorem. In: Hasegawa, M. (eds) Typed Lambda Calculi and Applications. TLCA 2013. Lecture Notes in Computer Science, vol 7941. Springer.

   https://doi.org/10.1007/978-3-642-38946-7_14

4. Martín H. Escardó. Constructive decidability of classical continuity. Mathematical Structures in Computer Science, Volume 25 , Special Issue 7: Computing with Infinite Data: Topological and Logical Foundations Part 1 , October 2015 , pp. 1578 - 1589 DOI:

   https://doi.org/10.1017/S096012951300042X

5. Martín H. Escardó and Chuangjie Xu. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015).

   https://doi.org/10.4230/LIPIcs.TLCA.2015.153

6. Martín H. Escardó and T. Streicher. The intrinsic topology of Martin-Löf universes. Annals of Pure and Applied Logic, Volume 167, Issue 9, 2016, Pages 794-805.

   https://doi.org/10.1016/j.apal.2016.04.010

7. Martín H. Escardó and Cory Knapp. Partial elements and recursion via dominances in univalent type theory. Leibniz International Proceedings in Informatics (LIPIcs), Proceedings of CSL 2017.

   https://doi.org/10.4230/LIPIcs.CSL.2017.21

8. Nicolai Kraus, Martín H. Escardó, T. Coquand, T. Altenkirch. Notions of Anonymous Existence in Martin-Löf Type Theory. Logical Methods in Computer Science, March 24, 2017, Volume 13, Issue 1.

   https://doi.org/10.23638/LMCS-13(1:15)2017

9. Tom de Jong. The Scott model of PCF in univalent type theory. Mathematical Structures in Computer Science, Volume 31, Issue 10 - Homotopy Type Theory 2019, July 2021.

   https://doi.org/10.1017/S0960129521000153

10. Martín H. Escardó. The Cantor-Schröder-Bernstein Theorem for ∞-groupoids. Journal of Homotopy and Related Structures, 16(3), 363-366, 2021.

    https://doi.org/10.1007/s40062-021-00284-6

11. Martín H. Escardó. Injective types in univalent mathematics. Mathematical Structures in Computer Science, Volume 31 , Issue 1 , 2021 , pp. 89 - 111.

    https://doi.org/10.1017/S0960129520000225

12. Tom de Jong and Martín H. Escardó. Domain Theory in Constructive and Predicative Univalent Foundations. Leibniz International Proceedings in Informatics (LIPIcs), Volume 183 - Proceedings of CSL 2021, January 2021.

    https://doi.org/10.4230/LIPIcs.CSL.2021.28

13. Dan R. Ghica and Todd Waugh Ambridge. Global Optimisation with Constructive Reals. Logic in Computer Science (LICS), Proceedings of LICS 2021, June 2021.

    https://doi.org/10.1109/LICS52264.2021.9470549

14. Tom de Jong and Martín H. Escardó. Predicative Aspects of Order Theory in Univalent Foundations. Leibniz International Proceedings in Informatics (LIPIcs), Volume 195 - Proceedings of FSCD 2021, July 2021.

    https://doi.org/10.4230/LIPIcs.FSCD.2021.8

15. Ayberk Tosun and Martín H. Escardó. Patch Locale of a Spectral Locale in Univalent Type Theory. Electronic Notes in Theoretical Informatics and Computer Science, Volume 1 - Proceedings of MFPS XXXVIII, February 2023.

    https://doi.org/10.46298/entics.10808

16. Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu. Set-Theoretic and Type-Theoretic Ordinals Coincide. To appear at LICS 2023. June 2023.

    https://arxiv.org/abs/2301.10696

17. Tom de Jong and Martín H. Escardó. On Small Types in Univalent Foundations. Logical Methods in Computer Science, Volume 19, Issue 2, May 2023.

    https://doi.org/10.46298/lmcs-19(2:8)2023