# first.items[].content
*2024/02/04. Using Yoneda rather than J to present the identity type.
https://mathstodon.xyz/deck/@MartinEsc ardo/111874700368118421

*2024/02/06. The patch of a spectral locale X has fewer points than X.
https://mathstodon.xyz/deck/@MartinEsc ardo/111886020216629690

* 2024/02/16. On Pataraia's fixed-point theorem.
https://mathstodon.xyz/deck/@MartinEsc ardo/111943474521669669

* 2024/02/28. LLPO in constructive mathematics.
https://mathstodon.xyz/deck/@MartinEsc ardo/112011057976815731

* 2024/03/07. Teaching program/specification/verification and definition/theorem/proof.
https://mathstodon.xyz/deck/@MartinEsc ardo/112056560542575049

*2024/03/14. The subtype of sharp elements of the flat domain of natural numbers.
https://mathstodon.xyz/deck/@MartinEsc ardo/112096634888563693

*2024/03/19. Topological intuition for computational, and more generally constructive, mathematics.
https://mathstodon.xyz/deck/@MartinEsc ardo/112124678815998407

*2024/04/27. What is a topological space, what is the intuition behind the definition, and what is (roughly) the history of all this.
https://mathstodon.xyz/deck/@MartinEsc ardo/112344531871296929

*2024/05/02. Free graphic monoids and the monad of lists without repetitions.
https://mathstodon.xyz/deck/@MartinEsc ardo/112373111671959398

*2024/06/14. A question about thinly inhabited types.
https://mathstodon.xyz/deck/@MartinEsc ardo/112615840084539200

*2024/06/23. Just for fun, Android/Linux hacking.
https://mathstodon.xyz/deck/@MartinEsc ardo/112661718405023763

*2024/07/18. ¬ WLPO as a weak continuity principle.
https://mathstodon.xyz/deck/@MartinEsc ardo/112809256762862829

*2024/08/21. Continuity of functions ℕ∞ → ℕ.
https://mathstodon.xyz/deck/@MartinEsc ardo/113001536506411322

*2024/09/11. When can a function ℕ → ℕ be extended to a function ℕ∞ → ℕ constructively, without assuming continuity axioms?
https://mathstodon.xyz/deck/@MartinEsc ardo/113024154634637479

*2024/09/21. Applying domain theory and topology to come up with seemingly impossible programs.
https://mathstodon.xyz/deck/@MartinEsc ardo/113177615482791270

*2024/09/23. Understanding propositional truncations in HoTT/UF.
https://mathstodon.xyz/deck/@MartinEsc ardo/113188689591632856

*2024/12/13. Negative axioms can be postulated without loss of canonicity.
https://mathstodon.xyz/deck/@MartinEsc ardo/113646659385507211

3/

# first.items[].contentMap.en
*2024/02/04. Using Yoneda rather than J to present the identity type.
https://mathstodon.xyz/deck/@MartinEsc ardo/111874700368118421

*2024/02/06. The patch of a spectral locale X has fewer points than X.
https://mathstodon.xyz/deck/@MartinEsc ardo/111886020216629690

* 2024/02/16. On Pataraia's fixed-point theorem.
https://mathstodon.xyz/deck/@MartinEsc ardo/111943474521669669

* 2024/02/28. LLPO in constructive mathematics.
https://mathstodon.xyz/deck/@MartinEsc ardo/112011057976815731

* 2024/03/07. Teaching program/specification/verification and definition/theorem/proof.
https://mathstodon.xyz/deck/@MartinEsc ardo/112056560542575049

*2024/03/14. The subtype of sharp elements of the flat domain of natural numbers.
https://mathstodon.xyz/deck/@MartinEsc ardo/112096634888563693

*2024/03/19. Topological intuition for computational, and more generally constructive, mathematics.
https://mathstodon.xyz/deck/@MartinEsc ardo/112124678815998407

*2024/04/27. What is a topological space, what is the intuition behind the definition, and what is (roughly) the history of all this.
https://mathstodon.xyz/deck/@MartinEsc ardo/112344531871296929

*2024/05/02. Free graphic monoids and the monad of lists without repetitions.
https://mathstodon.xyz/deck/@MartinEsc ardo/112373111671959398

*2024/06/14. A question about thinly inhabited types.
https://mathstodon.xyz/deck/@MartinEsc ardo/112615840084539200

*2024/06/23. Just for fun, Android/Linux hacking.
https://mathstodon.xyz/deck/@MartinEsc ardo/112661718405023763

*2024/07/18. ¬ WLPO as a weak continuity principle.
https://mathstodon.xyz/deck/@MartinEsc ardo/112809256762862829

*2024/08/21. Continuity of functions ℕ∞ → ℕ.
https://mathstodon.xyz/deck/@MartinEsc ardo/113001536506411322

*2024/09/11. When can a function ℕ → ℕ be extended to a function ℕ∞ → ℕ constructively, without assuming continuity axioms?
https://mathstodon.xyz/deck/@MartinEsc ardo/113024154634637479

*2024/09/21. Applying domain theory and topology to come up with seemingly impossible programs.
https://mathstodon.xyz/deck/@MartinEsc ardo/113177615482791270

*2024/09/23. Understanding propositional truncations in HoTT/UF.
https://mathstodon.xyz/deck/@MartinEsc ardo/113188689591632856

*2024/12/13. Negative axioms can be postulated without loss of canonicity.
https://mathstodon.xyz/deck/@MartinEsc ardo/113646659385507211

3/