martinescardo / TypeTopology

TypeTopology Various new theorems in constructive univalent mathematics written in Agda This development was started by Martin Escardo at around 2010 as an project, and transferred to 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. Table of contents • How to cite this repository • Root Agda files • Current contributors • Academic publications resulting from TypeTopology • Statement of inclusion • Code of conduct • Contributing (These guidelines need reworking. But, generally, see how we write things in TypeTopology, and try to immitate our style, although departures from our style may some times be acceptable, if they are implicitly or explicitly justified.) How to cite You can use the following BibTeX entry to cite : If you are citing only your own files, then create a different bibtex file with only your name as author. Root Agda files • source/index.lagda (only 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. Use your adopted name, and not necessarily your given name, at your discretion. • Alice Laroche • Andrew Sneap • Andrew Swan • Anna Williams • Ayberk Tosun • Brendan Hart • Bruno Paiva • Carlo Angiuli • Chuangjie Xu • Cory Knapp • Ettore Aldrovandi • Evan Cavallo • Fredrik Bakke • Fredrik Nordvall Forsberg • Ian Ray • Igor Arrieta (ii) • J. A. Carr • Jakub Opršal • 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 [ ]() • 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 • 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 • 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 • Lecture Notes in Computer Science, vol 7941. Springer. https://doi.org/10.1007/978-3-642-38946-7_14 • Martín H. Escardó. *Constructive decidability of classical continuity.* [Mathematical Structures in Computer Science][MSCS], 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 • 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 • 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 • Martín H. Escardó and Cory Knapp. *Partial elements and recursion via dominances in univalent type theory.* [Leibniz International Proceedings in Informatics (LIPIcs)][LIPICS], Proceedings of CSL • https://doi.org/10.4230/LIPIcs.CSL.2017.21 • 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][LMCS], March 24, 2017, Volume 13, Issue 1. https://doi.org/10.23638/LMCS-13(1:15)2017 • 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 • Martín H. Escardó. *The Cantor-Schröder-Bernstein Theorem for ∞-groupoids.* Journal of Homotopy and Related Structures, 16(3), 363-366, • https://doi.org/10.1007/s40062-021-00284-6 • 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 • 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][CSL21], January • https://doi.org/10.4230/LIPIcs.CSL.2021.28 • Dan R. Ghica and Todd Waugh Ambridge. *Global Optimisation with Constructive Reals.* Logic in Computer Science (LICS), Proceedings of [LICS 2021][LICS21], June 2021. https://doi.org/10.1109/LICS52264.2021.9470549 • 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][FSCD21], July 2021. https://doi.org/10.4230/LIPIcs.FSCD.2021.8 • 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.c…