Posts by MartinEscardo@mathstodon.xyz
(DIR) Post #AhP5Pm7O9Ree8iRQ2q by MartinEscardo@mathstodon.xyz
2024-04-29T21:39:12Z
0 likes, 0 repeats
I will delete this post tomorrow morning. For the moment, I will keep it in protest for the irritation this causes to me.
(DIR) Post #AhP5PpTpeSOEZBxswa by MartinEscardo@mathstodon.xyz
2024-04-29T22:34:58Z
0 likes, 0 repeats
I said "I will delete this post tomorrow morning. For the moment, I will keep it in protest for the irritation this causes to me."Should I keep my promise?
(DIR) Post #AhP5Ppum2HwNukZOwC by MartinEscardo@mathstodon.xyz
2024-04-29T21:51:05Z
1 likes, 0 repeats
It's fine to say, in your paper, that (in your view) *somebody else's* results are interesting, novel, surprising, important, etc. But such statements about your own work carry no weight.
(DIR) Post #AhP5Ptey6zftWtCprE by MartinEscardo@mathstodon.xyz
2024-04-29T22:06:19Z
0 likes, 0 repeats
"But such statements about your own work carry no weight."I would say more: they make your paper seem suspicious.
(DIR) Post #AhoK0MzJxDHmQANZgW by MartinEscardo@mathstodon.xyz
2024-05-03T22:50:06Z
0 likes, 0 repeats
I want a proof assistant in which category theory is built-in, rather than a library.
(DIR) Post #AhoK0P54Ap4OuZ5Buy by MartinEscardo@mathstodon.xyz
2024-05-04T18:26:08Z
0 likes, 0 repeats
My point, perhaps, is the following.Whenever I formalize something, I want the readers of the formalization to be able to understand what I have done by reading the code.At present, there are lots of places in TypeTopology where there is categorical reasoning, without officially invoking categories.I would like (1) the categorical reasoning to be officially recorded in the development (even though categories are not used officially), and (2) the proof assistant to support categorical reasoning in its interactive mode, as in the case of Agda.
(DIR) Post #AhoK0PJFK6PdcXiW1I by MartinEscardo@mathstodon.xyz
2024-05-04T14:19:42Z
0 likes, 0 repeats
I think my point is that it has been advocated in the past that category theory can be regarded as a foundation, at least for those of us who tend to think categorically. It would be nice to have a proof assistant based on category theory.
(DIR) Post #AhqqjMiVOXSXSbvv3Q by MartinEscardo@mathstodon.xyz
2024-05-04T18:43:37Z
0 likes, 0 repeats
What is categorical reasoning?In categorical reasoning, you define mathematical notions by universal properties, and you prove and construct things using them.This may seem very abstract, but it is very concrete in practice.Proving things using universal properties is so much easier in practice than proving them concretely and directly.(And it avoids a lot of repetition.)
(DIR) Post #AhxYbmxdUvuVTBy2fQ by MartinEscardo@mathstodon.xyz
2024-05-05T19:54:26Z
0 likes, 0 repeats
@zanzi @mc This is fine with me, if you define the devil to be (the rather kind) designers and developers of proof assistants.
(DIR) Post #AhzJ56nvacQEScIzTs by MartinEscardo@mathstodon.xyz
2024-05-05T18:27:35Z
0 likes, 0 repeats
@ToucanIan I want to be able to say to my proof assistant something like this."Now notice that the gadgets I am considering form a category, and that I have proved that there is a freely generated gadget over any set of generators (maybe with relations). Therefore I get a monad."At the moment, you can do that, with or without using category theory explicitly in a proof assistant, but in both cases there is a lot of required boiler plate to do that.Moreover, whether you do this with or without a library for categories, you have to repeat all this when you consider new mathematical gadgets.
(DIR) Post #AhzJ58asw5B40kDbQe by MartinEscardo@mathstodon.xyz
2024-05-05T20:00:48Z
0 likes, 0 repeats
@codyroux @ToucanIan We have a map η : X → Free-Foo X such that every function f : X → A from X to a Foo A extends uniquely to a Foo-map f' : Free-Foo X → A along η.
(DIR) Post #AnpMIqLFov25BCVFwG by MartinEscardo@mathstodon.xyz
2024-10-26T20:09:59Z
0 likes, 1 repeats
Time is the most scarce resource in my field. And yours too, probably.
(DIR) Post #AunCb9agps7UuubEUi by MartinEscardo@mathstodon.xyz
2025-06-04T16:34:42Z
1 likes, 0 repeats
Trivia. Today when I got back home early in the afternoon and continued to work from home, I noticed that my desktop computer screen hadn't locked automatically.I always turn the keyboard around after I finish working, to prevent it from getting dusty.This time a key (for some inexplicable reason, "-") got stuck, and so the character got being typed 509282 times in my emacs file which was open. 🙂
(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/
(DIR) Post #Ayi7dZZoqKgCGs62Jk by MartinEscardo@mathstodon.xyz
2025-09-29T21:18:54Z
0 likes, 0 repeats
@internetarchive There is also this The Guardian article, written by himself, and published a few days ago:"Why I gave the world wide web away for free": https://www.theguardian.com/technology/2025/sep/28/why-i-gave-the-world-wide-web-away-for-free
(DIR) Post #AzHJUsqnoSthQNGEK0 by MartinEscardo@mathstodon.xyz
2025-10-16T20:45:23Z
0 likes, 0 repeats
I give up. People seem to be invested in priorities rather than ideas and progress.This derails the mathematical discussions.It is so upsetting.
(DIR) Post #B1sl34fsm3AVVTkdPM by MartinEscardo@mathstodon.xyz
2025-12-29T15:43:44Z
1 likes, 0 repeats
@jesper writes "I just installed @nextcloud "Nice. A couple of months ago my 15-year old son installed nextcloud for me in our Linux server at home.This was mostly for being able to use Saber [1] to write notes by hand on both Android and iPad tablets, and having the notes visible in all computers, at home and at university.It works like a charm. I can write notes at university in the Android tablet I keep there, and then continue writing at home in my iPad. And I can read the notes from my laptop.It just works, thanks to both nextcloud and Saber. Thanks both!@nextcloud [1] https://saber.adil.hanney.org/And both are free, and also rather professional. More professional than e.g. what Apple provides on an iPad or a Mac.