Martín Escardó's published and unpublished work available online

(Research notes and mathematical and computational Haskell and Agda developments are also available below.)

1. M.H. Escardo and collaborators. TypeTopology. 2010-2024-∞, Agda code under continuous development. Many results haven't been published other than in this Agda development, which is also available at github. Additionally so far 16 papers have been published based on results first developed in TypeTopology.

2. Ayberk Tosun and M.H. Escardo. The Patch Topology in Univalent Foundations. arxiv, submitted for publication 2024.

3. M.H. Escardo and Paulo Oliva. Higher-order games with dependent types. Theoretical Computer Science, volume 974, 29th September 2023. Special issue "Continuity, Computability, Constructivity: From Logic to Algorithms", dedicated to Ulrich Berger's 65th birthday,

4. Tom de Jong and M.H. Escardo. On Small Types in Univalent Foundations. Logical Methods in Computer Science (LMCS), 19(2):8:1—8:33. May 2023.

5. Ayberk Tosun and M.H. Escardo. Patch Locale of a Spectral Locale in Univalent Type Theory. Electronic Notes in Theoretical Informatics and Computer Science, February 22, 2023, Volume 1 - Proceedings of MFPS XXXVIII.

6. Marc Bezem, Thierry Coquand, Peter Dybjer and M.H. Escardo. Type Theory with Explicit Universe Polymorphism, 28th International Conference on Types for Proofs and Programs (TYPES 2022), Leibniz International Proceedings in Informatics (LIPIcs), 2023.

7. Marc Bezem, Thierry Coquand, Peter Dybjer and M.H. Escardo. On generalized algebraic theories and categories with families, Mathematical Structures in Computer Science , Volume 31 , Special Issue 9: In Homage to Martin Hofmann , October 2021 , pp. 1006 - 1023.

8. Tom de Jong and M.H. Escardo. Predicative Aspects of Order Theory in Univalent Foundations. 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, Leibniz International Proceedings in Informatics (LIPIcs).

9. Tom de Jong and M.H. Escardo. Domain theory in constructive and predicative univalent foundations. Proceedings of CSL 2021, volume 183 of LIPIcs.

