ToucanIan

???
https://media.mathstodon.xyz/media_attachments/files/115/885/815/903/352/913/original/206aa3d8222df702.png
https://media.mathstodon.xyz/media_attachments/files/115/885/823/365/183/713/original/f067ab6171f997cf.png

2026-01-07 16:53:48 GMT

- reply

@nprofile…xuzd yes besides being heavy handed I just hate the way it dates the text. This is probably(?) my only complaint about dune messiah.

2025-12-30 17:17:20 GMT

This is very nice http://www.paultaylor.eu/ordinals/oldnew.pdf

2025-12-17 21:52:37 GMT

Thoroughly enjoying the talks so far at @nprofile…w8t5 60th birthday celebration! Happy (late) birthday Martin!

2025-12-05 23:06:53 GMT

The realization that your talk sucks

2025-12-04 01:30:12 GMT

What apps do people use for handwritten slides?

2025-11-19 00:40:10 GMT

- reply

@nprofile…w8t5 the first paper is really nice! Can’t wait to check out the rest.

2025-11-18 09:38:02 GMT

Are there any critical results of computability thoery that don’t hold constructively? I’ve been privately keeping track throughout the semester. So far “proofs by contradiction” where just proofs of negation and uses of LEM happened when the propositions where decidable. But I’ve just seen a proof of rices theorem which relies on the intuitionistically invalid version of constrapositive.

2025-11-17 20:00:00 GMT

- reply

@nprofile…rrqe can you link some examples

2025-11-15 12:08:19 GMT

- reply

@nprofile…rrqe wouldn’t you just need is-prop(P) to identify two witnesses of P?

2025-11-14 04:50:12 GMT

It must actually be really psychologically troubling to have your ego so deeply attached to one of your ideas.

2025-11-10 20:29:08 GMT

- reply

@nprofile…rrqe looking forward to reading it

2025-11-05 16:59:09 GMT

- reply

@nprofile…ral2 also kills me. But one thing I remind myself is negation is primitive classically. So along with not being aware of many of the subtleties of logic they don’t care about.. many people don’t even know that not A is logically equivalent to A -> false.

2025-11-01 22:25:25 GMT

- reply

@nprofile…w8t5 I’m curious if your insinuating that there are other ways of avoiding transport hell? Certainly displayed reflexive graphs is one of the ways!
@nprofile…rrqe

2025-11-01 20:02:34 GMT

- reply

@nprofile…rrqe I guess it only make sense for something to be unspecified when there is potentially more than one thing…
@nprofile…w8t5

2025-11-01 19:51:43 GMT

- reply

@nprofile…rrqe choice?
@nprofile…w8t5

2025-11-01 19:49:45 GMT

- reply

@nprofile…rrqe as Martin said when you truncate it it’s equivalent to itself so that doesn’t really do anything.
@nprofile…w8t5

2025-11-01 19:40:37 GMT

- reply

@nprofile…w8t5 yes it is a proposition, but unlike mere existence defined in terms of prop truncation you actually have the element in hand (even if you try to define it more naively in terms of truncations). At first, this seemed strange to me. Then it didn’t. And I’ve continued to go back and forth.

2025-11-01 18:58:48 GMT

- reply

@nprofile…w8t5 I’ve been thinking about unique existence a bit recently. I find it strange that it cannot be made anonymous (or unspecified). Does this make obvious sense to you? If so could you give me some insight?

2025-11-01 17:03:05 GMT

- reply

@nprofile…rrqe should f and /eta be the same function? If not what is /eta?

2025-10-30 16:57:48 GMT

- reply

@nprofile…rrqe the generalized algebraic theory write up is pretty nice, tbf!

2025-10-20 17:20:55 GMT

- reply

@nprofile…w8t5 too big to fail with a twist

2025-10-16 21:18:35 GMT

- reply

@nprofile…rrqe I remember when Egbert did it there constantly someone in the chat asking about there pre-calculus homework.

2025-10-16 16:13:58 GMT

- reply

