# orderedItems[].content
Academics in Computer Science:

# orderedItems[].contentMap.en
Academics in Computer Science:

# orderedItems[].oneOf[].name
This doesn't apply to me. Show me the results.

# orderedItems[].content
I was considering creating my own blog, but I am instead happy to post here or occasionally at @andrejbauer 's blog Mathematics and Computation.

For easy access, though, I've created a web page that indexes my posts, which, with luck, will itself be indexed by search engines:

https://www. cs.bham.ac.uk/~mhe/blog.html

# orderedItems[].contentMap.en
I was considering creating my own blog, but I am instead happy to post here or occasionally at @andrejbauer 's blog Mathematics and Computation.

For easy access, though, I've created a web page that indexes my posts, which, with luck, will itself be indexed by search engines:

https://www. cs.bham.ac.uk/~mhe/blog.html

# orderedItems[].content
Index of selected threads on #hott #constructive #math

* 2022/10/31. Proofs by contradiction.
https://mathstodon.xyz/@MartinEscardo/109264034964990196

* 2022/11/12. Synthetic topology of data types and classical spaces.
https://mathstodon.xyz/@MartinEscardo/109332986014534390

* 2022/11/14. Notions of space.
https://mathstodon.xyz/@MartinEscardo/109343930842850773

* 2022/11/16. Trichotomy of ordinals.
https://mathstodon.xyz/@MartinEscardo/109355604029879269

* 2022/11/22. Birthday present by Tom de Jong.
https://mathstodon.xyz/@MartinEscardo/109388875794058555

* 2022/11/23. Concrete example illustrating that constructive mathematics is more general than classical mathematics.
https://mathstodon.xyz/@MartinEscardo/109395006766077334

* 2022/12/01. Combinatorial game theory.
https://mathstodon.xyz/@MartinEscardo/109440314312765877

* 2022/12/08. Universe polymorphic type systems.
https://mathstodon.xyz/@MartinEscardo/109480057029596732

* 2022/12/08. Why cubical type theory, and why cubical Agda?
https://mathstodon.xyz/@MartinEscardo/109480455436886869

* 2022/12/20. The axiom of choice in HoTT/UF.
https://mathstodon.xyz/@MartinEscardo/109546988519874380

* 2022/12/22. A common generalization of the univalence axiom and the K axiom.
https://mathstodon.xyz/@MartinEscardo/109558670025171863

* 2023/02/03. Defining large numbers without using induction.
https://mathstodon.xyz/@MartinEscardo/109802885041067972

* 2023/02/10. Several kinds of categories in HoTT/UF.
https://mathstodon.xyz/@MartinEscardo/109842791175514936

* 2023/03/03. Universes in type theory as mathematical objects interesting in their own right.
https://mathstodon.xyz/@MartinEscardo/109961534132268566

* 2023/03/22. Playing rationally against irrational players.
https://mathstodon.xyz/@MartinEscardo/110068977445045121

* 2023/04/11. What are universes for in HoTT/UF?
https://mathstodon.xyz/@MartinEscardo/110181596099423100

* 2023/06/02. Ayberk's predicative version of the patch locale of a Stone locale.
https://mathstodon.xyz/@MartinEscardo/110476555405397697

* 2023/06/07. Github project TypeTopology.
https://mathstodon.xyz/@MartinEscardo/110504563233350460

* 2023/06/15. Constructive notions of disjunction.
https://mathstodon.xyz/@MartinEscardo/110549967500023998

* 2023/07/09. Trichotomy of the reals constructively.
https://mathstodon.xyz/@MartinEscardo/110685074921103237

1/

# orderedItems[].contentMap.en
Index of selected threads on #hott #constructive #math

* 2022/10/31. Proofs by contradiction.
https://mathstodon.xyz/@MartinEscardo/109264034964990196

* 2022/11/12. Synthetic topology of data types and classical spaces.
https://mathstodon.xyz/@MartinEscardo/109332986014534390

* 2022/11/14. Notions of space.
https://mathstodon.xyz/@MartinEscardo/109343930842850773

* 2022/11/16. Trichotomy of ordinals.
https://mathstodon.xyz/@MartinEscardo/109355604029879269

* 2022/11/22. Birthday present by Tom de Jong.
https://mathstodon.xyz/@MartinEscardo/109388875794058555

* 2022/11/23. Concrete example illustrating that constructive mathematics is more general than classical mathematics.
https://mathstodon.xyz/@MartinEscardo/109395006766077334

* 2022/12/01. Combinatorial game theory.
https://mathstodon.xyz/@MartinEscardo/109440314312765877

* 2022/12/08. Universe polymorphic type systems.
https://mathstodon.xyz/@MartinEscardo/109480057029596732

* 2022/12/08. Why cubical type theory, and why cubical Agda?
https://mathstodon.xyz/@MartinEscardo/109480455436886869

* 2022/12/20. The axiom of choice in HoTT/UF.
https://mathstodon.xyz/@MartinEscardo/109546988519874380

* 2022/12/22. A common generalization of the univalence axiom and the K axiom.
https://mathstodon.xyz/@MartinEscardo/109558670025171863

* 2023/02/03. Defining large numbers without using induction.
https://mathstodon.xyz/@MartinEscardo/109802885041067972

* 2023/02/10. Several kinds of categories in HoTT/UF.
https://mathstodon.xyz/@MartinEscardo/109842791175514936

* 2023/03/03. Universes in type theory as mathematical objects interesting in their own right.
https://mathstodon.xyz/@MartinEscardo/109961534132268566

* 2023/03/22. Playing rationally against irrational players.
https://mathstodon.xyz/@MartinEscardo/110068977445045121

* 2023/04/11. What are universes for in HoTT/UF?
https://mathstodon.xyz/@MartinEscardo/110181596099423100

* 2023/06/02. Ayberk's predicative version of the patch locale of a Stone locale.
https://mathstodon.xyz/@MartinEscardo/110476555405397697

* 2023/06/07. Github project TypeTopology.
https://mathstodon.xyz/@MartinEscardo/110504563233350460

* 2023/06/15. Constructive notions of disjunction.
https://mathstodon.xyz/@MartinEscardo/110549967500023998

* 2023/07/09. Trichotomy of the reals constructively.
https://mathstodon.xyz/@MartinEscardo/110685074921103237

1/