10. M.H. Escardo. The Cantor-Schröder-Bernstein Theorem for ∞-groupoids, in the Journal of Homotopy and Related Structures, published online 15th June 2021, Journal of Homotopy and Related Structures, 16(3), 363-366. There is also a blog post at the Homotopy Type Theory website, and an Agda version of the proof.

    M.H. Escardo. Compact, totally separated and well-ordered types in univalent mathematics. Abstract presented at Types 2019. Agda development.

    M.H. Escardo. Introduction to Univalent Foundations of Mathematics with Agda, March 2019. This is an html document. There is also an arxiv preprint. Lectures notes for the Midlands Graduate School in the Foundations of Computing Science, University of Birmingham, UK, 14-18th April 2019.

    M.H. Escardo. Injective types in univalent mathematics, in Mathematical Structures in Computer Science, Volume 31, Issue 1, pp. 89-111, January 2021.

    M.H. Escardo and Cory Knapp. Partial elements and recursion via dominances in univalent type theory. In proceedings of 26th EACSL Annual Conference on Computer Science Logic (CSL 2017).

    Auke Booij, M.H. Escardo, Peter L. Lumsdaine and Mike Shulman. Parametricity, automorphisms of the universe, and excluded middle. In post-proceedings of 22nd International Conference on Types for Proofs and Programs (TYPES 2016), published 2018.

    M.H. Escardo and Chuangjie Xu. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. In proceedings of 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

    Agda version, slides for the IHP 2014 talk, slides for the Mittag-Leffler 2015 talk, slides for the TLCA'2015 talk.

    Nicolai Kraus, M.H. Escardo, T. Coquand, T. Altenkirch. Notions of anonymous existence in Martin-Loef Type Theory. Logical Methods in Computer Science, March 24, 2017, Volume 13, Issue 1.

    pdf, Agda formalization (also as a zip file).

    M.H. Escardo and Paulo Oliva. The Herbrand Functional Interpretation of the Double Negation Shift. Journal of Symbolic Logic, Volume 82, Issue 2, June 2017, pp. 590-607.

    pdf.

    M.H. Escardo and A. Simpson. Abstract Datatypes for Real Numbers in Type Theory. RTA/TLCA'2014.

    pdf.

    M.H. Escardo and T. Streicher. The intrinsic topology of Martin-Lof universes. Version of Feb 2016. In Annals of Pure and Applied Logic (subsumes a draft paper included below with a similar title).

    pdf.

    M.H. Escardo and Chuangjie Xu. A constructive manifestation of the Kleene-Kreisel continuous functionals. Accepted for publication in Annals of Pure and Applied Logic, editors Thierry Coquand, Maria Emilia Maietti, Giovanni Sambin and Peter Schuster.

    pdf , Agda browsable in html, zip file

    T. Coquand, N.A. Danielsson, M.H. Escardo, U. Norell and Chuangjie Xu. Negative consistent axioms can be postulated without loss of canonicity. 3-page note.

    pdf.

    M.H. Escardo. Continuity of Godel's system T functionals via effectful forcing. MFPS'2013. Electronic Notes in Theoretical Computer Science 01/2013, volume 298, pages 119-141.

    pdf, Agda (with combinatory version of system T), Agda without comments, Agda using Church encoding of dialogues, Agda internalizing the modulus of continuity, Agda (with lambda-calculus version of system T), more.

    Chuangjie Xu and M.H. Escardo. A constructive model of uniform continuity, M. Hasegawa (Ed.): TLCA 2013, LNCS 7941, pp. 236-249. Springer, Heidelberg 2013.

    pdf, Agda

    Nicolai Kraus, M.H. Escardo, T. Coquand, T. Altenkirch. Generalizations of Hedberg's Theorem, M. Hasegawa (Ed.): TLCA 2013, LNCS 7941, pp. 173-188. Springer, Heidelberg 2013.

    pdf, Agda, A family of types that fail to be provably collapsible (also in Agda), Constant choice.

    M.H. Escardo. Constructive decidability of classical continuity. Mathematical Structures in Computer Science, published online 23 December 2014.

    pdf

    M.H. Escardo and Paulo Oliva. Computing Nash equilibria of unbounded games. Proceedings of The Turing Centenary Conference, EPiC Series, vol. 10, 53-65, Manchester, 2012.

    pdf.

    M.H. Escardo. The intrinsic topology of a Martin-Lof universe, March 2012.

    • Draft paper.
    • Slides for a talk at 4WFT (Fourth Workshop on Formal Topology), Ljubljana, Slovenia, June 2012.
    • Slides for an invited talk at DCM'2012, June, Cambridge, CiE.
    • Browse the Agda development of the intrinsic topology of a Martin-Lof universe.
    • Browse the Agda development of Rice's Theorem for the universe.

    M.H. Escardo. Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics. The Journal of Symbolic Logic (JSL), Volume 78, Number 3, September 2013, pages 764-784. An abstract for this paper was presented at Types'2011.

    • the paper, version of Jan 2013.
    • the slides for a talk about the paper.
    • Browse formal Martin-Loef-type-theory proofs written in Agda notation. (The original version.)
    • Browse ordinals in type theory written in Agda notation.
    • Browse proof translated to Coq by Vincent Siles originally advertised by him in the Agda mailing list.

    M.H. Escardo, Paulo Oliva, and Thomas Powell. System T and the product of selection functions. CSL'2011.

    pdf

    M.H. Escardo and Paulo Oliva. Bar recursion and products of selection functions. Journal of Symbolic Logic, 80(1):1-28, 2015.

    pdf

    M.H. Escardo and Paulo Oliva. Sequential Games and Optimal Strategies. In Proceedings of the Royal Society A (it is among the top 10 downloaded papers for 2011), December 2010.

    pdf

    M.H. Escardo and Paulo Oliva. The Peirce translation. To appear in APAL (revised version of a paper that was previously available here). A condensed version was published in conference proceedings (see below).

    pdf

    M.H. Escardo and Paulo Oliva. What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common. In MSFP 2010 (ACM SIGPLAN Mathematically Structured Functional Programming, ACM Press).

    pdf, companion Haskell and Agda files.

    M.H. Escardo and Paulo Oliva. The Peirce translation and the double negation shift. CiE 2010 (Computability in Europe, LNCS).

    pdf

    M.H. Escardo and Paulo Oliva. Computational interpretations of analysis via products of selection functions. CiE 2010 (Computability in Europe, LNCS).

    pdf

    M.H. Escardo and Paulo Oliva. Searchable Sets, Dubuc-Penon Compactness, Omniscience Principles, and the Drinker Paradox. In CiE 2010 (Computability in Europe) booklet.

    pdf

    See also the companion programs/proofs in Agda.

    M.H. Escardo and Paulo Oliva. Selection functions, bar recursion, and backward induction. In Mathematical Structures in Computer Science, Volume 20, Issue 2, April 2010, Cambridge University Press.

    pdf

    M.H. Escardo. Algorithmic solution of higher-type equations. To appear in JLC. A condensed version was published in CiE'2009 conference proceedings (see below).

    pdf

    M.H. Escardo. Intersections of compactly many open sets are open. arXiv:2001.06050. (A previous version of this paper (almost identical) has been available since 2005 under the name "notes on compactness".)

    pdf

    M.H. Escardo. Computability of continuous solutions of higher-type equations. Lecture Notes in Computer Science 5635 (Mathematical Theory and Computational Practice), Proceedings of the 5th Conference on Computability in Europe, CiE 2009, Springer.

    pdf

    M.H. Escardo. Semi-decidability of may, must and probabilistic testing in a higher-type setting. Electronic Notes in Theoretical Computer Science, Volume 249, 8 August 2009, Pages 219-242, Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics (MFPS 2009), Elsevier.

    pdf

    M.H. Escardo. Exhaustible sets in higher-type computation. In Logical Methods in Computer Science, volume 4, issue 3, paper 4, 2008, selected papers of the conference Logic in Computer Science 2007, editors Erich Graedel, Luke Ong, Andrew M. Pitts. https://doi.org/10.2168/LMCS-4(3:3)2008.

    pdf

    M.H. Escardo. Infinite sets that admit fast exhaustive search. In LICS'2007, IEEE, pages 443-452, Poland, Wroclaw, July.

    pdf (paper), hs (companion Haskell program extracted from the paper).

    M.H. Escardo and W.K. Ho. Operational domain theory and topology of sequential programming languages. 18 November 2006, revised May 2008. Subsumes LICS publication below with approximately the same title. Information and Computation 207 (2009) 411–437.

    pdf.

    J. Raymundo Marcial--Romero and M.H. Escardo. Semantics of a sequential language for exact real-number computation. Subsumes LICS publication below with the same title. Theoretical Computer Science, 379 (2007), no. 1-2, 120--141.

    pdf, ps, dvi.

    B. Cohen, M.H. Escardo, K. Keimel, K. The Extended Probabilistic Powerdomain Monad over Stably Compact Spaces. In: Cai, JY., Cooper, S.B., Li, A. (eds) Theory and Applications of Models of Computation. TAMC 2006. Lecture Notes in Computer Science, vol 3959. Springer, Berlin, Heidelberg, 2006.

    F. De Jaeger, M.H. Escardo and G. Santini. On the computational content of the Lawson topology, Theoretical Computer Science 357 (2006) 230--240, Elsevier.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo. Compactly generated Hausdorff locales. Annals of Pure and Applied Logic, Elsevier, volume 137, issues 1-3, pages 147-163, 2006.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo and W.K. Ho. Operational domain theory and topology of a sequential programming language. 31st December 2004, slightly revised 19th July 2005. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, June 2005, pages 427-436.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo, M. Hofmann and T. Streicher. On the non-sequential nature of the interval-domain model of exact real-number computation. Mathematical Structures in Computer Science, Cambridge University Press, volume 14, number 6, pages 803-814, December 2004.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo. Synthetic topology of data types and classical spaces. ENTCS, Elsevier, volume 87, pages 21-156, November 2004.

    pdf, ps, ps.gz, dvi, dvi.gz, handwritten manuscript (the "Barbados notes") .

    M.H. Escardo, J.D. Lawson and A. Simpson. Comparing cartesian closed categories of (core) compactly generated spaces. Topology and its Applications, Elsevier, volume 143, issues 1-3, pages 105--145, August 2004.

    pdf, ps, ps.gz, dvi, dvi.gz.

    J.R. Marcial-Romero and M.H. Escardo. Semantics of a sequential language for exact real-number computation. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 426-435, Jul 2004.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo. Joins in the frame of nuclei. Applied Categorical Structures, Springer (formerly Kluwer), volume 11, number 2, pp. 117-124, April 2003.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo. Injective locales over perfect embeddings and algebras of the upper powerlocale monad. Applied General Topology, volume 4, number 1, pp. 193-200, 2003.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo and T. Streicher. In domain realizability, not all functionals on C[-1,1] are continuous, Mathematical Logic Quarterly, Wiley, volume 48, suppl. 1, pages 41-44, October 2002.

    pdf, ps, ps.gz, dvi, dvi.gz.

    A. Bauer, M.H. Escardo and A. Simpson. Comparing functional paradigms for exact real-number computation (extended abstract). Proceedings ICALP 2002, Springer, LNCS 2380, pp. 488-500, 2002.

    pdf, ps. Unpublished full version (needs rewriting): pdf, ps.

    M.H. Escardo. Function-space compactifications of function spaces. Topology and its Applications, volume 120, issue 3, pp. 441-463, May 2002.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo and R. Heckmann. Topologies on spaces of continuous functions. Topology Proceedings, volume 26, number 2, pp. 545-564, 2001-2002.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo and A. Simpson. A universal characterization of the closed Euclidean interval (extended abstract). Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, pp.115--125. Boston, Massachusetts, June 16-19, 2001.

    paper, slides presented at MAP'2011 in Leiden, draft full version (a more polished full version will be eventually available, for the moment the paper is more readable).

    M.H. Escardo. The regular-locally-compact coreflection of a stably locally compact locale. Journal of Pure and Applied Algebra, Elsevier, volume 157, number 1, pages 41-55, March 2001.

    pdf, ps, ps.gz, dvi, dvi.gz.

    A. E. and M.H. Escardo. Integration in Real PCF. Information and Computation, Elsevier (Academic Press), volume 160, numbers 1-2, 128-166, July 2000.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo and R. Flagg. Semantic domains, injective spaces and monads. ENTCS, Elsevier, volume 20, April 1999.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo. On the compact-regular coreflection of a stably compact locale. ENTCS, Elsevier, volume 20, April 1999.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo and T. Streicher Induction and recursion on the partial real line with applications to Real PCF. Theoretical Computer Science, Elsevier, volume 210, number 1, pages 121-157, January 1999.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo. Properly injective spaces and function spaces. Topology and its Applications, Elsevier, volume 89, number 1-2, pp. 75-120, 1998.

    pdf, ps, ps.gz, dvi, dvi.gz.

    T. Erker, M.H. Escardo and K. Keimel. The way-below relation of function spaces over semantic domains. Topology and its Applications, Elsevier, volume 89, number 1-2, pp. 61-74, 1998.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo. Effective and sequential definition by cases on the reals via infinite signed-digit numerals. ENTCS, Elsevier, vol 13, 1998.

    pdf, ps, ps.gz, dvi, dvi.gz.

    D. Pavlovic and M.H. Escardo. Calculus in coinductive form. Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science. Indiana, USA, June 1998.

    Electronically available as Technical Report 97:05, School of Cognitive and Computing Sciences, University of Sussex.

    M.H. Escardo. Injective spaces via the filter monad. Topology Proceedings, volume 22, pp. 97-110, 1997.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo. PCF extended with real numbers: a domain-theoretic approach to higher-order exact real number computation. PhD thesis under the supervision of M.B. Smyth at the Department of Computing of Imperial College, University of London, submitted in November 1996 and defended in February 1997. Published as Technical Report number ECS-LFCS-97-374 of the LFCS, Division of Informatics , University of Edinburgh, November 1997.

    ECS-LFCS-97-374 (follow this link and then find file at the bottom).

    M.H. Escardo and T. Streicher. Induction and recursion on the partial real line via biquotients of bifree algebras. Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science. Warsaw, Poland, June 1997, pages 376-386.

    pdf, ps, ps.gz, dvi, dvi.gz.

    P. Potts and A. E. and M.H. Escardo. Semantics of exact real arithmetic. Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science. Warsaw, Poland, June 1997, pages 248-257.

    ps, ps.gz.

    A. E. and M.H. Escardo. Integration in Real PCF (extended abstract). Proceedings of the 11th Annual IEEE Symposium on Logic In Computer Science, New Brunswick, New Jersey, USA, June 1996, pages 382-393.

    pdf, ps, ps.gz, dvi, dvi.gz.

    M.H. Escardo. Real PCF extended with ∃ is universal. Eds. A.E., A., Jourdan, S., McCusker, G., Proceedings of the 3rd Workshop on Theory and Formal Methods, IC Press, pages 13-24, April 1996. Christ Church, Oxford, 1996.

    pdf, ps, ps.gz, dvi, dvi.gz.

    PCF extended with real numbers. Theoretical Computer Science, Elsevier, volume 162, issue 1, pp. 79-115, August 1996.

    pdf, ps, ps.gz, dvi, dvi.gz.

