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/
Martin Escardo /
npub1t3…fg3z4
2023-08-18 20:49:48
Author Public Key
npub1t3n4le6kr3f09s823keer5kr53j4d0kf50q2fd83pu35lcpltr9q0fg3z4Published at
2023-08-18 20:49:48Event JSON
{
"id": "f0ff9a890e933207794880c74e9f34bfda6d2a18e1ef4fcb037b5907ee997ae9",
"pubkey": "5c675fe7561c52f2c0ea8db391d2c3a46556bec9a3c0a4b4f10f234fe03f58ca",
"created_at": 1692391788,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/users/MartinEscardo/statuses/110912588238494225",
"activitypub"
]
],
"content": "Injective types in constructive HoTT/UF.\n\nThis 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.\n\nMotivation. Very often we want to extend functions to larger domains of definition. This may or may not possible.\n\nThe notion of injectivity is about the possibility of extensions, as we shall see when I eventually give the definition of injective type.\n\n(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.)\n\n1/",
"sig": "c6e70bd2d90780f8f4416751f16d78f541ad65697b39df36030d3edf1943cc2c2941acb5289471db80f9a6fd2295672e357fe56e400bbd295a20cbb06c24e051"
}