Martin Escardo / is on Nostr

Professor at the University of Birmingham, UK.
I am interested in constructive mathematics and (constructive and non-constructive) homotopy type theory and univalent foundations, connections of topology with computation, (infinity) topos theory, locale theory, domain theory, combinatorial game theory and much more.

Last Notes

2024-08-12 20:22:45

- reply

@npub1c9m…9xjd What does your wife think about this?

2023-09-08 12:27:29

- reply

@npub1z2q…3yuf It worked for me immediately on Firefox, which is the only browser I use, except in the above circumstance. It ust have been a glitch.

2023-09-08 12:03:54

- reply

@npub1z2q…3yuf You actually don't need to do wget first.
See https://developer.chrome.com/blog/headless-chrome/

2023-09-03 06:32:56

- reply

@npub1m5h…4v3j Same.

2023-09-03 06:32:27

- reply

@npub1m5h…4v3j @npub1jd8…t4jc TypeTopology does that.

2023-08-18 20:49:48

Injective types in constructive HoTT/UF.
This is a very long thread, written in the style of a blog post, but split into chunks so that people can ask questions or make remarks about specific things I say or ask. I will unlist all but this initial post to avoid clutter in your timeline.
Motivation. Very often we want to extend functions to larger domains of definition. This may or may not possible.
The notion of injectivity is about the possibility of extensions, as we shall see when I eventually give the definition of injective type.
(I don't know where the terminology "injective", for mathematical objects rather than functions, comes from. Who were the first people to use and define it? I am sure this was used before the notion was defined explicitly, as is often the case.)
1/