@nprofile…rrqe I’m interested in taking this class

2025-10-16 12:33:58 GMT

The nLab says prop resizing can’t hold in a theory with canonicity. But that seems not right. I am vaguely aware of a weird thing you could do to break normalization.

2025-10-06 12:01:18 GMT

- reply

@nprofile…6kk0 as someone who is very interested in “matters of size” but simultaneously becoming a bit disillusioned with making my work universe polymorphic by hand, this is very interesting.

2025-10-05 14:07:35 GMT

The google AI incorrectly insists that Arden’s rule only applies to regular languages. Most of the training data available applies Arden’s rule to regular languages but the result holds for general languages (afact). Has anyone else noticed similar situations? Where use cases of theorems are typically so specific that AI wrongly states the hypothesis of the theorem.

2025-10-04 18:21:22 GMT

- reply

@nprofile…hszg I skipped it too

2025-09-06 23:28:53 GMT

Classical mathematicians should be called non-constructive mathematicians, the people they are scared of should be called non-classical mathematicians (who pretty much don’t exist?). Everyone else is just a mathematician. Leave us alone.

2025-09-04 12:28:23 GMT

- reply

@nprofile…6kk0
Hmm I understand why you are motivated by checking program correctness. And I see that many of the same criticism befall “checking correctness of math”. But ‘being a trillion miles away’ seems a bit shocking to me. You certainly have experienced less anxiety about subtle arguments that you have put through a proof assistant, no?

2025-09-04 12:22:30 GMT

- reply

@nprofile…6kk0 weird book. Some arguement for the pacing being intentional but it was my least favorite so far

2025-08-20 03:45:35 GMT

How are people so good at finding counterexamples…? Gotta be one of my biggest blind spots.

2025-08-19 18:23:07 GMT

- reply

@nprofile…v2av is there no difference between assuming a natural numbers object and more inductive objects?

2025-08-19 03:02:00 GMT

- reply

@nprofile…hszg there does seem to be a glaring terminological issue, maybe that is affecting the searches.

2025-08-18 20:53:21 GMT

- reply

@nprofile…hszg how likely is it that no one has done any interesting research in this area

2025-08-18 20:51:12 GMT

- reply

@nprofile…hszg I have only found “Outline of General Topology” by Engelking. You seem to be familiar with the main results stated there, but I noticed no explicit mention of compactness (it was probably implicit somewhere).

2025-08-18 20:28:54 GMT

- reply

@nprofile…hszg sorry :)

2025-08-18 20:28:34 GMT

- reply

@nprofile…hszg yeah I can’t find any references either.

2025-08-18 20:24:00 GMT

- reply

@nprofile…hszg here are some similar pages that have implications from totally separated:
https://proofwiki.org/wiki/Category:Totally_Separated_Spaces

2025-08-18 20:04:24 GMT

- reply

@nprofile…hszg underrepresented concept I guess. Happens to me a lot when I look up more niche topological things.

2025-08-18 19:48:12 GMT

- reply

@nprofile…hszg
https://media.mathstodon.xyz/media_attachments/files/115/051/494/556/696/805/original/6929e7c7ed98ded9.png

2025-07-31 21:15:27 GMT

- reply

@nprofile…6kk0 good stuff

2025-07-24 10:47:48 GMT

- reply

@nprofile…6kk0 god emperor is great (a bit problematic)

2025-07-11 17:08:10 GMT

- reply

@nprofile…6kk0 btw I would agree. I wish I learned about structural induction in my discrete maths course.

2025-07-11 16:37:46 GMT

- reply

@nprofile…6kk0 makes perfect sense! My university had other motivation I think. Discrete maths always triggers graph theory and combinatorics to me.

2025-07-11 16:07:31 GMT

- reply

@nprofile…6kk0 upon browsing your teaching page I find that you include a lot of thing within the realm of discrete mathematics I would expect. Can you enlighten me with a broad definition?

2025-07-05 20:00:48 GMT

- reply

@nprofile…6kk0 @nprofile…hszg making a distinction between vertical and horizontal lines helped my partner finally see the circles.

