Post AwTIOrGdjiPtfhaAPQ by MartinEscardo@mathstodon.xyz
(DIR) More posts by MartinEscardo@mathstodon.xyz
(DIR) Post #AwTIOQmcCix1X3Kp04 by MartinEscardo@mathstodon.xyz
2023-08-14T21:44:56Z
0 likes, 1 repeats
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/1106850749211032371/
(DIR) Post #AwTIOa2tlYK8GA1S88 by MartinEscardo@mathstodon.xyz
2023-08-14T21:45:11Z
0 likes, 0 repeats
* 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/@MartinEscardo/111178225435612295* 2023/10/13. The "philosophy" of TypeTopology.https://mathstodon.xyz/deck/@MartinEscardo/111229203225759689* 2023/10/24. Automorphisms of the subobject classifier and excluded middle.https://mathstodon.xyz/deck/@MartinEscardo/111291658836418672* 2023/11/04. Embeddings versus left-cancellable maps in HoTT/UFhttps://mathstodon.xyz/deck/@MartinEscardo/111353724713972893* 2023/11/08. The meaning of "type" in various type theories, including HoTT/UF.https://mathstodon.xyz/deck/@MartinEscardo/111376929816890580* 2023/11/09. The notion of equivalence in HoTT/UF.The notion of equivalence in HoTT/UF.https://mathstodon.xyz/deck/@MartinEscardo/111382482977842039* 2023/11/13. Constructive taboos.https://mathstodon.xyz/deck/@MartinEscardo/111405121300053710*2023/12/07. Exhaustibly searchable sets in higher-type computation.https://mathstodon.xyz/deck/@MartinEscardo/111540938183855671*2024/01/03. The delay monad, searchable types and totally separated types.https://mathstodon.xyz/deck/@MartinEscardo/111666070245799946*2024/01/21. Computability at higher types.https://mathstodon.xyz/deck/@MartinEscardo/111795547575914525*2024/01/29. How I view the formalization of mathematics.https://mathstodon.xyz/deck/@MartinEscardo/111835176816331626*2024/02/02. A mathematical coincidence?https://mathstodon.xyz/deck/@MartinEscardo/1118637961413203842/
(DIR) Post #AwTIOjHPQyHKtlsfUu by MartinEscardo@mathstodon.xyz
2024-02-04T18:58:20Z
0 likes, 0 repeats
*2024/02/04. Using Yoneda rather than J to present the identity type.https://mathstodon.xyz/deck/@MartinEscardo/111874700368118421*2024/02/06. The patch of a spectral locale X has fewer points than X.https://mathstodon.xyz/deck/@MartinEscardo/111886020216629690* 2024/02/16. On Pataraia's fixed-point theorem.https://mathstodon.xyz/deck/@MartinEscardo/111943474521669669* 2024/02/28. LLPO in constructive mathematics.https://mathstodon.xyz/deck/@MartinEscardo/112011057976815731* 2024/03/07. Teaching program/specification/verification and definition/theorem/proof.https://mathstodon.xyz/deck/@MartinEscardo/112056560542575049*2024/03/14. The subtype of sharp elements of the flat domain of natural numbers.https://mathstodon.xyz/deck/@MartinEscardo/112096634888563693*2024/03/19. Topological intuition for computational, and more generally constructive, mathematics.https://mathstodon.xyz/deck/@MartinEscardo/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/@MartinEscardo/112344531871296929*2024/05/02. Free graphic monoids and the monad of lists without repetitions.https://mathstodon.xyz/deck/@MartinEscardo/112373111671959398*2024/06/14. A question about thinly inhabited types.https://mathstodon.xyz/deck/@MartinEscardo/112615840084539200*2024/06/23. Just for fun, Android/Linux hacking. https://mathstodon.xyz/deck/@MartinEscardo/112661718405023763*2024/07/18. ¬ WLPO as a weak continuity principle. https://mathstodon.xyz/deck/@MartinEscardo/112809256762862829*2024/08/21. Continuity of functions ℕ∞ → ℕ.https://mathstodon.xyz/deck/@MartinEscardo/113001536506411322*2024/09/11. When can a function ℕ → ℕ be extended to a function ℕ∞ → ℕ constructively, without assuming continuity axioms? https://mathstodon.xyz/deck/@MartinEscardo/113024154634637479*2024/09/21. Applying domain theory and topology to come up with seemingly impossible programs.https://mathstodon.xyz/deck/@MartinEscardo/113177615482791270*2024/09/23. Understanding propositional truncations in HoTT/UF. https://mathstodon.xyz/deck/@MartinEscardo/113188689591632856*2024/12/13. Negative axioms can be postulated without loss of canonicity.https://mathstodon.xyz/deck/@MartinEscardo/1136466593855072113/
(DIR) Post #AwTIOrGdjiPtfhaAPQ by MartinEscardo@mathstodon.xyz
2025-04-12T14:05:59Z
0 likes, 0 repeats
* 2025/04/12. A universal characterization of the closed Euclidean interval.https://mathstodon.xyz/deck/@MartinEscardo/114325340007735876*2025/05/14. Computing all optimal plays of a sequential game.https://mathstodon.xyz/deck/@MartinEscardo/114506199078361520*2025/05/20. Internal effectful forcing.https://mathstodon.xyz/deck/@MartinEscardo/114541967632998444*2025/05/21. A positive way of saying that a type is different from the unit type, in connection with the lifting monad.https://mathstodon.xyz/deck/@MartinEscardo/114547664640960020*2025/06/05. Taking "algebraically" seriously in the definition of algebraically injective type.https://mathstodon.xyz/deck/@MartinEscardo/114633174055141602*2025/06/20. The fundamental lemma of transport along equivalences.https://mathstodon.xyz/deck/@MartinEscardo/114717657709706036*2025/06/22. Question about object classifiers and univalence.https://mathstodon.xyz/deck/@MartinEscardo/114722727504214914*2025/06/26. Dependent equality in dependent type theory.https://mathstodon.xyz/deck/@MartinEscardo/114751426538568913*2025/07/01. A proof that the type of natural numbers is a set in MLTT without universes by Evan Cavallo. https://mathstodon.xyz/deck/@ncf@types.pl/114779291804001070The above is a thread started by @ncf with that question, and eventually answered by @ecavallo . I made wrong statements in that thread, but I am keeping them without correction (people corrected me there).*2025/07/05. The definition of equivalence in HoTT/UF.https://mathstodon.xyz/deck/@MartinEscardo/1148018087733169844/