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/