Martin Escardo@MartinEscardo@mathstodon.xyz
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/