# first.items[].content
* 2023/07/18. Motivation for ∞-categories.
https://mathstodon.xyz/@MartinEscardo/110737059204379256

* 2023/07/21. Iterative multisets, sets and ordinals.
https://mathstodon.xyz/@MartinEscardo/110753930251021051

* 2023/08/18. Injective types in constructive HoTT/UF. https://mathstodon.xyz/@MartinEscardo/110912588238494225

* 2023/09/01. Three exercises for HoTT/UF students. https://mathstodon.xyz/@MartinEscardo/110991799307299727

* 2023/09/03. Two exercises in constructive mathematics (which evolved to more). https://mathstodon.xyz/@MartinEscardo/111002413035009813

* 2023/09/05. Demystifying propositional truncations in HoTT/UF. https://mathstodon.xyz/@MartinEscardo/111014413939196037

* 2023/09/23. An amusing proof in constructive type theory. https://mathstodon.xyz/@MartinEscardo/111115846596114122

* 2023/10/04. Formalizations written for people, not (only) computers.
https://mathstodon.xyz/deck/@MartinEsc ardo/111178225435612295

* 2023/10/13. The "philosophy" of TypeTopology.
https://mathstodon.xyz/deck/@MartinEsc ardo/111229203225759689

* 2023/10/24. Automorphisms of the subobject classifier and excluded middle.
https://mathstodon.xyz/deck/@MartinEsc ardo/111291658836418672

* 2023/11/04. Embeddings versus left-cancellable maps in HoTT/UF
https://mathstodon.xyz/deck/@MartinEsc ardo/111353724713972893

* 2023/11/08. The meaning of "type" in various type theories, including HoTT/UF.
https://mathstodon.xyz/deck/@MartinEsc ardo/111376929816890580

* 2023/11/09. The notion of equivalence in HoTT/UF.
The notion of equivalence in HoTT/UF.
https://mathstodon.xyz/deck/@MartinEsc ardo/111382482977842039

* 2023/11/13. Constructive taboos.
https://mathstodon.xyz/deck/@MartinEsc ardo/111405121300053710

*2023/12/07. Exhaustibly searchable sets in higher-type computation.
https://mathstodon.xyz/deck/@MartinEsc ardo/111540938183855671

*2024/01/03. The delay monad, searchable types and totally separated types.
https://mathstodon.xyz/deck/@MartinEsc ardo/111666070245799946

*2024/01/21. Computability at higher types.
https://mathstodon.xyz/deck/@MartinEsc ardo/111795547575914525

*2024/01/29. How I view the formalization of mathematics.
https://mathstodon.xyz/deck/@MartinEsc ardo/111835176816331626

*2024/02/02. A mathematical coincidence?
https://mathstodon.xyz/deck/@MartinEsc ardo/111863796141320384

2/

# first.items[].contentMap.en
* 2023/07/18. Motivation for ∞-categories.
https://mathstodon.xyz/@MartinEscardo/110737059204379256

* 2023/07/21. Iterative multisets, sets and ordinals.
https://mathstodon.xyz/@MartinEscardo/110753930251021051

* 2023/08/18. Injective types in constructive HoTT/UF. https://mathstodon.xyz/@MartinEscardo/110912588238494225

* 2023/09/01. Three exercises for HoTT/UF students. https://mathstodon.xyz/@MartinEscardo/110991799307299727

* 2023/09/03. Two exercises in constructive mathematics (which evolved to more). https://mathstodon.xyz/@MartinEscardo/111002413035009813

* 2023/09/05. Demystifying propositional truncations in HoTT/UF. https://mathstodon.xyz/@MartinEscardo/111014413939196037

* 2023/09/23. An amusing proof in constructive type theory. https://mathstodon.xyz/@MartinEscardo/111115846596114122

* 2023/10/04. Formalizations written for people, not (only) computers.
https://mathstodon.xyz/deck/@MartinEsc ardo/111178225435612295

* 2023/10/13. The "philosophy" of TypeTopology.
https://mathstodon.xyz/deck/@MartinEsc ardo/111229203225759689

* 2023/10/24. Automorphisms of the subobject classifier and excluded middle.
https://mathstodon.xyz/deck/@MartinEsc ardo/111291658836418672

* 2023/11/04. Embeddings versus left-cancellable maps in HoTT/UF
https://mathstodon.xyz/deck/@MartinEsc ardo/111353724713972893

* 2023/11/08. The meaning of "type" in various type theories, including HoTT/UF.
https://mathstodon.xyz/deck/@MartinEsc ardo/111376929816890580

* 2023/11/09. The notion of equivalence in HoTT/UF.
The notion of equivalence in HoTT/UF.
https://mathstodon.xyz/deck/@MartinEsc ardo/111382482977842039

* 2023/11/13. Constructive taboos.
https://mathstodon.xyz/deck/@MartinEsc ardo/111405121300053710

*2023/12/07. Exhaustibly searchable sets in higher-type computation.
https://mathstodon.xyz/deck/@MartinEsc ardo/111540938183855671

*2024/01/03. The delay monad, searchable types and totally separated types.
https://mathstodon.xyz/deck/@MartinEsc ardo/111666070245799946

*2024/01/21. Computability at higher types.
https://mathstodon.xyz/deck/@MartinEsc ardo/111795547575914525

*2024/01/29. How I view the formalization of mathematics.
https://mathstodon.xyz/deck/@MartinEsc ardo/111835176816331626

*2024/02/02. A mathematical coincidence?
https://mathstodon.xyz/deck/@MartinEsc ardo/111863796141320384

2/