bblfish on Nostr: Hi #[1] here's an interesting case for your #mostr.pub. Martin Escardo wrote a 20 ...

Hi Alex Gleason (npub15ph…kw0q) here's an interesting case for your #mostr.pub.
Martin Escardo wrote a 20 post thread on Mastodon which started here:
https://mathstodon.xyz/@MartinEscardo/110912588238494225
It looks like I need to reToot each post in the thread on w3c.social for the other Toots to appear on #nostr.
So you’ll see I rebooted half of them on https://w3c.social/@bblfish
But I think that may bother folks at W3C if I do that too often. It would help if when I reboot one, the whole thread then becomes visible on nostr.

quoting nevent1q…pv2s

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/