Toots for mudri@mathstodon.xyz account

Written by James Wood on 2025-02-04 at 17:49

I find it amusing, but quite bizarre, that some eastbound 34s run part route to Semple Street and become southbound X33s. I wonder whether some X33s do the reverse. I've never seen it, but I suppose it'd happen at the end of rush hour.

=> More informations about this toot | View the thread

Written by James Wood on 2025-01-23 at 17:17

Urgh, I'm too ill to go to POPL today.

=> More informations about this toot | View the thread

Written by James Wood on 2025-01-19 at 03:33

America, I am in you.

=> View attached media

=> More informations about this toot | View the thread

Written by James Wood on 2025-01-17 at 16:10

I am once again asking for your recommendations of Android music players that let me turn off audio ducking.

=> More informations about this toot | View the thread

Written by James Wood on 2025-01-17 at 09:01

Anyone else doing Heathrow to Denver tomorrow?

=> More informations about this toot | View the thread

Written by James Wood on 2025-01-14 at 17:53

Wait, is the tram really slower than 2 buses?

=> View attached media

=> More informations about this toot | View the thread

Written by James Wood on 2025-01-10 at 15:45

WTF; NO!

=> View attached media

=> More informations about this toot | View the thread

Written by James Wood on 2025-01-04 at 12:37

Urgh, I don't really want to depend on indices coming from a setoid.

=> More informations about this toot | View the thread

Written by James Wood on 2025-01-03 at 15:39

I think I actually want pseudomonoids on Span(Set). Or rather, on the equivalent bicategory that avoids having to use spans when I already have indexed types.

=> More informations about this toot | View the thread

Written by James Wood on 2025-01-02 at 17:05

After a nice relaxing Christmas break, I think it's time to do some Agda hacking.

I wanted to start off with a question, but instead I'm filling in all the gaps needed to give the Poset-enriched category of sets and relations so that I can check that I'm asking the right question...

=> More informations about this toot | View the thread

Written by James Wood on 2025-01-01 at 17:03

2025 snow: tick!

=> More informations about this toot | View the thread

Written by James Wood on 2024-12-01 at 11:57

Chaos on the rails today has left me on a largely empty Class 800 running non-stop from Peterborough to York. Good times.

=> More informations about this toot | View the thread

Written by James Wood on 2024-12-01 at 11:29

I've never seen a train quite like the Class 755 before. It seems to have a separate very short coach in the middle of the train for a diesel engine.

=> More informations about this toot | View the thread

Written by James Wood on 2024-11-25 at 20:21

You know the one.

=> View attached media

=> More informations about this toot | View the thread

Written by James Wood on 2024-11-25 at 19:19

Now I head to the other land of the Dutch – the Dutch that call themselves Dutch, and the Dutch the Dutch call Dutch.

=> More informations about this toot | View the thread

Written by James Wood on 2024-11-24 at 18:36

I don't want to change the world

=> View attached media

=> More informations about this toot | View the thread

Written by James Wood on 2024-11-24 at 17:36

Bloody Trots, always opping mine work!

=> View attached media

=> More informations about this toot | View the thread

Written by James Wood on 2024-10-30 at 20:42

Surely, if anything, I didn't travel ScotRail; ScotRail travelled me.

=> More informations about this toot | View the thread

Written by James Wood on 2024-10-12 at 11:39

In Coq/Rocq, we abstract common patterns in Gallina using Definition, and common patterns in Ltac using Ltac. How do we abstract common patterns in Vernacular?

=> More informations about this toot | View the thread

Written by James Wood on 2024-09-18 at 19:50

Given that “catholic” can mean “universal” or “embracing all” (“below/in accordance with the whole”), the version with a capital letter seems like a bad name for the kind of indices it describes (precisely those that can take a limited range of values).

=> More informations about this toot | View the thread

=> This profile with reblog | Go to mudri@mathstodon.xyz account