1. M.H. Escardo. A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom, March 2018, arXiv preprint. Includes Agda code as an ancillary file.

2. M.H. Escardo. Agda in a Hurry. Concise tutorial (written for Haskell programmers) to get started with Agda, 5th October 2017.

3. M.H. Escardo. Dummett disjunction in Martin-Löf Type Theory. 31 March 2016, Unpublished research note.

   html.

4. Chuangjie Xu and M.H. Escardo. Universes in sheaf models. February 2016, Unpublished research note.

   pdf.

5. M.H. Escardo. Using Yoneda rather than Martin-Lof's induction principle J to present the identity type in MLTT. Unpublished note. 7 May 2015.

   html , Agda.

6. T. Coquand and M.H. Escardo. The geometry of constancy. Unpublished note, to be presented at HoTT/UF. May 2015.

   pdf abstract, talk at HoTT/UF in Warsaw 2015, cubicaltt code with full formal proofs.

7. M.H. Escardo. Computing with real numbers represented as infinite sequences of digits in Haskell. CCA'2009 tutorial, August 2009, based on older stuff.

   zip file with Haskell programs and scripts.

   There is also a literate program derived from this used for a talk in Fun in the Afternoon (March 2011).

8. M.H. Escardo. Kreisel's counter-example to full abstraction of the set-theoretical model of Goedel's system T. 23rd July 2007.

   pdf.