2025-07-05 19:52:24 GMT

- reply

@nprofile…hszg the circles are composed of two halves of neighboring rectangles. I can see both

2025-07-04 22:15:55 GMT

- reply

@nprofile…6kk0 I’ll check it out

2025-07-04 20:22:26 GMT

At some point mastadon should mimic (maybe improve) the quoting feature of twitter. Namely, when you link a post on mastadon users should be able to view the post while staying in app. I notice this mainly because I am a mobile user. Anyone else been frustrated by this?

2025-06-30 16:57:44 GMT

- reply

@nprofile…v2av I seem to recall you making a technical distinction in the past about arrows and morphisms but I can’t recall the context.

2025-06-28 19:42:29 GMT

- reply

@nprofile…hszg when I said “what I think is being asked” I didn’t meant by you I meant by ____. In their post they asked about your quote, "even *without* the univalence axiom, it is just *impossible* for you to write down a (true or false) mathematical statement that is not invariant under isomorphism". I believe your reply above answers this.

2025-06-28 19:26:14 GMT

- reply

@nprofile…hszg @nprofile…rs4v
Do your notes cover the meta theoretic invariance under isomorphism that all type theorist must accept? If so where? I think that is what is being asked about?

2025-06-26 22:54:28 GMT

- reply

@nprofile…hszg doesn’t work for me on an iPhone.

2025-06-23 19:49:08 GMT

- reply

@nprofile…6kk0 @nprofile…hszg wish more people did this (assuming you also assure them no negative repercussions for being out sick).

2025-06-22 17:59:29 GMT

- reply

@nprofile…hszg that is annoying.

2025-06-21 20:52:02 GMT

- reply

@nprofile…hszg @nprofile…6kk0 is it too late to correct this terminological defect? Does anyone not agree?

2025-06-21 20:03:31 GMT

- reply

@nprofile…hszg is there a reason you say isomorphic not equivalent?

2025-06-11 19:07:25 GMT

- reply

@nprofile…6kk0 looks pretty

2025-05-20 21:57:08 GMT

- reply

@nprofile…6kk0 interesting. Curious if you have a handy example of the internal statement being different? I know I asked a vague question and I was looking for answers just like you gave, but I am curious.

2025-05-20 20:48:51 GMT

Why do we care about proving facts, that are known externally, internally (wrt to categories/type theories, etc.) I *think* there are many answers and I may have vague ideas of a few of those but I’m still curious what others have to say.

2025-05-13 19:32:55 GMT

- reply

@nprofile…6kk0 @nprofile…wmyf
Don’t you mean replace f with x?

2025-05-05 18:26:37 GMT

- reply

@nprofile…fa4k @nprofile…r8sr @nprofile…hszg
Martin has helped me a lot. And Andrej, more indirectly, has too.

2025-05-05 18:11:44 GMT

- reply

@nprofile…q7zp @nprofile…fa4k @nprofile…dpa9
I discovered this guy on YouTube around the time I started exploring constructive mathematics. I, a naive young mathematician, very quickly became disillusioned with his claims because he seemed very arrogant and self assured. He acted like he alone held the suspicions of mainstream math, never referenced any other work and never made any of it satisfactorily precise.

2025-04-08 10:38:56 GMT

- reply

@nprofile…6kk0 I use emacs for no particular reason 😎

2025-04-03 12:53:22 GMT

- reply

@nprofile…6kk0 don’t forget to ask chatGPT to make sure it’s right

2025-02-14 15:11:35 GMT

- reply

@nprofile…6kk0
As someone who unfortunately lives in the US what’s even funnier is that you rarely hear it on the lips, but rather from the thumbs of the stupidest people on earth.

2025-02-14 01:54:09 GMT

- reply

@nprofile…2pts this is awful

2025-02-12 21:06:41 GMT

- reply

@nprofile…6kk0 has anyone made a path algebra solver?

2025-02-12 20:59:58 GMT

How do solvers work in proof assistants?