Martín Escardó's "metablog"

Some of my blog posts are at Andrej Bauer's Mathematics and Computation, or at homotopytypetheory, but more recently they are at Mathstodon.
  1. 2007/09/28. Seemingly impossible functional programs.
  2. 2008/11/21. A Haskell monad for infinite search in finite time.
  3. 2011/05/10. Running a classical proof with choice in Agda.
  4. 2012/03/30. The topology on the set of all types.
  5. 2014/05/08. Seemingly impossible proofs.
  6. 2018/03/07. A self-contained, brief and complete formulation of Voevodsky's univalence axiom
  7. 2019/03/20. Introduction to univalent foundations of mathematics with Agda.
  8. 2021/01/23. Can the type of truth values be given the structure of a group?
  9. 2020/01/26. The Cantor-Schroder-Bernstein Theorem for ∞-groupoids.
  10. 2021/05/18. Computing an integer using a Grothendieck topos.
  11. 2021/02/22. Burali-Forti in HoTT/UF.
  12. 2022/10/31. Proofs by contradiction.
  13. 2022/11/12. Synthetic topology of data types and classical spaces.
  14. 2022/11/14. Notions of space.
  15. 2022/11/16. Trichotomy of ordinals.
  16. 2022/11/22. Birthday present by Tom de Jong.
  17. 2022/11/23. Concrete example illustrating that constructive mathematics is more general than classical mathematics.
  18. 2022/12/01. Combinatorial game theory.
  19. 2022/12/08. Universe polymorphic type systems.
  20. 2022/12/08. Why cubical type theory, and why cubical Agda?
  21. 2022/12/20. The axiom of choice in HoTT/UF.
  22. 2022/12/22. A common generalization of the univalence axiom and the K axiom.
  23. 2023/02/03. Defining large numbers without using induction.
  24. 2023/02/10. Several kinds of categories in HoTT/UF.
  25. 2023/03/03. Universes in type theory as mathematical objects interesting in their own right.
  26. 2023/03/22. Playing rationally against irrational players.
  27. 2023/04/11. What are universes for in HoTT/UF?
  28. 2023/06/02. Patch locale in HoTT/UF.
  29. 2023/06/07. Github project TypeTopology.
  30. 2023/06/15. Constructive notions of disjunction.
  31. 2023/07/09. Trichotomy of the reals constructively.
  32. 2023/07/18. Motivation for ∞-categories.
  33. 2023/07/21. Iterative multisets, sets and ordinals.
  34. 2023/08/18. Injective types in constructive HoTT/UF.
  35. 2023/09/01. Three exercises for HoTT/UF students.
  36. 2023/09/03. Two exercises in constructive mathematics (which evolved to more).
  37. 2023/09/05. Demystifying propositional truncations in HoTT/UF.
  38. 2023/09/23. An amusing proof in constructive type theory.
  39. 2023/10/04. Formalization for people, not (only) computers.
  40. 2023/10/13. The "philosophy" of TypeTopology.
  41. 2023/10/24. Automorphisms of the subobject classifier and excluded middle.
  42. 2023/11/04. Embeddings versus left-cancellable maps in HoTT/UF.
  43. 2023/11/08. The meaning of "type" in various type theories, including HoTT/UF.
  44. 2023/11/09. The notion of equivalence in HoTT/UF.
  45. 2023/11/13. Constructive taboos.
  46. 2023/12/07. Exhaustibly searchable sets in higher-type computation.
  47. 2024/01/03. The delay monad.
  48. 2024/01/21. Computability at higher types.
  49. 2024/01/29. How I view the formalization of mathematics.
  50. 2024/02/02. A mathematical coincidence?
  51. 2024/02/04. Using Yoneda rather than J to present the identity type
  52. 2024/02/06. The patch of a spectral locale X has fewer points than X.
  53. 2024/02/16. On Pataraia's fixed-point theorem.
  54. 2024/02/28. LLPO in constructive mathematics.
  55. 2024/03/07. Teaching program/specification/verification and definition/theorem/proof.
  56. 2024/03/14. The subtype of sharp elements of the flat domain of natural numbers.
  57. 2024/03/19. Topological intuition for computational, and more generally constructive, mathematics.
  58. 2024/04/27. What is a topological space, what is the intuition behind the definition, and what is (roughly) the history of all this.
  59. 2024/05/02. Free graphic monoids and the monad of lists without repetitions.
  60. 2024/06/14. A question about thinly inhabited types.
  61. 2024/06/23. Just for fun, Android/Linux hacking.
  62. 2024/07/18. ¬ WLPO as a weak continuity principle.
  63. 2024/08/21. Continuity of functions ℕ∞ → ℕ.
  64. 2024/09/11. When can a function ℕ → ℕ be extended to a function ℕ∞ → ℕ constructively, without assuming continuity axioms?
  65. 2024/09/21. Applying domain theory and topology to come up with seemingly impossible programs.
  66. 2024/09/23. Understanding propositional truncations in HoTT/UF.
  67. 2024/12/13. Negative axioms can be postulated without loss of canonicity.
Martin Escardo
m.escardo@bham.ac.uk

Last modified: Friday December 13 17:37:38 UTC 2024