9. M.H. Escardo. Notes on compactness. 8th April 2005, updated 12th Sept 2005. (Expanded version of a previous note called Synthetic compactness revisited.)

   pdf, ps, ps.gz, dvi, dvi.gz.

10. M.H. Escardo. [Synthetic] Topology via higher-order intuitionistic logic, version of 18 March 2004, made available here 07 Oct 2010, presented at MFPS in Pittsburgh in 2004. These are first steps, which I intended to eventually carry out, but I was occupied with many other things. Because Davorin Lesnik has produced a very nice PhD thesis taking this as a starting point, under the advice of Andrej Bauer, I decided to make my unfinished paper publicly available (it may contain mistakes, particularly in the claims left without proofs).

    pdf.

11. M.H. Escardo. Mathematical foundations of functional programming with real numbers. Notes for a course delivered at the Midlands Graduate School in the Foundations of Computer Science, Leicester, Mar 31, Apr 1, 2003.

    pdf.

12. M.H. Escardo. Introduction to Real PCF. Notes for an invited talk at the 3rd Real Numbers and Computers Conference (RNC3), l'Université Pierre et Marrie Curie, Paris, April 1998.

    pdf, ps, ps.gz, dvi, dvi.gz.

13. M.H. Escardo. Introduction to exact numerical computation. Notes for a tutorial course at the International Symposium on Symbolic and Algebraic Computation (ISSAC), St Andrews, 6-9 August 2000.

    pdf, html, ps, ps.gz, dvi, dvi.gz.

