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.

Root of the development

• source/index.lagda (only --safe modules).
• source/AllModulesIndex.lagda (including "unsafe" ones).
• Each subdirectory in source/ has its own index file.

Current contributors in alphabetical order of first name

Please add yourself the first time you contribute.

• Alice Laroche
• Andrew Sneap
• Andrew Swan
• Ayberk Tosun
• Brendan Hart
• Bruno Paiva
• Chuangjie Xu
• Cory Knapp
• Ettore Aldrovandi
• Fredrik Nordvall Forsberg
• Ian Ray
• Igor Arrieta (ii)
• Jon Sterling
• Kelton OBrien
• Keri D'Angelo
• Lane Biocini
• Marc Bezem
• Martin Escardo
• Nicolai Kraus
• Ohad Kammar
• Paul Levy (i)
• Paulo Oliva
• Peter Dybjer
• Simcha van Collem
• Thierry Coquand
• 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 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. Tom de Jong. Domain Theory in Constructive and Predicative Univalent Foundations. PhD thesis. School of Computer Science, University of Birmingham, UK. Submitted: 30 September 2022; accepted: 1 February 2023.

    https://etheses.bham.ac.uk/id/eprint/13401/
    Updated versions:
    https://arxiv.org/abs/2301.12405
    https://tdejong.com/writings/phd-thesis.pdf

16. 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

17. Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu. Set-Theoretic and Type-Theoretic Ordinals Coincide. Logic in Computer Science (LICS), Proceedings of LICS 2023. June 2023.

    https://doi.org/10.1109/LICS56636.2023.10175762

    Publicly available at https://arxiv.org/abs/2301.10696.

18. 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

19. Martín H. Escardó and Paulo Oliva. Higher-order Games with Dependent Types.

    Theoretical Computer Science, Special issue "Continuity, Computability, Constructivity: From Logic to Algorithms", dedicated to Ulrich Berger's 65th birthday, volume 974, 29 September 2023, available online 2 August 2023.

    https://doi.org/10.1016/j.tcs.2023.114111

20. Todd Waugh Ambridge. Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics. January 2024. University of Birmingham. PhD thesis.

    https://doi.org/10.48550/arXiv.2401.09270

21. Igor Arrieta, Martín H. Escardó and Ayberk Tosun. The Patch Topology in Univalent Foundations.

    ArXiv preprint. Available online 5 February 2024.

    https://arxiv.org/abs/2402.03134

22. Tom de Jong. Domain theory in univalent foundations I: Directed complete posets and Scott's D∞. July 2024.

    https://doi.org/10.48550/arxiv.2407.06952

23. Tom de Jong and Martín H. Escardó. Domain theory in univalent foundations II: Continuous and algebraic domains. July 2024.

    https://doi.org/10.48550/arxiv.2407.06956