14. M.H. Escardo. The patch frame of the Lawson dual of a stably continuous frame. 23 May 2000.

    pdf, ps, ps.gz, dvi, dvi.gz.

15. M.H. Escardo. Spatiality of the patch frame. 18 May 2000.

    pdf, ps, ps.gz, dvi, dvi.gz.

16. M.H. Escardo. The interpolation property of the way-below relation of a continuous poset. 18 Mar 2000. It has been included in the paper Function-space compactifications of function spaces and in the book "Continuous lattices and domains" (CUP 2003) by GHKLMS via Keimel.

    pdf, ps, ps.gz, dvi, dvi.gz.

17. M.H. Escardo. A metric model of PCF. Presented at the Workshop on Realizability Semantics and Applications, June 30-July 1, 1999 (associated to the Federated Logic Conference, held in Trento, June 29-July 12, 1999).

    pdf, ps, ps.gz, dvi, dvi.gz.

Some mathematical and computational developments in Haskell and Agda

1. Seemingly impossible functional programs (in Haskell).


2. Real number computation in Haskell with real numbers represented as infinite sequences of digits.


3. A Haskell monad for infinite search in finite time (in Haskell).


4. Running a classical proof with choice in Agda (a blog post summarizes this).


5. What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common.


6. Various new theorems in constructive mathematics developed in a constructive univalent type theory using Agda.

   This includes, among other things:

   • The conatural numbers (or extended natural numbers, or the one-point compactification of the discrete space of natural numbers) are exhaustibly searchable, despite the fact that they form an infinite space (also known as the generic convergent sequence), and so are many more infinite types.
   • The universe of all types is indiscrete (see also a brief blog post with links to an older agda version).
   • Rice's Theorem for the universe as a corollary.
   • The universe is injective, which is used as a lemma in the indiscreteness theorem.

   This is also briefly reported as a blog post with links to an older version.

7. Using Yoneda rather than J to present Martin-Löf's identity type.


8. Continuity of Godel's system T functionals via effectful forcing.


9. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation.


10. Univalent logic.
    • A small type of propositions a la Voevodsky in Agda. This uses Type:Type in only one module.
    • This uses rewriting instead.
    • This lives with the fact that the type of propositions is large, and also discusses a large propositional truncation a la Voevodsky and its relation to the small one (if it exists).
    • This uses rewriting only to make propositional truncations a la Voevodsky small. Everything else retains its native universe level.



11. Agda discussion about propositional truncation, function extensionality, and turning any factorization via the propositional truncation of the domain of a function into a judgmental one. It includes the fact that the interval is the propositional truncation of the booleans, which gives the germ of the idea for the factorization.
12. Generalizations of Hedberg's Theorem.
13. The empty type has a constant endomap (the identity function). Any type that has a given point has a constant endomap (that maps everything to that point). If every type has a constant endomap, then every type has decidable equality, which implies WLPO and other constructive taboos.
14. Dummett disjunction in Martin-Löf Type Theory.

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders, usually the publishers. All persons and robots copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Last modified: Friday May 17 14:16:5 UTC 2024